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

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

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

theorem Regex.Backtracker.captureNext.not_captures_of_none_compile {e : Data.Expr} {it : String.Iterator} (hres : captureNext HistoryStrategy (NFA.compile e) ⋯ it = none) (v : it.Valid) (it' it'' : String.Iterator) (groups : Data.CaptureGroups) (eqs : it'.toString = it.toString) (le : it.pos ≤ it'.pos) : ¬Data.Expr.Captures it' it'' groups e