Theorem 1.49 in ACMOI

def ringδ' {A : Type} {n : ℕ} (w : Fin n → A) : A → Fin (n + 1) → Set (Fin (n + 1))

Equations

• ringδ' w a q = if H₀ : ↑q < n then if H₁ : a = w ⟨↑q, H₀⟩ then {⟨(↑q + 1) % n, ⋯⟩} else {Fin.last n} else {Fin.last n}

theorem deadRingδ₀ {A : Type} {m : ℕ} {n : ℕ} (v : Fin m → A) (w : Fin n → A) (p : Fin (m + 1) → Fin (n + 1)) {final : Fin (n + 1)} (h : accepts_word_path (ringδ' w) v 0 final p) (t : Fin m) (ht : p t.castSucc = Fin.last n) : p t.succ = Fin.last n

theorem deadRingδ₂ {A : Type} {m : ℕ} {n : ℕ} (v : Fin m → A) (w : Fin n → A) (p : Fin (m + 1) → Fin (n + 1)) {final : Fin (n + 1)} (h : accepts_word_path (ringδ' w) v 0 final p) (t : Fin (m + 1)) (ht : p t = Fin.last n) (s : Fin (m + 1)) (hs : ↑t ≤ ↑s) : p s = Fin.last n

theorem deadRingδ₁ {A : Type} {m : ℕ} {n : ℕ} (v : Fin m → A) (w : Fin n → A) (p : Fin (m + 1) → Fin (n + 1)) {final : Fin (n + 1)} {hfinal : final ≠ Fin.last n} (h : accepts_word_path (ringδ' w) v 0 final p) (t : Fin (m + 1)) : p t ≠ Fin.last n

theorem ringPath'helper {n : ℕ} (t : Fin (n + 1)) : ↑t % n < n + 1

theorem ringPathhelper {m : ℕ} {n : ℕ} (hn : n ≠ 0) (t : Fin (m + 1)) : ↑t % n < n + 1

theorem liveRingδ₁ {A : Type} {m : ℕ} {n : ℕ} (v : Fin m → A) (w : Fin n → A) (p : Fin (m + 1) → Fin (n + 1)) {final : Fin (n + 1)} {hfinal : final ≠ Fin.last n} (h : accepts_word_path (ringδ' w) v 0 final p) (t : Fin (m + 1)) : p t = ⟨↑t % n, ⋯⟩

theorem liveRingδ₁' {A : Type} {n : ℕ} (w : Fin n → A) (v : Fin n → A) (p : Fin (n + 1) → Fin (n + 1)) {final : Fin (n + 1)} {hfinal : final ≠ Fin.last n} (h : accepts_word_path (ringδ' w) v 0 final p) (t : Fin (n + 1)) : t ≠ Fin.last n → p t = t

def ringPath' {n : ℕ} : Fin (n + 1) → Fin (n + 1)

A simpler construction of ringPath, although the proof that it makes sense is harder.

Equations

• ringPath' t = ⟨↑t % n, ⋯⟩

def ringPath {m : ℕ} {n : ℕ} (hn : n ≠ 0) : Fin (m + 1) → Fin (n + 1)

Equations

• ringPath hn t = ⟨↑t % n, ⋯⟩

theorem ringδ_unique_word {A : Type} {m : ℕ} {n : ℕ} (hn : n ≠ 0) (hm : m ≠ 0) (v : Fin m → A) (w : Fin n → A) {final : Fin (n + 1)} {hfinal : final ≠ Fin.last n} (h : accepts_word_path (ringδ' w) v 0 final (ringPath hn)) (i : Fin m) : v i = w ⟨↑i % n, ⋯⟩

theorem ringδ_unique_word' {A : Type} {n : ℕ} (w : Fin n → A) (v : Fin n → A) {final : Fin (n + 1)} {hfinal : final ≠ Fin.last n} (h : accepts_word_path (ringδ' w) v 0 final ringPath') : w = v

theorem A_bound₀'pow {A : Type} {n : ℕ} {e : ℕ} (hn : n ≠ 0) (he : e ≠ 0) (w : Fin n → A) : A_at_most (Fin.repeat e w) (n + 1)

A power of a word has low complexity.

theorem A_bound₀'square {A : Type} {n : ℕ} (hn : n ≠ 0) (w : Fin n → A) : A_at_most (Fin.append w w) (n + 1)

A square has low complexity.

theorem A_bound₀' {A : Type} {n : ℕ} (w : Fin n → A) : A_at_most w (n + 1)

theorem A_bounded {A : Type} {n : ℕ} (w : Fin n → A) : ∃ (q : ℕ), A_at_most w q

theorem A_minus_bounded {A : Type} {n : ℕ} (w : Fin n → A) : ∃ (q : ℕ), A_minus_at_most w q

noncomputable def A {A : Type} {n : ℕ} : (Fin n → A) → ℕ

Equations

• _root_.A w = Nat.find ⋯

noncomputable def A_minus {A : Type} {n : ℕ} : (Fin n → A) → ℕ

Equations

• A_minus w = Nat.find ⋯

def extend {A : Type} {n : ℕ} (hn : n ≠ 0) (w : Fin n → A) (m : ℕ) : Fin m → A

Equations

• extend hn w m i = w ⟨↑i % n, ⋯⟩

theorem A_bound₀'extend {A : Type} {n : ℕ} (hn : n ≠ 0) (w : Fin n → A) (m : ℕ) (hm : m ≠ 0) : A_at_most (extend hn w m) (n + 1)

Theorem 1.49 of ACMOI, in so many words. Also essentially Lemma 9 in "Maximal automatic complexity and context-free languages" although that was given for A_N.