Lemma 9 in NUS paper 2025

The file Theorem1_49.lean combines the ring construction with the dead state completion. Here we try to separate them.

def ringδ {A : Type} {n : ℕ} (hn : n ≠ 0) (w : Fin n → A) : A → Fin n → Set (Fin n)

Equations

• ringδ hn w a q = if H : a = w q then {⟨(↑q + 1) % n, ⋯⟩} else ∅

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

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

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

Equations

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

theorem ringδ_uniqueWord {A : Type} {m : ℕ} {n : ℕ} (hn : n ≠ 0) (hm : m ≠ 0) (v : Fin m → A) (w : Fin n → A) {start : Fin n} {final : Fin n} (h : accepts_word_path (ringδ hn w) v start final (ringpath hn)) (i : Fin m) : v i = w ⟨↑i % n, ⋯⟩

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

Equations

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

theorem A_minus_bound₀'extendMod {A : Type} {n : ℕ} (hn : n ≠ 0) (w : Fin n → A) (m : ℕ) (hm : m ≠ 0) : A_minus_at_most (extendMod hn w m) n

This is Lemma 9 in NUS paper (even stronger since it is for A_minus).

def complet {A : Type} {Q : Type} (δ : A → Q → Set Q) : A → Option Q → Set (Option Q)

The non-state / one-state / dead-state / trash-state completion of δ.

Equations

• complet δ a o = if H₀ : o = none then {none} else if H₁ : δ a (o.get ⋯) = ∅ then {none} else some '' δ a (o.get ⋯)

theorem complet_card {A : Type} {Q : Type} [Fintype Q] {δ : A → Q → Set Q} (q : Q) (a : A) : Fintype.card ↑(complet δ a (some q)) = max (Fintype.card ↑(δ a q)) 1

theorem complet_extends_paths {A : Type} {Q : Type} {δ : A → Q → Set Q} {n : ℕ} {w : Fin n → A} {init : Q} {final : Q} {p : Fin (n + 1) → Q} (hδ : accepts_word_path δ w init final p) : accepts_word_path (complet δ) w (some init) (some final) fun (x : Fin (n + 1)) => some (p x)

theorem complet_conservative {A : Type} {Q : Type} {δ : A → Q → Set Q} {n : ℕ} {w : Fin n → A} {init : Q} {final : Q} {p : Fin (n + 1) → Q} (hδ : accepts_word_path (complet δ) w (some init) (some final) fun (x : Fin (n + 1)) => some (p x)) : accepts_word_path δ w init final p

theorem complet_preserves_unique_path' {A : Type} {Q : Type} {δ : A → Q → Set Q} {n : ℕ} {init : Q} {final : Q} {p : Fin (n + 1) → Q} {v : Fin n → A} (hv : ∀ (p' : Fin (n + 1) → Q), accepts_word_path δ v init final p' → p = p') (op' : Fin (n + 1) → Option Q) : accepts_word_path (complet δ) v (some init) (some final) op' → (fun (x : Fin (n + 1)) => some (p x)) = op'

theorem complet_preserves_unique {A : Type} {Q : Type} {δ : A → Q → Set Q} {n : ℕ} {w : Fin n → A} {init : Q} {final : Q} {p : Fin (n + 1) → Q} (hδ : ∀ (v : Fin n → A) (p' : Fin (n + 1) → Q), accepts_word_path δ v init final p' → p = p' ∧ w = v) (v : Fin n → A) (op' : Fin (n + 1) → Option Q) : accepts_word_path (complet δ) v (some init) (some final) op' → (fun (x : Fin (n + 1)) => some (p x)) = op' ∧ w = v

theorem complet_and {A : Type} {Q : Type} {δ : A → Q → Set Q} {n : ℕ} {w : Fin n → A} {init : Q} {final : Q} {p : Fin (n + 1) → Q} (hδ : accepts_word_path δ w init final p ∧ ∀ (v : Fin n → A) (p' : Fin (n + 1) → Q), accepts_word_path δ v init final p' → p = p' ∧ w = v) : (accepts_word_path (complet δ) w (some init) (some final) fun (x : Fin (n + 1)) => some (p x)) ∧ ∀ (v : Fin n → A) (op' : Fin (n + 1) → Option Q), accepts_word_path (complet δ) v (some init) (some final) op' → (fun (x : Fin (n + 1)) => some (p x)) = op' ∧ w = v

Silly, but used twice.

theorem none_state_completion' {q : ℕ} {A : Type} {n : ℕ} (w : Fin n → A) : A_N_at_most w q → A_N_tot_at_most w (q + 1)

theorem none_state_completion {q : ℕ} {A : Type} {n : ℕ} (w : Fin n → A) : A_minus_at_most w q → A_at_most w (q + 1)

Dead-state completion lemma.

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

This is the main result of Theorem1_49.lean with a more modular proof.