def Regex.NFA.εStep' {s : String} (nfa : NFA) (pos : s.ValidPos) (i j : Fin nfa.nodes.size) (update : Option (ℕ × s.ValidPos)) : Prop

Equations

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

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

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

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

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

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

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

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

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

inductive Regex.NFA.εClosure' {s : String} (nfa : NFA) (pos : s.ValidPos) : Fin nfa.nodes.size → Fin nfa.nodes.size → List (ℕ × s.ValidPos) → Prop

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

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

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

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

theorem Regex.NFA.εClosure'_of_path {nfa : NFA} {s : String} {pos : s.ValidPos} {i j : ℕ} {pos' : s.ValidPos} {updates : List (ℕ × s.ValidPos)} (wf : nfa.WellFormed) (hpos : pos = pos') (path : nfa.Path 0 i pos j pos' updates) : nfa.εClosure' pos ⟨i, ⋯⟩ ⟨j, ⋯⟩ updates

theorem Regex.NFA.εClosure'_iff_path {s : String} (nfa : NFA) (wf : nfa.WellFormed) (i j : Fin nfa.nodes.size) (pos : s.ValidPos) (updates : List (ℕ × s.ValidPos)) : nfa.εClosure' pos i j updates ↔ i = j ∧ updates = [] ∨ nfa.Path 0 (↑i) pos (↑j) pos updates