theorem Regex.NFA.ge_pushRegex_start {nfa : NFA} {next : ℕ} {e : Data.Expr} {result : NFA} (eq : nfa.pushRegex next e = result) : nfa.size ≤ result.start

theorem Regex.NFA.eq_or_ge_of_step_pushRegex {nfa : NFA} {next : ℕ} {e : Data.Expr} {result : NFA} {i j : ℕ} (eq : nfa.pushRegex next e = result) (h₁ : nfa.size ≤ i) (h₂ : i < result.size) (step : (∃ (c : Char), j ∈ result[i].charStep c) ∨ j ∈ result[i].εStep) : j = next ∨ nfa.size ≤ j

theorem Regex.NFA.mem_save_of_mem_tags_pushRegex {nfa : NFA} {next : ℕ} {e : Data.Expr} {tag : ℕ} (h : tag ∈ e.tags) : ∃ (i : Fin (nfa.pushRegex next e).size) (offset : ℕ), (nfa.pushRegex next e)[i] = Node.save (2 * tag + 1) offset

theorem Regex.NFA.mem_save_of_mem_tags_compile {e : Data.Expr} {tag : ℕ} (h : tag ∈ e.tags) : ∃ (i : Fin (compile e).size) (offset : ℕ), (compile e)[i] = Node.save (2 * tag + 1) offset

theorem Regex.NFA.lt_of_mem_tags_compile {e : Data.Expr} {tag : ℕ} (h : tag ∈ e.tags) : 2 * tag < (compile e).maxTag

theorem Regex.NFA.ne_done_of_pushRegex_ge {nfa : NFA} {next : ℕ} {e : Data.Expr} (i : ℕ) (h₁ : nfa.size ≤ i) (h₂ : i < (nfa.pushRegex next e).size) : (nfa.pushRegex next e)[i] ≠ Node.done

theorem Regex.NFA.done_iff_zero_compile {e : Data.Expr} (i : ℕ) (h : i < (compile e).size) : (compile e)[i] = Node.done ↔ i = 0

theorem Regex.NFA.lt_zero_size_compile {e : Data.Expr} : 0 < (compile e).size

theorem Regex.NFA.lt_zero_start_compile {e : Data.Expr} : 0 < (compile e).start