axiom u : ℕ

def α : Type

Equations

• α = Fin u

@[implicit_reducible]

noncomputable instance instDecidableEqα : DecidableEq α

Equations

• instDecidableEqα = Classical.decEq α

@[implicit_reducible]

noncomputable instance instDecidableEqFinOfNatNat_acmoi : DecidableEq (Fin 2)

Equations

• instDecidableEqFinOfNatNat_acmoi = Classical.decEq (Fin 2)

def q0 : Fin 2

Equations

• q0 = ⟨0, q0._proof_1⟩

def q1 : Fin 2

Equations

• q1 = ⟨1, q1._proof_1⟩

noncomputable def TwoState (z : α) : DFA α (Fin 2)

Equations

• TwoState z = { step := fun (q : Fin 2) (b : α) => if q = q0 then if b = z then q0 else q1 else q1, start := q0, accept := {q0} }

def uniquely_accepts {τ : Type} (M : DFA α τ) (s : List α) : Prop

Equations

• uniquely_accepts M s = ∀ (t : List α), t.length = s.length → (M.accepts t ↔ t = s)

def automatic_complexity_is_at_most : List α → ℕ → Prop

Equations

• automatic_complexity_is_at_most s k = ∃ (M : DFA α (Fin k)), uniquely_accepts M s

theorem q0_ne_q1 : q0 ≠ q1

theorem TwoState_stay_q0 {a z : α} (h : (TwoState z).eval [a] = q0) : a = z

theorem TwoState_stay_q1 (z : α) (x : List α) : (TwoState z).evalFrom q1 x = q1

theorem TwoState_accepts_repeat {z : α} {n : ℕ} : (TwoState z).eval (List.replicate n z) = q0

theorem either_or {a : Fin 2} (h : ↑a ≠ 1) : ↑a = 0

theorem either_or_strong {a : Fin 2} (not_zero : a ≠ q0) : a = q1

theorem TwoState_no_return_to_q0 {q : Fin 2} {z : α} {x : List α} (h : (TwoState z).evalFrom q x = q0) : q = q0

theorem TwoState_accepts_only_starts_z {a z : α} {y : List α} (hq0 : (TwoState z).eval (a :: y) = q0) : a = z

theorem TwoState_accepts_only_repeat {z : α} {x : List α} : (TwoState z).eval x = q0 → x = List.replicate x.length z

theorem complexity_of_repeat (z : α) (n : ℕ) : automatic_complexity_is_at_most (List.replicate n z) 2