theorem
Regex.Data.Expr.BacktrackingTree.mem_extractCaptures_of_captures
{s : String}
{p p' : s.Pos}
{groups : CaptureGroups s}
{e : Expr}
{t : BacktrackingTree}
(v : IsValid [Action.expr e] p GroupMap.empty t)
(disj : e.Disjoint)
(c : Captures p p' groups e)
:
theorem
Regex.Data.Expr.BacktrackingTree.captures_of_mem_extractCaptures
{s : String}
{p p' : s.Pos}
{gs : GroupMap s}
{e : Expr}
{t : BacktrackingTree}
(v : IsValid [Action.expr e] p GroupMap.empty t)
(hmem : (p', gs) ∈ extractCaptures p t)
(disj : e.Disjoint)
:
∃ (groups : CaptureGroups s), Captures p p' groups e ∧ gs = GroupMap.empty.addCaptures groups