theorem Regex.captures_of_find_some {re : Regex} {haystack : String} {positions : Substring} (h : re.find haystack = some positions) (s : re.IsSearchRegex) : Matches.Spec s haystack { } positions

theorem Regex.captures_of_mem_findAll.go {m : Matches} {accum : Array Substring} (v : m.Valid) (inv : ∀ str ∈ accum, ∃ (startPos : String.Pos), Matches.Spec ⋯ m.haystack startPos str) (str : Substring) : str ∈ findAll.go m accum → ∃ (startPos : String.Pos), Matches.Spec ⋯ m.haystack startPos str

theorem Regex.captures_of_mem_findAll {re : Regex} {haystack : String} {positions : Substring} (mem : positions ∈ re.findAll haystack) (s : re.IsSearchRegex) : ∃ (startPos : String.Pos), Matches.Spec s haystack startPos positions

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

theorem Regex.captures_of_mem_captureAll.go {captures : Captures} {accum : Array CapturedGroups} (v : captures.Valid) (inv : ∀ captured ∈ accum, ∃ (startPos : String.Pos), CapturedGroups.Spec ⋯ captures.haystack startPos captured) (captured : CapturedGroups) : captured ∈ captureAll.go captures accum → ∃ (startPos : String.Pos), CapturedGroups.Spec ⋯ captures.haystack startPos captured

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