theorem Regex.NFA.Compile.ProofData.Empty.not_step_start [Empty] {s : String} {lb : ℕ} {p p' : s.Pos} {j : ℕ} {update : Option (ℕ × s.Pos)} : ¬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.Pos} {j : ℕ} {update : List (ℕ × s.Pos)} : ¬nfa'.Path lb nfa'.start p j p' update

theorem Regex.NFA.Compile.ProofData.Epsilon.step_start_iff [Epsilon] {s : String} {p p' : s.Pos} {j : ℕ} {update : Option (ℕ × s.Pos)} : nfa'.Step nfa.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.Pos} {j : ℕ} {update : List (ℕ × s.Pos)} (next_lt : next < nfa.size) : nfa'.Path nfa.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.Pos} {j : ℕ} {update : Option (ℕ × s.Pos)} : nfa'.Step nfa.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.Pos} {j : ℕ} {update : List (ℕ × s.Pos)} (next_lt : next < nfa.size) : nfa'.Path nfa.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.Pos} {j : ℕ} {update : Option (ℕ × s.Pos)} : nfa'.Step nfa.size nfa'.start p j p' update ↔ j = next ∧ update = none ∧ ∃ (ne : p ≠ s.endPos), p' = p.next ne ∧ p.get ne = c

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

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

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

theorem Regex.NFA.Compile.ProofData.Group.step_start_iff [Group] {s : String} {p p' : s.Pos} {j : ℕ} {update : Option (ℕ × s.Pos)} : nfa'.Step nfa.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.Pos} {j : ℕ} {update : Option (ℕ × s.Pos)} : nfa'.Step nfa.size nfaClose.start p j p' update ↔ j = next ∧ p' = p ∧ update = some (2 * tag + 1, p)

theorem Regex.NFA.Compile.ProofData.Group.path_start_iff [Group] {s : String} {p p' : s.Pos} {update : List (ℕ × s.Pos)} (wf : nfa.WellFormed) (next_lt : next < nfa.size) : nfa'.Path nfa.size nfa'.start p next p' update ↔ ∃ (updates : List (ℕ × s.Pos)), update = (2 * tag, p) :: updates ++ [(2 * tag + 1, p')] ∧ nfaExpr.Path nfaClose.size nfaExpr.start p nfaClose.start p' updates

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

theorem Regex.NFA.Compile.ProofData.Alternate.path_start_iff [Alternate] {s : String} {p p' : s.Pos} {update : List (ℕ × s.Pos)} (wf : nfa.WellFormed) (next_lt : next < nfa.size) : nfa'.Path nfa.size nfa'.start p next p' update ↔ nfa₁.Path nfa.size nfa₁.start p next p' update ∨ nfa₂.Path nfa₁.size nfa₂.start p next p' update

theorem Regex.NFA.Compile.ProofData.Concat.path_start_iff [Concat] {s : String} {p p' : s.Pos} {update : List (ℕ × s.Pos)} (wf : nfa.WellFormed) (next_lt : next < nfa.size) : nfa'.Path nfa.size nfa'.start p next p' update ↔ ∃ (pm : s.Pos) (updates₁ : List (ℕ × s.Pos)) (updates₂ : List (ℕ × s.Pos)), update = updates₁ ++ updates₂ ∧ nfa'.Path nfa₂.size nfa'.start p nfa₂.start pm updates₁ ∧ nfa₂.Path nfa.size nfa₂.start pm next p' updates₂

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

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