Preliminaries for Hyde's Theorem

theorem flipCast {t : ℕ} {k : ℕ} (h : ¬t < k + 1) : 2 * k + 1 - t < k + 1

If we are not yet half-way there, then if we started at the destination, we would not yet be half-way home.

theorem odd_tuples_aux {A : Type u_1} {k : ℕ} {w : Fin (2 * k + 1) → A} {v : Fin (2 * k + 1) → A} {i : Fin (2 * k + 1)} (g₀ : ¬↑i < k + 1) (g₆ : ⟨2 * k + 1 - ↑i, ⋯⟩ = Fin.last k) (h₂ : v i = w ⟨2 * k + 1 - ↑i, ⋯⟩ ∧ 2 * k + 1 - ↑i = 2 * k - ↑i ∨ v i = w ⟨2 * k + 1 - (2 * k + 1 - ↑i), ⋯⟩ ∧ 2 * k - ↑i + 1 = 2 * k + 1 - ↑i) : w i = v i

A strange auxiliary lemma about odd-length tuples.

theorem racecar {k : ℕ} {f : Fin (k + 1) → Fin (k + 1)} {a : Fin (k + 1)} {b : Fin (k + 1)} (h₀ : f a = b) (h : ∀ (s : Fin k), ↑(f s.succ) ≤ ↑(f s.castSucc) + 1) (s : ℕ) (hs : s + ↑a < k + 1) : ↑(f ⟨s + ↑a, hs⟩) ≤ s + ↑b

Discrete version of the Racecar Principle.

theorem exact_racecar {k : ℕ} {f : Fin (k + 1) → Fin (k + 1)} (h₀ : f 0 = 0) (hk : f (Fin.last k) = Fin.last k) (h : ∀ (s : Fin k), ↑(f s.succ) ≤ ↑(f s.castSucc) + 1) {a : Fin k} : f a.castSucc = a.castSucc

Bidirectional version of the Discrete Racecar Principle.

def accepts_word_path {Q : Type u_1} {A : Type u_2} {n : ℕ} (δ : A → Q → Set Q) (w : Fin n → A) (init : Q) (final : Q) (path : Fin (n + 1) → Q) : Prop

p is an accepting path for the word w in the NFA δ.

Equations

• accepts_word_path δ w init final path = (path 0 = init ∧ path (Fin.last n) = final ∧ ∀ (i : Fin n), path i.succ ∈ δ (w i) (path i.castSucc))

def accepts_path {Q : Type u_1} {A : Type u_2} {n : ℕ} (δ : A → Q → Set Q) (init : Q) (final : Q) (path : Fin (n + 1) → Q) : Prop

p is an accepting path for the NFA δ.

Equations

• accepts_path δ init final path = (path 0 = init ∧ path (Fin.last n) = final ∧ ∀ (i : Fin n), ∃ (a : A), path i.succ ∈ δ a (path i.castSucc))

theorem accepts_path_of_accepts_word_path {Q : Type u_1} {A : Type u_2} {n : ℕ} (δ : A → Q → Set Q) (w : Fin n → A) (init : Q) (final : Q) (path : Fin (n + 1) → Q) (h : accepts_word_path δ w init final path) : accepts_path δ init final path

If an NFA accepts a word along a path p, then p is an accepting path.

def A_N_at_most {A : Type u_1} {n : ℕ} (w : Fin n → A) (q : ℕ) : Prop

Nondeterministic automatic complexity, relational form.

Equations

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

def A_at_most {A : Type u_1} {n : ℕ} (w : Fin n → A) (q : ℕ) : Prop

Total automatic complexity, relational form.

Equations

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

def A_minus_at_most {A : Type u_1} {n : ℕ} (w : Fin n → A) (q : ℕ) : Prop

The incomplete deterministic automatic complexity A⁻.

Equations

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

def A_N_tot_at_most {A : Type u_1} {n : ℕ} (w : Fin n → A) (q : ℕ) : Prop

Total nondeterministic automatic complexity, relational form.

Equations

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

theorem A_N_ge_one {A : Type u_1} {n : ℕ} (w : Fin n → A) : ¬A_N_at_most w 0

A word cannot have complexity 0, because then there'd be no initial state.

theorem hyde_emp {A : Type u_1} (w : Fin 0 → A) : A_N_at_most w 1

The empty word has A_N at most 1. This version does not require the alphabet A to be nonempty, hence does not follow using restricting.

theorem restricting_construction {A : Type u_1} {Q : Type} {δ : A → Q → Set Q} {init : Q} {final : Q} {n : ℕ} {w₁ : Fin (n + 1) → A} {p₁ : Fin (n + 1 + 1) → Q} (h₁ : accepts_word_path δ w₁ init final p₁) {w₀ : Fin n → A} {p₀ : Fin (n + 1) → Q} (h₀ : accepts_word_path δ w₀ init (p₁ (Fin.last n).castSucc) p₀) : accepts_word_path δ (Fin.snoc w₀ (w₁ (Fin.last n))) init final (Fin.snoc p₀ (p₁ (Fin.last (n + 1))))

If an NFA accepts a word then by changing the final state we can also accept its prefixes.

theorem restricting {A : Type u_1} {n : ℕ} {q : ℕ} {w : Fin (n + 1) → A} (h : A_N_at_most w q) : A_N_at_most (Fin.init w) q

Subword inequality for A_N.

def A_Ne_at_most {A : Type} {n : ℕ} (w : Fin n → A) (q : ℕ) : Prop

The relation behind exact nondeterministic automatic complexity.

Equations

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

theorem A_Ne_le_A_N {A : Type} {n : ℕ} {q : ℕ} {w : Fin n → A} (h : A_N_at_most w q) : A_Ne_at_most w q

theorem A_N_le_A_minus {A : Type} {n : ℕ} {q : ℕ} {w : Fin n → A} (h : A_minus_at_most w q) : A_N_at_most w q

theorem A_Ne_le_A_minus {A : Type} {n : ℕ} {q : ℕ} {w : Fin n → A} (h : A_minus_at_most w q) : A_Ne_at_most w q

theorem A_minus_le_A {A : Type} {n : ℕ} {q : ℕ} {w : Fin n → A} (h : A_at_most w q) : A_minus_at_most w q

theorem A_Ne_le_A {A : Type} {n : ℕ} {q : ℕ} {w : Fin n → A} (h : A_at_most w q) : A_Ne_at_most w q