inductive Regex.Backtracker.Path {s : String} (nfa : NFA) (wf : nfa.WellFormed) (pos : s.Pos) : s.Pos → Fin nfa.nodes.size → List (ℕ × s.Pos) → Prop

• init {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos : s.Pos} : Path nfa wf pos pos ⟨nfa.start, ⋯⟩ []
• more {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos : s.Pos} {i j : Fin nfa.nodes.size} {pos' pos'' : s.Pos} {update₁ : List (ℕ × s.Pos)} {update₂ : Option (ℕ × s.Pos)} {update₃ : List (ℕ × s.Pos)} (prev : Path nfa wf pos pos' i update₁) (step : nfa.Step 0 (↑i) pos' (↑j) pos'' update₂) (equpdate : update₃ = update₁ ++ List.ofOption update₂) : Path nfa wf pos pos'' j update₃

theorem Regex.Backtracker.Path.le {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' : s.Pos} {i : Fin nfa.nodes.size} {update : List (ℕ × s.Pos)} (path : Path nfa wf pos pos' i update) : pos ≤ pos'

theorem Regex.Backtracker.Path.eq_or_nfaPath {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' : s.Pos} {i : Fin nfa.nodes.size} {update : List (ℕ × s.Pos)} (path : Path nfa wf pos pos' i update) : pos' = pos ∧ ↑i = nfa.start ∧ update = [] ∨ nfa.Path 0 nfa.start pos (↑i) pos' update

theorem Regex.Backtracker.Path.nfaPath_of_ne {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' : s.Pos} {i : Fin nfa.nodes.size} {update : List (ℕ × s.Pos)} (path : Path nfa wf pos pos' i update) (ne : ↑i ≠ nfa.start) : nfa.Path 0 nfa.start pos (↑i) pos' update

theorem Regex.Backtracker.Path.concat_nfaPath {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' pos'' : s.Pos} {update₁ update₂ update₃ : List (ℕ × s.Pos)} {i j : ℕ} (isLt : i < nfa.nodes.size) (path₁ : Path nfa wf pos pos' ⟨i, isLt⟩ update₁) (path₂ : nfa.Path 0 i pos' j pos'' update₂) (equpdate : update₃ = update₁ ++ update₂) : Path nfa wf pos pos'' ⟨j, ⋯⟩ update₃

theorem Regex.Backtracker.Path.of_nfaPath {s : String} {nfa : NFA} {wf : nfa.WellFormed} {pos pos' : s.Pos} {update : List (ℕ × s.Pos)} {i : ℕ} (path : nfa.Path 0 nfa.start pos i pos' update) : Path nfa wf pos pos' ⟨i, ⋯⟩ update

def Regex.Backtracker.Path.bvpos' {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : s.Pos} {bvpos : Data.BVPos startPos} {pos' : s.Pos} {i : Fin nfa.nodes.size} {update : List (ℕ × s.Pos)} (path : Path nfa wf bvpos.current pos' i update) : Data.BVPos startPos

Equations

• path.bvpos' = { current := pos', le := ⋯ }