def Regex.NFA.CharStep {s : String} (nfa : NFA) (pos : s.ValidPos) (i j : Fin nfa.nodes.size) : Prop

Equations

• nfa.CharStep pos i j = ∃ (ne : pos ≠ s.endValidPos), nfa.Step 0 (↑i) pos (↑j) (pos.next ne) none

theorem Regex.NFA.CharStep.ne {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} (step : nfa.CharStep pos i j) : pos ≠ s.endValidPos

theorem Regex.NFA.CharStep.step {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} (step : nfa.CharStep pos i j) : nfa.Step 0 (↑i) pos (↑j) (pos.next ⋯) none

@[simp]

theorem Regex.NFA.CharStep.done {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} (hn : nfa[i] = Node.done) : nfa.CharStep pos i j ↔ False

@[simp]

theorem Regex.NFA.CharStep.fail {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} (hn : nfa[i] = Node.fail) : nfa.CharStep pos i j ↔ False

@[simp]

theorem Regex.NFA.CharStep.epsilon {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} {next : ℕ} (hn : nfa[i] = Node.epsilon next) : nfa.CharStep pos i j ↔ False

@[simp]

theorem Regex.NFA.CharStep.anchor {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} {anchor : Data.Anchor} {next : ℕ} (hn : nfa[i] = Node.anchor anchor next) : nfa.CharStep pos i j ↔ False

@[simp]

theorem Regex.NFA.CharStep.split {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} {next₁ next₂ : ℕ} (hn : nfa[i] = Node.split next₁ next₂) : nfa.CharStep pos i j ↔ False

@[simp]

theorem Regex.NFA.CharStep.save {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} {offset next : ℕ} (hn : nfa[i] = Node.save offset next) : nfa.CharStep pos i j ↔ False

@[simp]

theorem Regex.NFA.CharStep.char {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} {c : Char} {next : ℕ} (hn : nfa[i] = Node.char c next) : nfa.CharStep pos i j ↔ ∃ (ne : pos ≠ s.endValidPos), ↑j = next ∧ pos.get ne = c

@[simp]

theorem Regex.NFA.CharStep.sparse {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} {cs : Data.Classes} {next : ℕ} (hn : nfa[i] = Node.sparse cs next) : nfa.CharStep pos i j ↔ ∃ (ne : pos ≠ s.endValidPos), ↑j = next ∧ pos.get ne ∈ cs

theorem Regex.NFA.CharStep.char_or_sparse {s : String} {nfa : NFA} {pos : s.ValidPos} {i j : Fin nfa.nodes.size} (step : nfa.CharStep pos i j) : (∃ (c : Char) (next : ℕ), nfa[i] = Node.char c next) ∨ ∃ (cs : Data.Classes) (next : ℕ), nfa[i] = Node.sparse cs next