axiom alpha : ℕ

structure NA' (α σ : Type) : Type

• step : σ → α → Set σ
• start : σ
• accept : σ

@[implicit_reducible]

instance NA'.instInhabitedFinAlpha {σ : Type} [Inhabited σ] : Inhabited (NA' (Fin alpha) σ)

Equations

• NA'.instInhabitedFinAlpha = { default := { step := fun (x : σ) (x_1 : Fin alpha) => ∅, start := default, accept := default } }

def NA'.step_set {σ : Type} (M : NA' (Fin alpha) σ) (S : Set σ) (a : Fin alpha) : Set σ

Equations

• M.step_set S a = ⋃ s ∈ S, M.step s a

def NA'.eval_from {σ : Type} (M : NA' (Fin alpha) σ) (start : Set σ) : List (Fin alpha) → Set σ

Equations

• M.eval_from start = List.foldl M.step_set start

def NA'.eval {σ : Type} (M : NA' (Fin alpha) σ) : List (Fin alpha) → Set σ

Equations

• M.eval = M.eval_from {M.start}

def NA'.accepts {σ : Type} (M : NA' (Fin alpha) σ) : Language (Fin alpha)

Equations

• M.accepts x = (M.accept ∈ M.eval x)

theorem NA'.step_set_empty {σ : Type} (M : NA' (Fin alpha) σ) {a : Fin alpha} : M.step_set ∅ a = ∅

theorem eval.from_empty {σ : Type} (M : NA' (Fin alpha) σ) (y : List (Fin alpha)) : M.eval_from ∅ y = ∅

theorem eval.eval_from_subset {γ : Type} (M : NA' (Fin alpha) γ) (w : List (Fin alpha)) (S T : Set γ) : S ⊆ T → M.eval_from S w ⊆ M.eval_from T w

theorem eval.step_singleton {σ : Type} (M : NA' (Fin alpha) σ) (q : σ) (a : Fin alpha) : M.step_set {q} a = M.step q a

theorem eval.eval_from_set_cons {σ : Type} {M : NA' (Fin alpha) σ} {q : σ} {y : List (Fin alpha)} {F : Set σ} {a : Fin alpha} (h_given : ∃ r ∈ M.step_set F a, q ∈ M.eval_from {r} y) : ∃ s ∈ F, q ∈ M.eval_from {s} (a :: y)

theorem eval.singleton_member_of_set {σ : Type} {M : NA' (Fin alpha) σ} {q : σ} {l : List (Fin alpha)} (F : Set σ) : q ∈ M.eval_from F l → ∃ r ∈ F, q ∈ M.eval_from {r} l

theorem eval.set_of_singleton_member {σ : Type} {M : NA' (Fin alpha) σ} {q : σ} {l : List (Fin alpha)} {F : Set σ} (hsome : ∃ r ∈ F, q ∈ M.eval_from {r} l) : q ∈ M.eval_from F l

theorem eval.set_iff_singleton_member {σ : Type} {M : NA' (Fin alpha) σ} {q : σ} {l : List (Fin alpha)} (F : Set σ) : q ∈ M.eval_from F l ↔ ∃ r ∈ F, q ∈ M.eval_from {r} l

@[implicit_reducible]

instance my_sum_inst {δ : Type} [u : Fintype δ] : Fintype (Unit ⊕ δ)

Equations

• my_sum_inst = instFintypeSum Unit δ

@[implicit_reducible]

noncomputable instance instDecidableEqFinAlpha (a b : Fin alpha) : Decidable (a = b)

Equations

• instDecidableEqFinAlpha a b = Classical.dec (a = b)

def hd.trafo {δ : Type} : Fintype δ → (N : NA' (Fin alpha) δ) → (a : Fin alpha) → NA' (Fin alpha) (Unit ⊕ δ)

Equations

• One or more equations did not get rendered due to their size.

theorem hd.lift_to {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a : Fin alpha} {t : List (Fin alpha)} : have M := trafo u N a; ∀ (q1 q2 : δ), q2 ∈ N.eval_from {q1} t → Sum.inr q2 ∈ M.eval_from {Sum.inr q1} t

theorem hd.accept_self {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a : Fin alpha} {t : List (Fin alpha)} : N.accepts t → (trafo u N a).accepts (a :: t)

theorem hd.stay_old {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a b : Fin alpha} {q : δ} {q' : Unit ⊕ δ} : have M := trafo u N a; q' ∈ M.step_set {Sum.inr q} b → ∃ (q_ : δ), q' = Sum.inr q_

theorem hd.remove_step {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {q q_ : δ} {a b : Fin alpha} (hq1 : Sum.inr q_ ∈ (trafo u N a).step_set {Sum.inr q} b) : q_ ∈ N.step_set {q} b

theorem hd.remove_accept {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {q : δ} {a b : Fin alpha} {z : List (Fin alpha)} : (∃ q' ∈ (trafo u N a).step_set {Sum.inr q} b, (trafo u N a).accept ∈ (trafo u N a).eval_from {q'} z) → ∃ (q_ : δ), Sum.inr q_ ∈ (trafo u N a).step_set {Sum.inr q} b ∧ (trafo u N a).accept ∈ (trafo u N a).eval_from {Sum.inr q_} z

theorem hd.remove {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a : Fin alpha} {y : List (Fin alpha)} : have M := trafo u N a; ∀ (q : δ), M.accept ∈ M.eval_from {Sum.inr q} y → N.accept ∈ N.eval_from {q} y

theorem hd.accepts_only {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a : Fin alpha} {t : List (Fin alpha)} : (trafo u N a).accepts t → ∃ (s : List (Fin alpha)), t = a :: s ∧ N.accepts s

theorem hd.regex {δ : Type} {u : Fintype δ} {N : NA' (Fin alpha) δ} {a : Fin alpha} (t : List (Fin alpha)) : (trafo u N a).accepts t ↔ ∃ (s : List (Fin alpha)), t = a :: s ∧ N.accepts s

def accepts_exactly {δ : Type} (M : NA' (Fin alpha) δ) (x : List (Fin alpha)) : Prop

Equations

• accepts_exactly M x = ∀ (y : List (Fin alpha)), y.length = x.length → (M.accepts y ↔ y = x)

def A_N_word_bounded_by (x : List (Fin alpha)) (n : ℕ) : Prop

Equations

• A_N_word_bounded_by x n = ∃ (δ : Type) (u : Fintype δ), Fintype.elems.card ≤ n ∧ ∃ (M : NA' (Fin alpha) δ), accepts_exactly M x

theorem A_N_word_finite_prelim (x : List (Fin alpha)) : ∃ (δ : Type) (x_1 : Fintype δ) (M : NA' (Fin alpha) δ), accepts_exactly M x

theorem A_N_word_finite (x : List (Fin alpha)) : ∃ (n : ℕ), A_N_word_bounded_by x n

noncomputable def A_N_word : List (Fin alpha) → ℕ

Equations

• A_N_word x = Nat.find ⋯

theorem Fintype_card_sum_typesafe {δ : Type} {u : Fintype δ} : Fintype.elems.card = Fintype.card Unit + Fintype.elems.card

theorem autocomplex_bound_nil : ∃ (δ : Type) (u : Fintype δ), Fintype.elems.card ≤ [].length.succ ∧ ∃ (M : NA' (Fin alpha) δ), accepts_exactly M []

theorem A_N_word_nil_bound_length_succ : A_N_word [] ≤ 1

theorem nonempty_of_mem {α : Type} {a : α} {s : Finset α} : a ∈ s → s.Nonempty

theorem lower_bound (x : List (Fin alpha)) : 1 ≤ A_N_word x

theorem A_N_word_nil : A_N_word [] = 1

theorem accepts_exactly_hd {δ : Type} (N : NA' (Fin alpha) δ) (y : List (Fin alpha)) (a : Fin alpha) (u : Fintype δ) (hae : accepts_exactly N y) : have M := hd.trafo u N a; accepts_exactly M (a :: y)

theorem hd_card (δ : Type) (u : Fintype δ) : Fintype.elems.card = Fintype.elems.card.succ

theorem hd_card_my (δ : Type) (u : Fintype δ) : Fintype.elems.card = Fintype.elems.card.succ

theorem iterative_bound (x : List (Fin alpha)) (a : Fin alpha) : A_N_word (a :: x) ≤ (A_N_word x).succ

theorem subword_inequality (x y : List (Fin alpha)) : A_N_word (x ++ y) ≤ x.length + A_N_word y

theorem A_N_word_bound_length_succ' (x : List (Fin alpha)) : A_N_word x ≤ x.length.succ