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

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

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

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

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

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

theorem Regex.NFA.Compile.ProofData.Char.step_start_iff [Char] {s : String} {p p' : s.ValidPos} {j : ℕ} {update : Option (ℕ × s.ValidPos)} : nfa'.Step nfa.nodes.size nfa'.start p j p' update ↔ j = next ∧ update = none ∧ ∃ (ne : p ≠ s.endValidPos), p' = p.next ne ∧ p.get ne = c

theorem Regex.NFA.Compile.ProofData.Char.path_start_iff [Char] {s : String} {p p' : s.ValidPos} {j : ℕ} {update : List (ℕ × s.ValidPos)} (next_lt : next < nfa.nodes.size) : nfa'.Path nfa.nodes.size nfa'.start p j p' update ↔ j = next ∧ update = [] ∧ ∃ (ne : p ≠ s.endValidPos), p' = p.next ne ∧ p.get ne = c

theorem Regex.NFA.Compile.ProofData.Classes.step_start_iff [Classes] {s : String} {p p' : s.ValidPos} {j : ℕ} {update : Option (ℕ × s.ValidPos)} : nfa'.Step nfa.nodes.size nfa'.start p j p' update ↔ j = next ∧ update = none ∧ ∃ (ne : p ≠ s.endValidPos), p' = p.next ne ∧ p.get ne ∈ cs

theorem Regex.NFA.Compile.ProofData.Classes.path_start_iff [Classes] {s : String} {p p' : s.ValidPos} {j : ℕ} {update : List (ℕ × s.ValidPos)} (next_lt : next < nfa.nodes.size) : nfa'.Path nfa.nodes.size nfa'.start p j p' update ↔ j = next ∧ update = [] ∧ ∃ (ne : p ≠ s.endValidPos), p' = p.next ne ∧ p.get ne ∈ cs

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

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

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

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