def power' (u : List (Fin 2)) (k : ℕ) : List (Fin 2)

Equations

• power' u k = Nat.recOn k [] fun (x : ℕ) (pow_ind : List (Fin 2)) => u ++ pow_ind

theorem power_length' (u : List (Fin 2)) (k : ℕ) : (power' u k).length = k * u.length

def nontrivial_power' (x : List (Fin 2)) : Prop

Equations

• nontrivial_power' x = ∃ (k : ℕ) (u : List (Fin 2)), 1 ≤ u.length ∧ x = power' u k.succ.succ

def c' : List (Fin 2)

Equations

• c' = [0, 0]

def primitive' (x : List (Fin 2)) : Prop

Equations

• primitive' x = ¬nontrivial_power' x

theorem short_primitive' (x : List (Fin 2)) (h : x.length ≤ 1) : primitive' x

theorem List_nil_primitive' : primitive' []

theorem singleton_primitive' : primitive' [0]

theorem repeat_is_power' {k : ℕ} : List.replicate k.succ.succ 0 = power' [0] k.succ.succ

theorem repeat_not_primitive' {k : ℕ} : nontrivial_power' (List.replicate k.succ.succ 0)

theorem List_nil_length : [].length = 0

theorem List_ne_nil (x : List (Fin 2)) (h : x.length ≠ 0) : x ≠ []

theorem middle_of_List_repeat {b : Fin 2} {v : List (Fin 2)} {u : List (Fin 2)} : List.replicate (u.length + v.length).succ 1 = u ++ b :: v → b = 1

theorem why_01n_is_primitive (u : List (Fin 2)) (v : List (Fin 2)) (a : Fin 2) (b : Fin 2) (h : 0 :: List.replicate (u.length + v.length).succ 1 = a :: u ++ b :: v) : a = 0 ∧ b = 1

theorem power_manipulations (l : ℕ) {u : List (Fin 2)} {v : List (Fin 2)} {a : Fin 2} (hv : u = a :: v) : power' u l.succ.succ = a :: v ++ a :: (v ++ power' u l)

theorem power_succ (l : ℕ) (u : List (Fin 2)) : (power' u l.succ.succ).length = (power' u l).length + u.length + u.length

theorem length_manipulations {k : ℕ} {l : ℕ} {u : List (Fin 2)} {v : List (Fin 2)} {a : Fin 2} (hv : u = a :: v) (hu2 : 0 :: List.replicate k.succ 1 = power' u l.succ.succ) : 0 :: List.replicate (v.length + (v ++ power' u l).length).succ 1 = a :: v ++ a :: (v ++ power' u l)

theorem primitive_words_of_length_two_or_more (k : ℕ) : ∃ (x : List (Fin 2)), x.length = k.succ.succ ∧ primitive' x

theorem succ_succ {n : ℕ} (h : n ≠ 0) (hn : n ≠ 1) : ∃ (k : ℕ), n = k.succ.succ

theorem primitive_words_of_every_length (n : ℕ) : ∃ (x : List (Fin 2)), x.length = n ∧ primitive' x