theorem
Regex.Backtracker.captureNextAux.pushNext.done
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
(hn : nfa[state] = NFA.Node.done)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.fail
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
(hn : nfa[state] = NFA.Node.fail)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.epsilonFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.epsilon ↑state')
:
theorem
Regex.Backtracker.captureNextAux.pushNext.epsilon
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{state' : Nat}
(hn : nfa[state] = NFA.Node.epsilon state')
:
theorem
Regex.Backtracker.captureNextAux.pushNext.splitFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{state₁ state₂ : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.split ↑state₁ ↑state₂)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.split
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{state₁ state₂ : Nat}
(hn : nfa[state] = NFA.Node.split state₁ state₂)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.saveFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{offset : Nat}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.save offset ↑state')
:
theorem
Regex.Backtracker.captureNextAux.pushNext.save
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{offset state' : Nat}
(hn : nfa[state] = NFA.Node.save offset state')
:
theorem
Regex.Backtracker.captureNextAux.pushNext.anchor_posFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{a : Data.Anchor}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.anchor a ↑state')
(h : Data.Anchor.test it.it a = true)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.anchor_pos
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{a : Data.Anchor}
{state' : Nat}
(hn : nfa[state] = NFA.Node.anchor a state')
(h : Data.Anchor.test it.it a = true)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.anchor_negFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{a : Data.Anchor}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.anchor a ↑state')
(h : ¬Data.Anchor.test it.it a = true)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.anchor_neg
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{a : Data.Anchor}
{state' : Nat}
(hn : nfa[state] = NFA.Node.anchor a state')
(h : ¬Data.Anchor.test it.it a = true)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.char_posFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{c : Char}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.char c ↑state')
(h : it.hasNext = true)
(hc : it.curr h = c)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.char_pos
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{c : Char}
{state' : Nat}
(hn : nfa[state] = NFA.Node.char c state')
(h : it.hasNext = true)
(hc : it.curr h = c)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.char_negFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{c : Char}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.char c ↑state')
(h : it.hasNext = true)
(hc : ¬it.curr h = c)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.char_endFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{c : Char}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.char c ↑state')
(h : ¬it.hasNext = true)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.char_neg
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{c : Char}
{state' : Nat}
(hn : nfa[state] = NFA.Node.char c state')
(h : ¬it.hasNext = true ∨ ∃ (hnext : it.hasNext = true), ¬it.curr hnext = c)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.sparse_posFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{cs : Data.Classes}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.sparse cs ↑state')
(h : it.hasNext = true)
(hc : it.curr h ∈ cs)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.sparse_pos
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{cs : Data.Classes}
{state' : Nat}
(hn : nfa[state] = NFA.Node.sparse cs state')
(h : it.hasNext = true)
(hc : it.curr h ∈ cs)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.sparse_negFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{cs : Data.Classes}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.sparse cs ↑state')
(h : it.hasNext = true)
(hc : ¬it.curr h ∈ cs)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.sparse_endFin
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{cs : Data.Classes}
{state' : Fin nfa.nodes.size}
(hn : nfa[state] = NFA.Node.sparse cs ↑state')
(h : ¬it.hasNext = true)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.sparse_neg
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{stack : List (StackEntry σ nfa startIdx maxIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{cs : Data.Classes}
{state' : Nat}
(hn : nfa[state] = NFA.Node.sparse cs state')
(h : ¬it.hasNext = true ∨ ∃ (hnext : it.hasNext = true), ¬it.curr hnext ∈ cs)
:
theorem
Regex.Backtracker.captureNextAux.pushNext.fun_cases'
(σ : Strategy)
(nfa : NFA)
(wf : nfa.WellFormed)
(startIdx maxIdx : Nat)
{motive :
List (StackEntry σ nfa startIdx maxIdx) → σ.Update → Fin nfa.nodes.size → Data.BoundedIterator startIdx maxIdx → Prop}
(done :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx), nfa[state] = NFA.Node.done → motive stack update state it)
(fail :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx), nfa[state] = NFA.Node.fail → motive stack update state it)
(epsilon :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (state' : Fin nfa.nodes.size),
nfa[state] = NFA.Node.epsilon ↑state' → motive stack update state it)
(split :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (state₁ state₂ : Fin nfa.nodes.size),
nfa[state] = NFA.Node.split ↑state₁ ↑state₂ → motive stack update state it)
(save :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (offset : Nat) (state' : Fin nfa.nodes.size),
nfa[state] = NFA.Node.save offset ↑state' → motive stack update state it)
(anchor_pos :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (a : Data.Anchor) (state' : Fin nfa.nodes.size),
nfa[state] = NFA.Node.anchor a ↑state' → Data.Anchor.test it.it a = true → motive stack update state it)
(anchor_neg :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (a : Data.Anchor) (state' : Fin nfa.nodes.size),
nfa[state] = NFA.Node.anchor a ↑state' → ¬Data.Anchor.test it.it a = true → motive stack update state it)
(char_pos :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (c : Char) (state' : Fin nfa.nodes.size),
nfa[state] = NFA.Node.char c ↑state' → ∀ (h : it.hasNext = true), it.curr h = c → motive stack update state it)
(char_neg :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (c : Char) (state' : Fin nfa.nodes.size),
nfa[state] = NFA.Node.char c ↑state' →
(¬it.hasNext = true ∨ ∃ (hnext : it.hasNext = true), ¬it.curr hnext = c) → motive stack update state it)
(sparse_pos :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (cs : Data.Classes) (state' : Fin nfa.nodes.size),
nfa[state] = NFA.Node.sparse cs ↑state' → ∀ (h : it.hasNext = true), it.curr h ∈ cs → motive stack update state it)
(sparse_neg :
∀ (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (cs : Data.Classes) (state' : Fin nfa.nodes.size),
nfa[state] = NFA.Node.sparse cs ↑state' →
(¬it.hasNext = true ∨ ∃ (hnext : it.hasNext = true), ¬it.curr hnext ∈ cs) → motive stack update state it)
(stack : List (StackEntry σ nfa startIdx maxIdx))
(update : σ.Update)
(state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx)
:
motive stack update state it
theorem
Regex.Backtracker.captureNextAux.induct'
(σ : Strategy)
(nfa : NFA)
(wf : nfa.WellFormed)
(startIdx maxIdx : Nat)
(motive : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx) → List (StackEntry σ nfa startIdx maxIdx) → Prop)
(base : ∀ (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)), motive visited [])
(visited :
∀ (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (stack' : List (StackEntry σ nfa startIdx maxIdx)),
visited.get state it.index = true →
motive visited stack' → motive visited ({ update := update, state := state, it := it } :: stack'))
(done :
∀ (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (stack' : List (StackEntry σ nfa startIdx maxIdx)),
¬visited.get state it.index = true →
nfa[state] = NFA.Node.done → motive visited ({ update := update, state := state, it := it } :: stack'))
(next :
∀ (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) (update : σ.Update) (state : Fin nfa.nodes.size)
(it : Data.BoundedIterator startIdx maxIdx) (stack' : List (StackEntry σ nfa startIdx maxIdx)),
¬visited.get state it.index = true →
nfa[state] ≠ NFA.Node.done →
motive (visited.set state it.index) (pushNext σ nfa wf startIdx maxIdx stack' update state it) →
motive visited ({ update := update, state := state, it := it } :: stack'))
(visited✝ : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx))
(stack : List (StackEntry σ nfa startIdx maxIdx))
:
motive visited✝ stack
theorem
Regex.Backtracker.captureNextAux_base
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
:
theorem
Regex.Backtracker.captureNextAux_visited
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{stack' : List (StackEntry σ nfa startIdx maxIdx)}
(mem : visited.get state it.index = true)
:
captureNextAux σ nfa wf startIdx maxIdx visited ({ update := update, state := state, it := it } :: stack') = captureNextAux σ nfa wf startIdx maxIdx visited stack'
theorem
Regex.Backtracker.captureNextAux_done
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{stack' : List (StackEntry σ nfa startIdx maxIdx)}
(mem : ¬visited.get state it.index = true)
(hn : nfa[state] = NFA.Node.done)
:
theorem
Regex.Backtracker.captureNextAux_next
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{update : σ.Update}
{state : Fin nfa.nodes.size}
{it : Data.BoundedIterator startIdx maxIdx}
{stack' : List (StackEntry σ nfa startIdx maxIdx)}
(mem : ¬visited.get state it.index = true)
(hn : nfa[state] ≠ NFA.Node.done)
:
captureNextAux σ nfa wf startIdx maxIdx visited ({ update := update, state := state, it := it } :: stack') = captureNextAux σ nfa wf startIdx maxIdx (visited.set state it.index)
(captureNextAux.pushNext σ nfa wf startIdx maxIdx stack' update state it)
theorem
Regex.Backtracker.captureNext.go.induct'
(σ : Strategy)
(nfa : NFA)
(wf : nfa.WellFormed)
(startIdx maxIdx : Nat)
(motive : Data.BoundedIterator startIdx maxIdx → Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx) → Prop)
(found :
∀ (bit : Data.BoundedIterator startIdx maxIdx) (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx))
(update : σ.Update) (visited' : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)),
captureNextAux σ nfa wf startIdx maxIdx visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = (some update, visited') →
motive bit visited)
(not_found_next :
∀ (bit : Data.BoundedIterator startIdx maxIdx)
(visited visited' : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)),
captureNextAux σ nfa wf startIdx maxIdx visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = (none, visited') →
∀ (h : bit.hasNext = true), motive (bit.next h) visited' → motive bit visited)
(not_found_end :
∀ (bit : Data.BoundedIterator startIdx maxIdx)
(visited visited' : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)),
captureNextAux σ nfa wf startIdx maxIdx visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = (none, visited') →
¬bit.hasNext = true → motive bit visited)
(bit : Data.BoundedIterator startIdx maxIdx)
(visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx))
:
motive bit visited
theorem
Regex.Backtracker.captureNext.go_found
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{bit : Data.BoundedIterator startIdx maxIdx}
{visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
{update : σ.Update}
{visited' : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
(h :
captureNextAux σ nfa wf startIdx maxIdx visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = (some update, visited'))
:
theorem
Regex.Backtracker.captureNext.go_not_found_next
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{bit : Data.BoundedIterator startIdx maxIdx}
{visited visited' : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
(h :
captureNextAux σ nfa wf startIdx maxIdx visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = (none, visited'))
(h' : bit.hasNext = true)
:
theorem
Regex.Backtracker.captureNext.go_not_found_end
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : Nat}
{bit : Data.BoundedIterator startIdx maxIdx}
{visited visited' : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)}
(h :
captureNextAux σ nfa wf startIdx maxIdx visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, it := bit }] = (none, visited'))
(h' : ¬bit.hasNext = true)
:
theorem
Regex.Backtracker.captureNext_le
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
(le : it.pos ≤ it.toString.endPos)
:
theorem
Regex.Backtracker.captureNext_not_le
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
(h : ¬it.pos ≤ it.toString.endPos)
: