Abstrakt
A code X is not primitivity preserving if there is a primitive list w is an element of lists X whose concatenation is imprimitive. We formalize a full characterization of such codes in the binary case in the proof assistant Isabelle/HOL.
Part of the formalization, interesting on its own, is a description of {x, y}-interpretations of the square xx if |y| <= |x|. We also provide a formalized parametric solution of the related equation x(j) y(k) = z(l).