theorem Regex.Backtracker.captureNextAux.mem_or_path_of_mem_of_none {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit₀ bit : Data.BoundedIterator startIdx maxIdx} {visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} {result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} (hres : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited [{ update := HistoryStrategy.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = result) (isNone : result.1 = none) (reaches : bit₀.Reaches bit) : VisitedInv wf bit₀ bit reaches visited result.2

theorem Regex.Backtracker.captureNextAux.PathClosure.preserves {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit₀ bit : Data.BoundedIterator startIdx maxIdx} {visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} {result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} (hres : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited [{ update := HistoryStrategy.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = result) (isNone : result.1 = none) (reaches : bit₀.Reaches bit) (cls : PathClosure bit₀ visited) : PathClosure bit₀ result.2

theorem Regex.Backtracker.captureNextAux.mem_of_path_of_none {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit₀ bit : Data.BoundedIterator startIdx maxIdx} {visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} {result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} (hres : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited [{ update := HistoryStrategy.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = result) (isNone : result.1 = none) (reaches : bit₀.Reaches bit) (cls : PathClosure bit₀ visited) (bit' : Data.BoundedIterator startIdx maxIdx) (state : Fin nfa.nodes.size) (update : List (ℕ × String.Pos)) (path : Path nfa wf bit.it bit'.it state update) : result.2.get state bit'.index = true

theorem Regex.Backtracker.captureNextAux.mem_iff_mem_or_path_of_none {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit₀ bit : Data.BoundedIterator startIdx maxIdx} {visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} {result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} (hres : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited [{ update := HistoryStrategy.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = result) (isNone : result.1 = none) (reaches : bit₀.Reaches bit) (cls : PathClosure bit₀ visited) (bit' : Data.BoundedIterator startIdx maxIdx) (state : Fin nfa.nodes.size) (reaches' : bit₀.Reaches bit') : result.2.get state bit'.index = true ↔ visited.get state bit'.index = true ∨ ∃ (update : List (ℕ × String.Pos)), Path nfa wf bit.it bit'.it state update

structure Regex.Backtracker.captureNext.go.Inv {nfa : NFA} {startIdx maxIdx : ℕ} (wf : nfa.WellFormed) (bit₀ bit : Data.BoundedIterator startIdx maxIdx) (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) : Prop

• closure : captureNextAux.PathClosure bit₀ visited
• mem_iff_path (state' : Fin nfa.nodes.size) (bit' : Data.BoundedIterator startIdx maxIdx) : bit₀.Reaches bit' → (visited.get state' bit'.index = true ↔ ∃ (bitPrev : Data.BoundedIterator startIdx maxIdx) (update : List (ℕ × String.Pos)), bitPrev.BetweenE bit₀ bit ∧ Path nfa wf bitPrev.it bit'.it state' update)

theorem Regex.Backtracker.captureNext.go.Inv.zero {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit₀ : Data.BoundedIterator startIdx maxIdx} : Inv wf bit₀ bit₀ (Data.BitMatrix.zero nfa.nodes.size (maxIdx + 1 - startIdx))

theorem Regex.Backtracker.captureNext.go.Inv.mem_iff_of_aux_none {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit₀ bit : Data.BoundedIterator startIdx maxIdx} {visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} {result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} (haux : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited [{ update := HistoryStrategy.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = result) (isNone : result.1 = none) (reaches : bit₀.Reaches bit) (inv : Inv wf bit₀ bit visited) (state' : Fin nfa.nodes.size) (bit' : Data.BoundedIterator startIdx maxIdx) (reaches' : bit₀.Reaches bit') : result.2.get state' bit'.index = true ↔ (∃ (bitPrev : Data.BoundedIterator startIdx maxIdx) (update : List (ℕ × String.Pos)), bitPrev.BetweenE bit₀ bit ∧ Path nfa wf bitPrev.it bit'.it state' update) ∨ ∃ (update : List (ℕ × String.Pos)), Path nfa wf bit.it bit'.it state' update

theorem Regex.Backtracker.captureNext.go.Inv.preservesAux {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit₀ bit : Data.BoundedIterator startIdx maxIdx} {visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} {result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} (haux : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited [{ update := HistoryStrategy.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = result) (isNone : result.1 = none) (hnext : bit.hasNext = true) (reaches : bit₀.Reaches bit) (inv : Inv wf bit₀ bit visited) : Inv wf bit₀ (bit.next hnext) result.2

theorem Regex.Backtracker.captureNext.go.Inv.mem_iff_path_of_aux_none_of_not_hasNext {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit₀ bit : Data.BoundedIterator startIdx maxIdx} {visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} {result : Option HistoryStrategy.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} (haux : captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited [{ update := HistoryStrategy.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = result) (isNone : result.1 = none) (reaches : bit₀.Reaches bit) (hnext : ¬bit.hasNext = true) (inv : Inv wf bit₀ bit visited) (state' : Fin nfa.nodes.size) (bit' : Data.BoundedIterator startIdx maxIdx) (reaches' : bit₀.Reaches bit') : result.2.get state' bit'.index = true ↔ ∃ (bit : Data.BoundedIterator startIdx maxIdx) (update : List (ℕ × String.Pos)), bit₀.Reaches bit ∧ Path nfa wf bit.it bit'.it state' update

theorem Regex.Backtracker.captureNext.go.ne_done_of_path_of_none {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit₀ bit : Data.BoundedIterator startIdx maxIdx} {visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} (hres : go HistoryStrategy nfa wf startIdx maxIdx bit visited = none) (reaches : bit₀.Reaches bit) (inv : Inv wf bit₀ bit visited) (ndinv : captureNextAux.NotDoneInv visited) (bit' bit'' : Data.BoundedIterator startIdx maxIdx) (state : Fin nfa.nodes.size) (update : List (ℕ × String.Pos)) : bit₀.Reaches bit' → Path nfa wf bit'.it bit''.it state update → nfa[state] ≠ NFA.Node.done

theorem Regex.Backtracker.captureNext.go.path_done_of_some {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx : ℕ} {bit : Data.BoundedIterator startIdx maxIdx} {update : HistoryStrategy.Update} {visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)} (v : bit.Valid) (hres : go HistoryStrategy nfa wf startIdx maxIdx bit visited = some update) : ∃ (state : Fin nfa.nodes.size) (bit' : Data.BoundedIterator startIdx maxIdx) (bit'' : Data.BoundedIterator startIdx maxIdx), nfa[state] = NFA.Node.done ∧ bit.Reaches bit' ∧ Path nfa wf bit'.it bit''.it state update