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

theorem Regex.VM.captureNext.not_captures_of_none_compile {s : String} {e : Data.Expr} {pos : s.ValidPos} (h : captureNext (HistoryStrategy s) (NFA.compile e) ⋯ pos = none) (pos' pos'' : s.ValidPos) (groups : Data.CaptureGroups s) (le : pos ≤ pos') : ¬Data.Expr.Captures pos' pos'' groups e