inductive Regex.NFA.EquivUpdate : Data.CaptureGroups → List (ℕ × String.Pos) → Prop

• empty : EquivUpdate Data.CaptureGroups.empty []
• group {groups : Data.CaptureGroups} {updates : List (ℕ × String.Pos)} {tag : ℕ} {first last : String.Pos} (eqv : EquivUpdate groups updates) : EquivUpdate (Data.CaptureGroups.group tag first last groups) ((2 * tag, first) :: updates ++ [(2 * tag + 1, last)])
• concat {groups₁ groups₂ : Data.CaptureGroups} {updates₁ updates₂ : List (ℕ × String.Pos)} (eqv₁ : EquivUpdate groups₁ updates₁) (eqv₂ : EquivUpdate groups₂ updates₂) : EquivUpdate (groups₁.concat groups₂) (updates₁ ++ updates₂)

theorem Regex.NFA.EquivUpdate.mem_groups_of_mem_updates {groups : Data.CaptureGroups} {updates : List (ℕ × String.Pos)} {offset : ℕ} {pos : String.Pos} (h : (offset, pos) ∈ updates) (eqv : EquivUpdate groups updates) : ∃ (tag : ℕ) (first : String.Pos) (last : String.Pos), (tag, first, last) ∈ groups ∧ (offset = 2 * tag ∨ offset = 2 * tag + 1)