theorem Regex.NFA.Step.eq_or_ge_of_pushRegex {nfa : NFA} {next : ℕ} {e : Data.Expr} {i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} (step : (nfa.pushRegex next e).Step nfa.nodes.size i it j it' update) : j = next ∨ nfa.nodes.size ≤ j

theorem Regex.NFA.Path.eq_or_path_next {nfa : NFA} {next : ℕ} {e : Data.Expr} {result : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : List (ℕ × String.Pos)} (eq : nfa.pushRegex next e = result) (jlt : j < nfa.nodes.size) (ige : i ≥ nfa.nodes.size) (path : result.Path lb i it j it' update) : j = next ∨ ∃ (itm : String.Iterator) (update₁ : List (ℕ × String.Pos)) (update₂ : List (ℕ × String.Pos)), update = update₁ ++ update₂ ∧ result.Path nfa.nodes.size i it next itm update₁ ∧ result.Path lb next itm j it' update₂

theorem Regex.NFA.Path.path_next_of_ne {nfa : NFA} {next : ℕ} {e : Data.Expr} {result : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : List (ℕ × String.Pos)} (eq : nfa.pushRegex next e = result) (jlt : j < nfa.nodes.size) (ige : i ≥ nfa.nodes.size) (ne : j ≠ next) (path : result.Path lb i it j it' update) : ∃ (itm : String.Iterator) (update₁ : List (ℕ × String.Pos)) (update₂ : List (ℕ × String.Pos)), update = update₁ ++ update₂ ∧ result.Path nfa.nodes.size i it next itm update₁ ∧ result.Path lb next itm j it' update₂