theorem Regex.find_str_eq_some {re : Regex} {haystack : String} {slice : String.Slice} (h : re.find haystack = some slice) : slice.str = haystack

theorem Regex.captures_of_find_some {re : Regex} {haystack : String} {slice : String.Slice} (h : re.find haystack = some slice) (isr : re.IsSearchRegex) : Matches.Spec isr haystack haystack.startValidPosPlusOne slice ⋯

theorem Regex.captures_of_mem_findAll.go {haystack : String} {m : Matches haystack} {accum : Array String.Slice} (isr : m.regex.IsSearchRegex) (inv : ∀ slice ∈ accum, ∃ (startPos : haystack.ValidPosPlusOne) (eq : slice.str = haystack), Matches.Spec isr haystack startPos slice eq) (slice : String.Slice) : slice ∈ findAll.go haystack m accum → ∃ (startPos : haystack.ValidPosPlusOne) (eq : slice.str = haystack), Matches.Spec isr haystack startPos slice eq

theorem Regex.captures_of_mem_findAll {re : Regex} {haystack : String} {slice : String.Slice} (mem : slice ∈ re.findAll haystack) (isr : re.IsSearchRegex) : ∃ (startPos : haystack.ValidPosPlusOne) (eq : slice.str = haystack), Matches.Spec isr haystack startPos slice eq

theorem Regex.captures_of_capture_some {re : Regex} {haystack : String} {captured : CapturedGroups haystack} (h : re.capture haystack = some captured) (isr : re.IsSearchRegex) : CapturedGroups.Spec isr haystack haystack.startValidPosPlusOne captured

theorem Regex.captures_of_mem_captureAll.go {haystack : String} {captures : Captures haystack} {accum : Array (CapturedGroups haystack)} (isr : captures.regex.IsSearchRegex) (inv : ∀ captured ∈ accum, ∃ (startPos : haystack.ValidPosPlusOne), CapturedGroups.Spec isr haystack startPos captured) (captured : CapturedGroups haystack) : captured ∈ captureAll.go haystack captures accum → ∃ (startPos : haystack.ValidPosPlusOne), CapturedGroups.Spec isr haystack startPos captured

theorem Regex.captures_of_mem_captureAll {re : Regex} {haystack : String} {captured : CapturedGroups haystack} (mem : captured ∈ re.captureAll haystack) (isr : re.IsSearchRegex) : ∃ (startPos : haystack.ValidPosPlusOne), CapturedGroups.Spec isr haystack startPos captured