theorem
Regex.NFA.EquivUpdate.materialize
{s : String}
{e : Data.Expr}
{n : ℕ}
{pos pos' : s.Pos}
{groups : Data.CaptureGroups s}
{updates : List (ℕ × s.Pos)}
(c : Data.Expr.Captures pos pos' groups e)
(disj : e.Disjoint)
(eqv : EquivUpdate groups updates)
:
Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups groups) (Strategy.materializeUpdates n updates)
Under suitable conditions, the equivalence between capture groups and NFA buffer updates can be naturally transformed into a materialized version.