theorem Regex.VM.captureNext.captures_of_some_compile {e : Data.Expr} {it₀ : String.Iterator} {matched' : Option HistoryStrategy.Update} (h : captureNext HistoryStrategy (NFA.compile e) ⋯ it₀ = matched') (v : it₀.Valid) (isSome' : matched'.isSome = true) : ∃ (it : String.Iterator) (it' : String.Iterator) (groups : Data.CaptureGroups), it.toString = it₀.toString ∧ it₀.pos ≤ it.pos ∧ Data.Expr.Captures it it' groups e ∧ NFA.EquivUpdate groups (matched'.get isSome')

theorem Regex.VM.captureNext.not_captures_of_none_compile {e : Data.Expr} {it : String.Iterator} (h : captureNext HistoryStrategy (NFA.compile e) ⋯ it = none) (v : it.Valid) (it' it'' : String.Iterator) (groups : Data.CaptureGroups) (eqs : it'.toString = it.toString) (le : it.pos ≤ it'.pos) : ¬Data.Expr.Captures it' it'' groups e