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