New constructions for $3$-free and $3^+$-free binary morphisms

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.