theorem Regex.NFA.Step.eq_or_lt_of_pushNode {s : String} {nfa : NFA} {lb : ℕ} {pos pos' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {node : Node} (step : (nfa.pushNode node).Step lb i pos j pos' update) : i = nfa.size ∨ i < nfa.size ∧ nfa.Step lb i pos j pos' update

theorem Regex.NFA.Step.eq_or_lt_of_pushRegex {s : String} {nfa : NFA} {next : ℕ} {e : Data.Expr} {lb : ℕ} {pos pos' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (step : (nfa.pushRegex next e).Step lb i pos j pos' update) : nfa.size ≤ i ∨ i < nfa.size ∧ nfa.Step lb i pos j pos' update

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

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

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