theorem Regex.Backtracker.captureNext.path_done_of_some {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos : s.ValidPos} {update : (HistoryStrategy s).Update} (hres : captureNext (HistoryStrategy s) nfa wf pos = some update) : ∃ (state : Fin nfa.nodes.size) (pos' : s.ValidPos) (pos'' : s.ValidPos), nfa[state] = NFA.Node.done ∧ pos ≤ pos' ∧ Path nfa wf pos' pos'' state update

theorem Regex.Backtracker.captureNext.capture_of_some_compile {s : String} {e : Data.Expr} {pos : s.ValidPos} {update : (HistoryStrategy s).Update} (hres : captureNext (HistoryStrategy s) (NFA.compile e) ⋯ pos = some update) : ∃ (pos' : s.ValidPos) (pos'' : s.ValidPos) (groups : Data.CaptureGroups s), pos ≤ pos' ∧ Data.Expr.Captures pos' pos'' groups e ∧ NFA.EquivUpdate groups update

theorem Regex.Backtracker.captureNext.ne_done_of_path_of_none {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos : s.ValidPos} (hres : captureNext (HistoryStrategy s) nfa wf pos = none) (pos' pos'' : s.ValidPos) (state : Fin nfa.nodes.size) (update : List (ℕ × s.ValidPos)) : pos ≤ pos' → Path nfa wf pos' pos'' state update → nfa[state] ≠ NFA.Node.done

theorem Regex.Backtracker.captureNext.not_captures_of_none_compile {s : String} {e : Data.Expr} {pos : s.ValidPos} (hres : captureNext (HistoryStrategy s) (NFA.compile e) ⋯ pos = none) (pos' pos'' : s.ValidPos) (groups : Data.CaptureGroups s) (le : pos ≤ pos') : ¬Data.Expr.Captures pos' pos'' groups e