unfold captureNext.go at h
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
h : captureNext.go nfa saveSize it current next saveSlots lastMatch = matched
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h :
  (if it.atEnd = true then lastMatch
    else
      if (current.isEmpty && lastMatch.isSome) = true then lastMatch
      else
        let currentAndSaveSlots :=
          if lastMatch.isNone = true then
            let explored :=
              exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
            explored.2
          else (current, saveSlots);
        let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
        captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
          (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done