def occurs_in {α : Type} (y : List α) (w : List α) : Prop

Equations

• occurs_in y w = ∃ (x : List α) (z : List α), w = x ++ y ++ z

def nonnil_occurs_squared_in {α : Type} (y : List α) (w : List α) : Prop

Equations

• nonnil_occurs_squared_in y w = (y ≠ [] ∧ occurs_in (y ++ y) w)

def pre_abstract_almost_square_free (a : Fin 2) (b : Fin 2) (w : List (Fin 2)) : Prop

Equations

• pre_abstract_almost_square_free a b w = ∀ (y : List (Fin 2)), nonnil_occurs_squared_in y w → y = [a] ∨ y = [b] ∨ y = [a, b]

def abstractAlmostSquareFree (w : List (Fin 2)) : Prop

Equations

• abstractAlmostSquareFree w = (pre_abstract_almost_square_free 0 1 w ∨ pre_abstract_almost_square_free 1 0 w)

def almostSquareFree (w : List (Fin 2)) : Prop

Equations

• almostSquareFree w = pre_abstract_almost_square_free 0 1 w

def abstract_almost_square_free (a : Fin 2) (b : Fin 2) : a ≠ b → List (Fin 2) → Prop

This is only interesting if a ≠ b so maybe that should be baked in.

Equations

• abstract_almost_square_free a b x w = ∀ (y : List (Fin 2)), nonnil_occurs_squared_in y w → y = [a] ∨ y = [b] ∨ y = [a, b]

def almost_square_free (w : List (Fin 2)) : Prop

Equations

• almost_square_free w = abstract_almost_square_free 0 1 almost_square_free.proof_2 w

def generalized_almost_square_free {α : Type} (w : List α) : Prop

Equations

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

theorem cons_ne_nil' {a : Fin 2} {b : Fin 2} {c : Fin 2} : [a, b] ≠ [c]

theorem eq_cons_ne_nil {a : Fin 2} {b : Fin 2} {c : Fin 2} {d : Fin 2} (hcd : [c, d] = [a] ∨ [c, d] = [b] ∨ [c, d] = [a, b]) (hdc : [d, c] = [a] ∨ [d, c] = [b] ∨ [d, c] = [a, b]) : a = b

theorem generalized (w : List (Fin 2)) (a : Fin 2) (b : Fin 2) (hab : a ≠ b) (hsqf : abstract_almost_square_free a b hab w) : generalized_almost_square_free w

def overlapfree (w : List (Fin 2)) : Prop

Equations

• overlapfree w = ∀ (y : List (Fin 2)) (a : Fin 2), ¬occurs_in (a :: y ++ a :: y ++ [a]) w

theorem cons_append_length {a : Fin 2} {b : Fin 2} {x : List (Fin 2)} {u : List (Fin 2)} {z : List (Fin 2)} : (x ++ (a :: b :: u ++ a :: b :: u) ++ z).length = x.length + u.length.succ.succ + u.length.succ.succ + z.length

theorem square_length_ge_four {x : List (Fin 2)} {z : List (Fin 2)} {u : List (Fin 2)} {a : Fin 2} {b : Fin 2} : (x ++ (a :: b :: u ++ a :: b :: u) ++ z).length ≥ 4

def ctrex : List (Fin 2)

Equations

• ctrex = [0, 0, 0]

theorem ctrex_ne {x : List (Fin 2)} {z : List (Fin 2)} {a : Fin 2} {b : Fin 2} : ctrex ≠ x ++ ([a, b] ++ [a, b]) ++ z