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

• empty {s : String} : EquivUpdate Data.CaptureGroups.empty []
• group {s : String} {groups : Data.CaptureGroups s} {updates : List (ℕ × s.ValidPos)} {tag : ℕ} {first last : s.ValidPos} (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 (ℕ × s.ValidPos)} (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 (ℕ × s.ValidPos)} {offset : ℕ} {pos : s.ValidPos} (h : (offset, pos) ∈ updates) (eqv : EquivUpdate groups updates) : ∃ (tag : ℕ) (first : s.ValidPos) (last : s.ValidPos), (tag, first, last) ∈ groups ∧ (offset = 2 * tag ∨ offset = 2 * tag + 1)