theorem Regex.NFA.EquivUpdate.materialize {e : Data.Expr} {n : ℕ} {it it' : String.Iterator} {groups : Data.CaptureGroups} {updates : List (ℕ × String.Pos)} (c : Data.Expr.Captures it it' 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.

theorem Regex.NFA.EquivUpdate.materialize.concat {n : ℕ} {g₁ g₂ : Data.CaptureGroups} {u₁ u₂ : List (ℕ × String.Pos)} (eqv₁ : Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups g₁) (Strategy.materializeUpdates n u₁)) (eqv₂ : Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups g₂) (Strategy.materializeUpdates n u₂)) (tag : ℕ) : (∀ (h₁ : 2 * tag < n), Option.map (fun (x : String.Pos × String.Pos) => x.1) (Strategy.materializeRegexGroups (g₁.concat g₂) tag) = (Strategy.materializeUpdates n (u₁ ++ u₂))[2 * tag]) ∧ ∀ (h₂ : 2 * tag + 1 < n), Option.map (fun (x : String.Pos × String.Pos) => x.2) (Strategy.materializeRegexGroups (g₁.concat g₂) tag) = (Strategy.materializeUpdates n (u₁ ++ u₂))[2 * tag + 1]