theorem Regex.NFA.Step.eq_or_lt_of_pushNode {s : String} {nfa : NFA} {lb : ℕ} {pos pos' : s.ValidPos} {i j : ℕ} {update : Option (ℕ × s.ValidPos)} {node : Node} (step : (nfa.pushNode node).Step lb i pos j pos' update) : i = nfa.nodes.size ∨ i < nfa.nodes.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.ValidPos} {i j : ℕ} {update : Option (ℕ × s.ValidPos)} (step : (nfa.pushRegex next e).Step lb i pos j pos' update) : nfa.nodes.size ≤ i ∨ i < nfa.nodes.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.ValidPos} {i j : ℕ} {update : Option (ℕ × s.ValidPos)} (step : (nfa.pushRegex next e).Step nfa.nodes.size i pos j pos' update) : j = next ∨ nfa.nodes.size ≤ j

theorem Regex.NFA.Path.eq_or_path_next {s : String} {nfa : NFA} {next : ℕ} {e : Data.Expr} {result : NFA} {lb : ℕ} {pos pos' : s.ValidPos} {i j : ℕ} {update : List (ℕ × s.ValidPos)} (eq : nfa.pushRegex next e = result) (jlt : j < nfa.nodes.size) (ige : i ≥ nfa.nodes.size) (path : result.Path lb i pos j pos' update) : j = next ∨ ∃ (posm : s.ValidPos) (update₁ : List (ℕ × s.ValidPos)) (update₂ : List (ℕ × s.ValidPos)), update = update₁ ++ update₂ ∧ result.Path nfa.nodes.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.ValidPos} {i j : ℕ} {update : List (ℕ × s.ValidPos)} (eq : nfa.pushRegex next e = result) (jlt : j < nfa.nodes.size) (ige : i ≥ nfa.nodes.size) (ne : j ≠ next) (path : result.Path lb i pos j pos' update) : ∃ (posm : s.ValidPos) (update₁ : List (ℕ × s.ValidPos)) (update₂ : List (ℕ × s.ValidPos)), update = update₁ ++ update₂ ∧ result.Path nfa.nodes.size i pos next posm update₁ ∧ result.Path lb next posm j pos' update₂