theorem Regex.Backtracker.captureNextAux.pushNext.done {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} (hn : nfa[state] = NFA.Node.done) : pushNext σ nfa wf startPos stack update state pos = stack

theorem Regex.Backtracker.captureNextAux.pushNext.fail {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} (hn : nfa[state] = NFA.Node.fail) : pushNext σ nfa wf startPos stack update state pos = stack

theorem Regex.Backtracker.captureNextAux.pushNext.epsilon {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {state' : Nat} (hn : nfa[state] = NFA.Node.epsilon state') : pushNext σ nfa wf startPos stack update state pos = { update := update, state := ⟨state', ⋯⟩, pos := pos } :: stack

theorem Regex.Backtracker.captureNextAux.pushNext.split {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {state₁ state₂ : Nat} (hn : nfa[state] = NFA.Node.split state₁ state₂) : pushNext σ nfa wf startPos stack update state pos = { update := update, state := ⟨state₁, ⋯⟩, pos := pos } :: { update := update, state := ⟨state₂, ⋯⟩, pos := pos } :: stack

theorem Regex.Backtracker.captureNextAux.pushNext.saveFin {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {offset : Nat} {state' : Fin nfa.nodes.size} (hn : nfa[state] = NFA.Node.save offset ↑state') : pushNext σ nfa wf startPos stack update state pos = { update := σ.write update offset pos.current, state := state', pos := pos } :: stack

theorem Regex.Backtracker.captureNextAux.pushNext.save {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {offset state' : Nat} (hn : nfa[state] = NFA.Node.save offset state') : pushNext σ nfa wf startPos stack update state pos = { update := σ.write update offset pos.current, state := ⟨state', ⋯⟩, pos := pos } :: stack

theorem Regex.Backtracker.captureNextAux.pushNext.anchor_pos {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {a : Data.Anchor} {state' : Nat} (hn : nfa[state] = NFA.Node.anchor a state') (h : Data.Anchor.test pos.current a = true) : pushNext σ nfa wf startPos stack update state pos = { update := update, state := ⟨state', ⋯⟩, pos := pos } :: stack

theorem Regex.Backtracker.captureNextAux.pushNext.anchor_neg {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {a : Data.Anchor} {state' : Nat} (hn : nfa[state] = NFA.Node.anchor a state') (h : ¬Data.Anchor.test pos.current a = true) : pushNext σ nfa wf startPos stack update state pos = stack

theorem Regex.Backtracker.captureNextAux.pushNext.char_pos {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {c : Char} {state' : Nat} (hn : nfa[state] = NFA.Node.char c state') (h : pos ≠ s.endBVPos startPos) (hc : pos.get h = c) : pushNext σ nfa wf startPos stack update state pos = { update := update, state := ⟨state', ⋯⟩, pos := pos.next h } :: stack

theorem Regex.Backtracker.captureNextAux.pushNext.char_neg {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {c : Char} {state' : Nat} (hn : nfa[state] = NFA.Node.char c state') (h : pos = s.endBVPos startPos ∨ ∃ (ne : pos ≠ s.endBVPos startPos), pos.get ne ≠ c) : pushNext σ nfa wf startPos stack update state pos = stack

theorem Regex.Backtracker.captureNextAux.pushNext.sparse_pos {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {cs : Data.Classes} {state' : Nat} (hn : nfa[state] = NFA.Node.sparse cs state') (h : pos ≠ s.endBVPos startPos) (hc : pos.get h ∈ cs) : pushNext σ nfa wf startPos stack update state pos = { update := update, state := ⟨state', ⋯⟩, pos := pos.next h } :: stack

theorem Regex.Backtracker.captureNextAux.pushNext.sparse_neg {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {stack : List (StackEntry σ nfa startPos)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {cs : Data.Classes} {state' : Nat} (hn : nfa[state] = NFA.Node.sparse cs state') (h : pos = s.endBVPos startPos ∨ ∃ (ne : pos ≠ s.endBVPos startPos), ¬pos.get ne ∈ cs) : pushNext σ nfa wf startPos stack update state pos = stack

theorem Regex.Backtracker.captureNextAux.pushNext.fun_cases' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : s.ValidPos) {motive : List (StackEntry σ nfa startPos) → σ.Update → Fin nfa.nodes.size → Data.BVPos startPos → Prop} (done : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos), nfa[state] = NFA.Node.done → motive stack update state pos) (fail : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos), nfa[state] = NFA.Node.fail → motive stack update state pos) (epsilon : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (state' : Fin nfa.nodes.size), nfa[state] = NFA.Node.epsilon ↑state' → motive stack update state pos) (split : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (state₁ state₂ : Fin nfa.nodes.size), nfa[state] = NFA.Node.split ↑state₁ ↑state₂ → motive stack update state pos) (save : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (offset : Nat) (state' : Fin nfa.nodes.size), nfa[state] = NFA.Node.save offset ↑state' → motive stack update state pos) (anchor_pos : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (a : Data.Anchor) (state' : Fin nfa.nodes.size), nfa[state] = NFA.Node.anchor a ↑state' → Data.Anchor.test pos.current a = true → motive stack update state pos) (anchor_neg : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (a : Data.Anchor) (state' : Fin nfa.nodes.size), nfa[state] = NFA.Node.anchor a ↑state' → ¬Data.Anchor.test pos.current a = true → motive stack update state pos) (char_pos : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (c : Char) (state' : Fin nfa.nodes.size), nfa[state] = NFA.Node.char c ↑state' → ∀ (h : pos ≠ s.endBVPos startPos), pos.get h = c → motive stack update state pos) (char_neg : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (c : Char) (state' : Fin nfa.nodes.size), nfa[state] = NFA.Node.char c ↑state' → (pos = s.endBVPos startPos ∨ ∃ (ne : pos ≠ s.endBVPos startPos), pos.get ne ≠ c) → motive stack update state pos) (sparse_pos : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (cs : Data.Classes) (state' : Fin nfa.nodes.size), nfa[state] = NFA.Node.sparse cs ↑state' → ∀ (h : pos ≠ s.endBVPos startPos), pos.get h ∈ cs → motive stack update state pos) (sparse_neg : ∀ (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (cs : Data.Classes) (state' : Fin nfa.nodes.size), nfa[state] = NFA.Node.sparse cs ↑state' → (pos = s.endBVPos startPos ∨ ∃ (ne : pos ≠ s.endBVPos startPos), ¬pos.get ne ∈ cs) → motive stack update state pos) (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) : motive stack update state pos

theorem Regex.Backtracker.captureNextAux.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : s.ValidPos) (motive : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) → List (StackEntry σ nfa startPos) → Prop) (base : ∀ (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)), motive visited []) (visited : ∀ (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (stack' : List (StackEntry σ nfa startPos)), visited.get state pos.index = true → motive visited stack' → motive visited ({ update := update, state := state, pos := pos } :: stack')) (done : ∀ (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (stack' : List (StackEntry σ nfa startPos)), ¬visited.get state pos.index = true → nfa[state] = NFA.Node.done → motive visited ({ update := update, state := state, pos := pos } :: stack')) (next : ∀ (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) (stack' : List (StackEntry σ nfa startPos)), ¬visited.get state pos.index = true → nfa[state] ≠ NFA.Node.done → motive (visited.set state pos.index) (pushNext σ nfa wf startPos stack' update state pos) → motive visited ({ update := update, state := state, pos := pos } :: stack')) (visited✝ : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (stack : List (StackEntry σ nfa startPos)) : motive visited✝ stack

theorem Regex.Backtracker.captureNextAux_base {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} : captureNextAux σ nfa wf startPos visited [] = (none, visited)

theorem Regex.Backtracker.captureNextAux_visited {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {stack' : List (StackEntry σ nfa startPos)} (mem : visited.get state pos.index = true) : captureNextAux σ nfa wf startPos visited ({ update := update, state := state, pos := pos } :: stack') = captureNextAux σ nfa wf startPos visited stack'

theorem Regex.Backtracker.captureNextAux_done {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {stack' : List (StackEntry σ nfa startPos)} (mem : ¬visited.get state pos.index = true) (hn : nfa[state] = NFA.Node.done) : captureNextAux σ nfa wf startPos visited ({ update := update, state := state, pos := pos } :: stack') = (some update, visited.set state pos.index)

theorem Regex.Backtracker.captureNextAux_next {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {update : σ.Update} {state : Fin nfa.nodes.size} {pos : Data.BVPos startPos} {stack' : List (StackEntry σ nfa startPos)} (mem : ¬visited.get state pos.index = true) (hn : nfa[state] ≠ NFA.Node.done) : captureNextAux σ nfa wf startPos visited ({ update := update, state := state, pos := pos } :: stack') = captureNextAux σ nfa wf startPos (visited.set state pos.index) (captureNextAux.pushNext σ nfa wf startPos stack' update state pos)

theorem Regex.Backtracker.captureNext.go.induct' {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : s.ValidPos) (motive : Data.BVPos startPos → Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1) → Prop) (found : ∀ (pos : Data.BVPos startPos) (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (update : σ.Update) (visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)), captureNextAux σ nfa wf startPos visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, pos := pos }] = (some update, visited') → motive pos visited) (not_found_next : ∀ (pos : Data.BVPos startPos) (visited visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)), captureNextAux σ nfa wf startPos visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, pos := pos }] = (none, visited') → ∀ (h : pos ≠ s.endBVPos startPos), motive (pos.next h) visited' → motive pos visited) (not_found_end : ∀ (pos : Data.BVPos startPos) (visited visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)), captureNextAux σ nfa wf startPos visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, pos := pos }] = (none, visited') → ¬pos ≠ s.endBVPos startPos → motive pos visited) (pos : Data.BVPos startPos) (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : motive pos visited

theorem Regex.Backtracker.captureNext.go_found {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {pos : Data.BVPos startPos} {update : σ.Update} {visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} (h : captureNextAux σ nfa wf startPos visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, pos := pos }] = (some update, visited')) : go σ nfa wf startPos pos visited = some update

theorem Regex.Backtracker.captureNext.go_not_found_next {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {pos : Data.BVPos startPos} {visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} (h : captureNextAux σ nfa wf startPos visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, pos := pos }] = (none, visited')) (h' : pos ≠ s.endBVPos startPos) : go σ nfa wf startPos pos visited = go σ nfa wf startPos (pos.next h') visited'

theorem Regex.Backtracker.captureNext.go_not_found_end {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.ValidPos} {visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} {pos : Data.BVPos startPos} {visited' : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)} (h : captureNextAux σ nfa wf startPos visited [{ update := σ.empty, state := ⟨nfa.start, ⋯⟩, pos := pos }] = (none, visited')) (h' : ¬pos ≠ s.endBVPos startPos) : go σ nfa wf startPos pos visited = none