def squarefree {k : ℕ} (w : List.Vector (Fin 2) k) : Prop

Equations

• squarefree w = ∀ l < w.length, ∀ (v : List.Vector (Fin 2) l), ↑v ≠ [] → ¬↑v ++ ↑v <:+: ↑w

@[implicit_reducible]

instance instDecidableSquarefree (w : List.Vector (Fin 2) 4) : Decidable (squarefree w)

Equations

• instDecidableSquarefree w = w.length.decidableBallLT fun (n : ℕ) (x : n < w.length) => ∀ (v : List.Vector (Fin 2) n), ↑v ≠ [] → ¬↑v ++ ↑v <:+: ↑w