We show that, for all $k\geq 1$, there exists a $k$-uniform $3^+$-free binary morphism. Furthermore, we revisit an old result of Currie and Rampersad on $3$-free binary morphisms and reprove it in a conceptually simpler (but computationally more intensive) way. Our proofs use the theorem-prover Walnut as an essential tool.

翻译：我们证明，对于所有$k\geq 1$，存在一个$k$均等的$3^+$自由二元态射。此外，我们重新审视了Currie和Rampersad关于$3$自由二元态射的一项早期结果，并以一种概念上更简单（但计算量更大）的方式对其进行了再证明。我们的证明将定理证明器Walnut作为关键工具。