We explore the Ziv-Lempel and Crochemore factorizations of some classical automatic sequences making an extensive use of the theorem prover Walnut.

翻译：我们借助定理证明器Walnut，对若干经典自动序列的Ziv-Lempel因子分解与Crochemore因子分解进行了深入探索。