论文标题
不保留原始性的二进制代码
Binary codes that do not preserve primitivity
论文作者
论文摘要
如果有原始列表$ {\ Mathbf w} \ in {\ tt Lists} x $的代码$ x $不能保留原始性。我们在证明助手isabelle/hol中在二进制案例中对此类代码进行正式表征。正式化的一部分，本身有趣，是$ \ {x，y \} $的描述 - 平方$ xx $的解释如果$ | y | \ leq | x | $。我们还提供了相关方程式的形式化参数解决方案$ x^jy^k = z^\ ell $。
A code $X$ is not primitivity preserving if there is a primitive list ${\mathbf w} \in {\tt 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| \leq |x|$. We also provide a formalized parametric solution of the related equation $x^jy^k = z^\ell$.
