theorem Regex.NFA.Compile.ProofData.Empty.not_step_start [Empty] {lb : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} : ¬nfa'.Step lb nfa'.start it j it' update

theorem Regex.NFA.Compile.ProofData.Empty.not_path_start [Empty] {lb : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : List (ℕ × String.Pos)} : ¬nfa'.Path lb nfa'.start it j it' update

theorem Regex.NFA.Compile.ProofData.Epsilon.step_start_iff [Epsilon] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} : nfa'.Step nfa.nodes.size nfa'.start it j it' update ↔ j = next ∧ it' = it ∧ update = none ∧ it.Valid

theorem Regex.NFA.Compile.ProofData.Epsilon.path_start_iff [Epsilon] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : List (ℕ × String.Pos)} (next_lt : next < nfa.nodes.size) : nfa'.Path nfa.nodes.size nfa'.start it j it' update ↔ j = next ∧ it' = it ∧ update = [] ∧ it.Valid

theorem Regex.NFA.Compile.ProofData.Anchor.step_start_iff [Anchor] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} : nfa'.Step nfa.nodes.size nfa'.start it j it' update ↔ j = next ∧ it' = it ∧ update = none ∧ it.Valid ∧ Data.Anchor.test it anchor = true

theorem Regex.NFA.Compile.ProofData.Anchor.path_start_iff [Anchor] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : List (ℕ × String.Pos)} (next_lt : next < nfa.nodes.size) : nfa'.Path nfa.nodes.size nfa'.start it j it' update ↔ j = next ∧ it' = it ∧ update = [] ∧ it.Valid ∧ Data.Anchor.test it anchor = true

theorem Regex.NFA.Compile.ProofData.Char.step_start_iff [Char] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} : nfa'.Step nfa.nodes.size nfa'.start it j it' update ↔ ∃ (l : List _root_.Char) (r : List _root_.Char), j = next ∧ it' = it.next ∧ update = none ∧ String.Iterator.ValidFor l (c :: r) it

theorem Regex.NFA.Compile.ProofData.Char.path_start_iff [Char] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : List (ℕ × String.Pos)} (next_lt : next < nfa.nodes.size) : nfa'.Path nfa.nodes.size nfa'.start it j it' update ↔ ∃ (l : List _root_.Char) (r : List _root_.Char), j = next ∧ it' = it.next ∧ update = [] ∧ String.Iterator.ValidFor l (c :: r) it

theorem Regex.NFA.Compile.ProofData.Classes.step_start_iff [Classes] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} : nfa'.Step nfa.nodes.size nfa'.start it j it' update ↔ ∃ (l : List _root_.Char) (c : _root_.Char) (r : List _root_.Char), j = next ∧ it' = it.next ∧ update = none ∧ String.Iterator.ValidFor l (c :: r) it ∧ c ∈ cs

theorem Regex.NFA.Compile.ProofData.Classes.path_start_iff [Classes] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : List (ℕ × String.Pos)} (next_lt : next < nfa.nodes.size) : nfa'.Path nfa.nodes.size nfa'.start it j it' update ↔ ∃ (l : List _root_.Char) (c : _root_.Char) (r : List _root_.Char), j = next ∧ it' = it.next ∧ update = [] ∧ String.Iterator.ValidFor l (c :: r) it ∧ c ∈ cs

theorem Regex.NFA.Compile.ProofData.Group.step_start_iff [Group] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} : nfa'.Step nfa.nodes.size nfa'.start it j it' update ↔ j = nfaExpr.start ∧ it' = it ∧ update = some (2 * tag, it.pos) ∧ it.Valid

theorem Regex.NFA.Compile.ProofData.Group.step_close_iff [Group] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} : nfa'.Step nfa.nodes.size nfaClose.start it j it' update ↔ j = next ∧ it' = it ∧ update = some (2 * tag + 1, it.pos) ∧ it.Valid

theorem Regex.NFA.Compile.ProofData.Alternate.step_start_iff [Alternate] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} : nfa'.Step nfa.nodes.size nfa'.start it j it' update ↔ (j = nfa₁.start ∨ j = nfa₂.start) ∧ it' = it ∧ update = none ∧ it.Valid

theorem Regex.NFA.Compile.ProofData.Star.step_start_iff [Star] {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} : nfa'.Step nfa.nodes.size nfa'.start it j it' update ↔ (j = nfaExpr.start ∨ j = next) ∧ it' = it ∧ update = none ∧ it.Valid