def Regex.NFA.εStep' (nfa : NFA) (it : String.Iterator) (i j : Fin nfa.nodes.size) (update : Option (ℕ × String.Pos)) : Prop

Equations

• nfa.εStep' it i j update = nfa.Step 0 (↑i) it (↑j) it update

theorem Regex.NFA.εStep'.done {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} (hn : nfa[i] = Node.done) : nfa.εStep' it i j update ↔ False

theorem Regex.NFA.εStep'.fail {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} (hn : nfa[i] = Node.fail) : nfa.εStep' it i j update ↔ False

theorem Regex.NFA.εStep'.epsilon {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} {next : ℕ} (hn : nfa[i] = Node.epsilon next) : nfa.εStep' it i j update ↔ ↑j = next ∧ update = none ∧ it.Valid

theorem Regex.NFA.εStep'.anchor {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} {anchor : Data.Anchor} {next : ℕ} (hn : nfa[i] = Node.anchor anchor next) : nfa.εStep' it i j update ↔ ↑j = next ∧ update = none ∧ it.Valid ∧ Data.Anchor.test it anchor = true

theorem Regex.NFA.εStep'.split {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} {next₁ next₂ : ℕ} (hn : nfa[i] = Node.split next₁ next₂) : nfa.εStep' it i j update ↔ (↑j = next₁ ∨ ↑j = next₂) ∧ update = none ∧ it.Valid

theorem Regex.NFA.εStep'.save {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} {offset next : ℕ} (hn : nfa[i] = Node.save offset next) : nfa.εStep' it i j update ↔ ↑j = next ∧ update = some (offset, it.pos) ∧ it.Valid

theorem Regex.NFA.εStep'.char {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} {c : Char} {next : ℕ} (hn : nfa[i] = Node.char c next) : nfa.εStep' it i j update ↔ False

theorem Regex.NFA.εStep'.sparse {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} {cs : Data.Classes} {next : ℕ} (hn : nfa[i] = Node.sparse cs next) : nfa.εStep' it i j update ↔ False

theorem Regex.NFA.εStep'.valid {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} (step : nfa.εStep' it i j update) : it.Valid

inductive Regex.NFA.εClosure' (nfa : NFA) (it : String.Iterator) : Fin nfa.nodes.size → Fin nfa.nodes.size → List (ℕ × String.Pos) → Prop

• base {nfa : NFA} {it : String.Iterator} {i : Fin nfa.nodes.size} (v : it.Valid) : nfa.εClosure' it i i []
• step {nfa : NFA} {it : String.Iterator} {i j k : Fin nfa.nodes.size} {update₁ : Option (ℕ × String.Pos)} {update₂ : List (ℕ × String.Pos)} (step : nfa.εStep' it i j update₁) (rest : nfa.εClosure' it j k update₂) : nfa.εClosure' it i k (update₁ ::ₒ update₂)

theorem Regex.NFA.εClosure'.single {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {update : Option (ℕ × String.Pos)} (step : nfa.εStep' it i j update) : nfa.εClosure' it i j (List.ofOption update)

theorem Regex.NFA.εClosure'.trans {nfa : NFA} {it : String.Iterator} {i j k : Fin nfa.nodes.size} {update₁ update₂ : List (ℕ × String.Pos)} (cls₁ : nfa.εClosure' it i j update₁) (cls₂ : nfa.εClosure' it j k update₂) : nfa.εClosure' it i k (update₁ ++ update₂)

theorem Regex.NFA.εClosure'.snoc {nfa : NFA} {it : String.Iterator} {i j k : Fin nfa.nodes.size} {update₁ : List (ℕ × String.Pos)} {update₂ : Option (ℕ × String.Pos)} (cls : nfa.εClosure' it i j update₁) (step : nfa.εStep' it j k update₂) : nfa.εClosure' it i k (update₁ ++ List.ofOption update₂)

theorem Regex.NFA.εClosure'_of_path {nfa : NFA} {i j : ℕ} {it it' : String.Iterator} {updates : List (ℕ × String.Pos)} (wf : nfa.WellFormed) (hit : it = it') (path : nfa.Path 0 i it j it' updates) : nfa.εClosure' it ⟨i, ⋯⟩ ⟨j, ⋯⟩ updates

theorem Regex.NFA.εClosure'_iff_path (nfa : NFA) (wf : nfa.WellFormed) (i j : Fin nfa.nodes.size) (it : String.Iterator) (updates : List (ℕ × String.Pos)) : nfa.εClosure' it i j updates ↔ i = j ∧ updates = [] ∧ it.Valid ∨ nfa.Path 0 (↑i) it (↑j) it updates

theorem Regex.NFA.εClosure'.valid {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {updates : List (ℕ × String.Pos)} (cls : nfa.εClosure' it i j updates) : it.Valid