theorem Regex.NFA.path_of_captures {s : String} {nfa : NFA} {next : ℕ} {e : Data.Expr} {result : NFA} {pos pos' : s.Pos} {groups : Data.CaptureGroups s} (eq : nfa.pushRegex next e = result) (wf : nfa.WellFormed) (next_lt : next < nfa.size) (c : Data.Expr.Captures pos pos' groups e) : ∃ (update : List (ℕ × s.Pos)), EquivUpdate groups update ∧ result.Path nfa.size result.start pos next pos' update

theorem Regex.NFA.path_of_captures_compile {s : String} {nfa : NFA} {e : Data.Expr} {pos pos' : s.Pos} {groups : Data.CaptureGroups s} (eq : compile e = nfa) (c : Data.Expr.Captures pos pos' groups e) : ∃ (update : List (ℕ × s.Pos)), EquivUpdate groups update ∧ nfa.Path 1 nfa.start pos 0 pos' update