theorem Regex.NFA.pushRegex_get_lt {nfa : NFA} {next : ℕ} {e : Data.Expr} {nfa' : NFA} (eq : nfa.pushRegex next e = nfa') (i : ℕ) (h : i < nfa.nodes.size) : nfa'[i] = nfa[i]

theorem Regex.NFA.Compile.ProofData.Group.get_close_expr [Group] : nfaExpr[nfa.nodes.size] = Node.save (2 * tag + 1) next

theorem Regex.NFA.Compile.ProofData.Group.get_close [Group] : nfa'[nfa.nodes.size] = Node.save (2 * tag + 1) next

theorem Regex.NFA.Compile.ProofData.Group.get [Group] (i : ℕ) (h : i < nfa'.nodes.size) : if x : i < nfa.nodes.size then nfa'[i] = nfa[i] else if x : i = nfa.nodes.size then nfa'[i] = Node.save (2 * tag + 1) next else if x : i < nfaExpr.nodes.size then nfa'[i] = nfaExpr[i] else nfa'[i] = Node.save (2 * tag) nfaExpr.start

theorem Regex.NFA.Compile.ProofData.Group.get_lt_close [Group] {i : ℕ} (h : i < nfaClose.nodes.size) : nfa'[i] = nfaClose[i]

theorem Regex.NFA.Compile.ProofData.Alternate.get_lt₂ [Alternate] {i : ℕ} (h : i < nfa₂.nodes.size) : nfa'[i] = nfa₂[i]

theorem Regex.NFA.Compile.ProofData.Alternate.get_lt₁ [Alternate] {i : ℕ} (h : i < nfa₁.nodes.size) : nfa'[i] = nfa₁[i]

theorem Regex.NFA.Compile.ProofData.Alternate.get [Alternate] (i : ℕ) (h : i < nfa'.nodes.size) : if x : i < nfa.nodes.size then nfa'[i] = nfa[i] else if x : i < nfa₁.nodes.size then nfa'[i] = nfa₁[i] else if x : i < nfa₂.nodes.size then nfa'[i] = nfa₂[i] else nfa'[i] = Node.split nfa₁.start nfa₂.start

theorem Regex.NFA.Compile.ProofData.Concat.get_lt₂ [Concat] {i : ℕ} (h : i < nfa₂.nodes.size) : nfa'[i] = nfa₂[i]

theorem Regex.NFA.Compile.ProofData.Concat.get [Concat] (i : ℕ) (h : i < nfa'.nodes.size) : if x : i < nfa.nodes.size then nfa'[i] = nfa[i] else if x : i < nfa₂.nodes.size then nfa'[i] = nfa₂[i] else True

theorem Regex.NFA.Compile.ProofData.Star.get [Star] (i : ℕ) (h : i < nfa'.nodes.size) : if x : i < nfa.nodes.size then nfa'[i] = nfa[i] else if x : i = nfa.nodes.size then nfa'[i] = Node.split nfaExpr.start next else nfa'[i] = nfaExpr[i]

theorem Regex.NFA.ge_pushRegex_start {nfa : NFA} {next : ℕ} {e : Data.Expr} {result : NFA} (eq : nfa.pushRegex next e = result) : nfa.nodes.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.nodes.size ≤ i) (h₂ : i < result.nodes.size) (step : (∃ (c : Char), j ∈ result[i].charStep c) ∨ j ∈ result[i].εStep) : j = next ∨ nfa.nodes.size ≤ j

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

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

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

theorem Regex.NFA.done_iff_zero_pushRegex {nfa : NFA} {next : ℕ} {e : Data.Expr} {result : NFA} (eq : nfa.pushRegex next e = result) (h₁ : 0 < nfa.nodes.size) (h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) (i : ℕ) (isLt : i < result.nodes.size) : result[i] = Node.done ↔ i = 0

theorem Regex.NFA.done_iff_zero_compile {e : Data.Expr} {nfa : NFA} (eq : compile e = nfa) (i : Fin nfa.nodes.size) : nfa[i] = Node.done ↔ ↑i = 0

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

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