inductive Regex.NFA.EquivUpdate {s : String} : Data.CaptureGroups s → List (Nat × s.Pos) → Prop

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

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