MAYBE Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

begin(end(x0)) rewrite(end(x0))
begin(a12(x0)) rotate(cut(Ca12(guess(x0))))
begin(a13(x0)) rotate(cut(Ca13(guess(x0))))
begin(a14(x0)) rotate(cut(Ca14(guess(x0))))
begin(a15(x0)) rotate(cut(Ca15(guess(x0))))
begin(a16(x0)) rotate(cut(Ca16(guess(x0))))
begin(a23(x0)) rotate(cut(Ca23(guess(x0))))
begin(a24(x0)) rotate(cut(Ca24(guess(x0))))
begin(a25(x0)) rotate(cut(Ca25(guess(x0))))
begin(a26(x0)) rotate(cut(Ca26(guess(x0))))
begin(a34(x0)) rotate(cut(Ca34(guess(x0))))
begin(a35(x0)) rotate(cut(Ca35(guess(x0))))
begin(a36(x0)) rotate(cut(Ca36(guess(x0))))
begin(a45(x0)) rotate(cut(Ca45(guess(x0))))
begin(a46(x0)) rotate(cut(Ca46(guess(x0))))
begin(a56(x0)) rotate(cut(Ca56(guess(x0))))
guess(a12(x0)) Ca12(guess(x0))
guess(a13(x0)) Ca13(guess(x0))
guess(a14(x0)) Ca14(guess(x0))
guess(a15(x0)) Ca15(guess(x0))
guess(a16(x0)) Ca16(guess(x0))
guess(a23(x0)) Ca23(guess(x0))
guess(a24(x0)) Ca24(guess(x0))
guess(a25(x0)) Ca25(guess(x0))
guess(a26(x0)) Ca26(guess(x0))
guess(a34(x0)) Ca34(guess(x0))
guess(a35(x0)) Ca35(guess(x0))
guess(a36(x0)) Ca36(guess(x0))
guess(a45(x0)) Ca45(guess(x0))
guess(a46(x0)) Ca46(guess(x0))
guess(a56(x0)) Ca56(guess(x0))
guess(a12(x0)) moveleft(Ba12(wait(x0)))
guess(a13(x0)) moveleft(Ba13(wait(x0)))
guess(a14(x0)) moveleft(Ba14(wait(x0)))
guess(a15(x0)) moveleft(Ba15(wait(x0)))
guess(a16(x0)) moveleft(Ba16(wait(x0)))
guess(a23(x0)) moveleft(Ba23(wait(x0)))
guess(a24(x0)) moveleft(Ba24(wait(x0)))
guess(a25(x0)) moveleft(Ba25(wait(x0)))
guess(a26(x0)) moveleft(Ba26(wait(x0)))
guess(a34(x0)) moveleft(Ba34(wait(x0)))
guess(a35(x0)) moveleft(Ba35(wait(x0)))
guess(a36(x0)) moveleft(Ba36(wait(x0)))
guess(a45(x0)) moveleft(Ba45(wait(x0)))
guess(a46(x0)) moveleft(Ba46(wait(x0)))
guess(a56(x0)) moveleft(Ba56(wait(x0)))
guess(end(x0)) finish(end(x0))
Ca12(moveleft(Ba12(x0))) moveleft(Ba12(Aa12(x0)))
Ca13(moveleft(Ba12(x0))) moveleft(Ba12(Aa13(x0)))
Ca14(moveleft(Ba12(x0))) moveleft(Ba12(Aa14(x0)))
Ca15(moveleft(Ba12(x0))) moveleft(Ba12(Aa15(x0)))
Ca16(moveleft(Ba12(x0))) moveleft(Ba12(Aa16(x0)))
Ca23(moveleft(Ba12(x0))) moveleft(Ba12(Aa23(x0)))
Ca24(moveleft(Ba12(x0))) moveleft(Ba12(Aa24(x0)))
Ca25(moveleft(Ba12(x0))) moveleft(Ba12(Aa25(x0)))
Ca26(moveleft(Ba12(x0))) moveleft(Ba12(Aa26(x0)))
Ca34(moveleft(Ba12(x0))) moveleft(Ba12(Aa34(x0)))
Ca35(moveleft(Ba12(x0))) moveleft(Ba12(Aa35(x0)))
Ca36(moveleft(Ba12(x0))) moveleft(Ba12(Aa36(x0)))
Ca45(moveleft(Ba12(x0))) moveleft(Ba12(Aa45(x0)))
Ca46(moveleft(Ba12(x0))) moveleft(Ba12(Aa46(x0)))
Ca56(moveleft(Ba12(x0))) moveleft(Ba12(Aa56(x0)))
Ca12(moveleft(Ba13(x0))) moveleft(Ba13(Aa12(x0)))
Ca13(moveleft(Ba13(x0))) moveleft(Ba13(Aa13(x0)))
Ca14(moveleft(Ba13(x0))) moveleft(Ba13(Aa14(x0)))
Ca15(moveleft(Ba13(x0))) moveleft(Ba13(Aa15(x0)))
Ca16(moveleft(Ba13(x0))) moveleft(Ba13(Aa16(x0)))
Ca23(moveleft(Ba13(x0))) moveleft(Ba13(Aa23(x0)))
Ca24(moveleft(Ba13(x0))) moveleft(Ba13(Aa24(x0)))
Ca25(moveleft(Ba13(x0))) moveleft(Ba13(Aa25(x0)))
Ca26(moveleft(Ba13(x0))) moveleft(Ba13(Aa26(x0)))
Ca34(moveleft(Ba13(x0))) moveleft(Ba13(Aa34(x0)))
Ca35(moveleft(Ba13(x0))) moveleft(Ba13(Aa35(x0)))
Ca36(moveleft(Ba13(x0))) moveleft(Ba13(Aa36(x0)))
Ca45(moveleft(Ba13(x0))) moveleft(Ba13(Aa45(x0)))
Ca46(moveleft(Ba13(x0))) moveleft(Ba13(Aa46(x0)))
Ca56(moveleft(Ba13(x0))) moveleft(Ba13(Aa56(x0)))
Ca12(moveleft(Ba14(x0))) moveleft(Ba14(Aa12(x0)))
Ca13(moveleft(Ba14(x0))) moveleft(Ba14(Aa13(x0)))
Ca14(moveleft(Ba14(x0))) moveleft(Ba14(Aa14(x0)))
Ca15(moveleft(Ba14(x0))) moveleft(Ba14(Aa15(x0)))
Ca16(moveleft(Ba14(x0))) moveleft(Ba14(Aa16(x0)))
Ca23(moveleft(Ba14(x0))) moveleft(Ba14(Aa23(x0)))
Ca24(moveleft(Ba14(x0))) moveleft(Ba14(Aa24(x0)))
Ca25(moveleft(Ba14(x0))) moveleft(Ba14(Aa25(x0)))
Ca26(moveleft(Ba14(x0))) moveleft(Ba14(Aa26(x0)))
Ca34(moveleft(Ba14(x0))) moveleft(Ba14(Aa34(x0)))
Ca35(moveleft(Ba14(x0))) moveleft(Ba14(Aa35(x0)))
Ca36(moveleft(Ba14(x0))) moveleft(Ba14(Aa36(x0)))
Ca45(moveleft(Ba14(x0))) moveleft(Ba14(Aa45(x0)))
Ca46(moveleft(Ba14(x0))) moveleft(Ba14(Aa46(x0)))
Ca56(moveleft(Ba14(x0))) moveleft(Ba14(Aa56(x0)))
Ca12(moveleft(Ba15(x0))) moveleft(Ba15(Aa12(x0)))
Ca13(moveleft(Ba15(x0))) moveleft(Ba15(Aa13(x0)))
Ca14(moveleft(Ba15(x0))) moveleft(Ba15(Aa14(x0)))
Ca15(moveleft(Ba15(x0))) moveleft(Ba15(Aa15(x0)))
Ca16(moveleft(Ba15(x0))) moveleft(Ba15(Aa16(x0)))
Ca23(moveleft(Ba15(x0))) moveleft(Ba15(Aa23(x0)))
Ca24(moveleft(Ba15(x0))) moveleft(Ba15(Aa24(x0)))
Ca25(moveleft(Ba15(x0))) moveleft(Ba15(Aa25(x0)))
Ca26(moveleft(Ba15(x0))) moveleft(Ba15(Aa26(x0)))
Ca34(moveleft(Ba15(x0))) moveleft(Ba15(Aa34(x0)))
Ca35(moveleft(Ba15(x0))) moveleft(Ba15(Aa35(x0)))
Ca36(moveleft(Ba15(x0))) moveleft(Ba15(Aa36(x0)))
Ca45(moveleft(Ba15(x0))) moveleft(Ba15(Aa45(x0)))
Ca46(moveleft(Ba15(x0))) moveleft(Ba15(Aa46(x0)))
Ca56(moveleft(Ba15(x0))) moveleft(Ba15(Aa56(x0)))
Ca12(moveleft(Ba16(x0))) moveleft(Ba16(Aa12(x0)))
Ca13(moveleft(Ba16(x0))) moveleft(Ba16(Aa13(x0)))
Ca14(moveleft(Ba16(x0))) moveleft(Ba16(Aa14(x0)))
Ca15(moveleft(Ba16(x0))) moveleft(Ba16(Aa15(x0)))
Ca16(moveleft(Ba16(x0))) moveleft(Ba16(Aa16(x0)))
Ca23(moveleft(Ba16(x0))) moveleft(Ba16(Aa23(x0)))
Ca24(moveleft(Ba16(x0))) moveleft(Ba16(Aa24(x0)))
Ca25(moveleft(Ba16(x0))) moveleft(Ba16(Aa25(x0)))
Ca26(moveleft(Ba16(x0))) moveleft(Ba16(Aa26(x0)))
Ca34(moveleft(Ba16(x0))) moveleft(Ba16(Aa34(x0)))
Ca35(moveleft(Ba16(x0))) moveleft(Ba16(Aa35(x0)))
Ca36(moveleft(Ba16(x0))) moveleft(Ba16(Aa36(x0)))
Ca45(moveleft(Ba16(x0))) moveleft(Ba16(Aa45(x0)))
Ca46(moveleft(Ba16(x0))) moveleft(Ba16(Aa46(x0)))
Ca56(moveleft(Ba16(x0))) moveleft(Ba16(Aa56(x0)))
Ca12(moveleft(Ba23(x0))) moveleft(Ba23(Aa12(x0)))
Ca13(moveleft(Ba23(x0))) moveleft(Ba23(Aa13(x0)))
Ca14(moveleft(Ba23(x0))) moveleft(Ba23(Aa14(x0)))
Ca15(moveleft(Ba23(x0))) moveleft(Ba23(Aa15(x0)))
Ca16(moveleft(Ba23(x0))) moveleft(Ba23(Aa16(x0)))
Ca23(moveleft(Ba23(x0))) moveleft(Ba23(Aa23(x0)))
Ca24(moveleft(Ba23(x0))) moveleft(Ba23(Aa24(x0)))
Ca25(moveleft(Ba23(x0))) moveleft(Ba23(Aa25(x0)))
Ca26(moveleft(Ba23(x0))) moveleft(Ba23(Aa26(x0)))
Ca34(moveleft(Ba23(x0))) moveleft(Ba23(Aa34(x0)))
Ca35(moveleft(Ba23(x0))) moveleft(Ba23(Aa35(x0)))
Ca36(moveleft(Ba23(x0))) moveleft(Ba23(Aa36(x0)))
Ca45(moveleft(Ba23(x0))) moveleft(Ba23(Aa45(x0)))
Ca46(moveleft(Ba23(x0))) moveleft(Ba23(Aa46(x0)))
Ca56(moveleft(Ba23(x0))) moveleft(Ba23(Aa56(x0)))
Ca12(moveleft(Ba24(x0))) moveleft(Ba24(Aa12(x0)))
Ca13(moveleft(Ba24(x0))) moveleft(Ba24(Aa13(x0)))
Ca14(moveleft(Ba24(x0))) moveleft(Ba24(Aa14(x0)))
Ca15(moveleft(Ba24(x0))) moveleft(Ba24(Aa15(x0)))
Ca16(moveleft(Ba24(x0))) moveleft(Ba24(Aa16(x0)))
Ca23(moveleft(Ba24(x0))) moveleft(Ba24(Aa23(x0)))
Ca24(moveleft(Ba24(x0))) moveleft(Ba24(Aa24(x0)))
Ca25(moveleft(Ba24(x0))) moveleft(Ba24(Aa25(x0)))
Ca26(moveleft(Ba24(x0))) moveleft(Ba24(Aa26(x0)))
Ca34(moveleft(Ba24(x0))) moveleft(Ba24(Aa34(x0)))
Ca35(moveleft(Ba24(x0))) moveleft(Ba24(Aa35(x0)))
Ca36(moveleft(Ba24(x0))) moveleft(Ba24(Aa36(x0)))
Ca45(moveleft(Ba24(x0))) moveleft(Ba24(Aa45(x0)))
Ca46(moveleft(Ba24(x0))) moveleft(Ba24(Aa46(x0)))
Ca56(moveleft(Ba24(x0))) moveleft(Ba24(Aa56(x0)))
Ca12(moveleft(Ba25(x0))) moveleft(Ba25(Aa12(x0)))
Ca13(moveleft(Ba25(x0))) moveleft(Ba25(Aa13(x0)))
Ca14(moveleft(Ba25(x0))) moveleft(Ba25(Aa14(x0)))
Ca15(moveleft(Ba25(x0))) moveleft(Ba25(Aa15(x0)))
Ca16(moveleft(Ba25(x0))) moveleft(Ba25(Aa16(x0)))
Ca23(moveleft(Ba25(x0))) moveleft(Ba25(Aa23(x0)))
Ca24(moveleft(Ba25(x0))) moveleft(Ba25(Aa24(x0)))
Ca25(moveleft(Ba25(x0))) moveleft(Ba25(Aa25(x0)))
Ca26(moveleft(Ba25(x0))) moveleft(Ba25(Aa26(x0)))
Ca34(moveleft(Ba25(x0))) moveleft(Ba25(Aa34(x0)))
Ca35(moveleft(Ba25(x0))) moveleft(Ba25(Aa35(x0)))
Ca36(moveleft(Ba25(x0))) moveleft(Ba25(Aa36(x0)))
Ca45(moveleft(Ba25(x0))) moveleft(Ba25(Aa45(x0)))
Ca46(moveleft(Ba25(x0))) moveleft(Ba25(Aa46(x0)))
Ca56(moveleft(Ba25(x0))) moveleft(Ba25(Aa56(x0)))
Ca12(moveleft(Ba26(x0))) moveleft(Ba26(Aa12(x0)))
Ca13(moveleft(Ba26(x0))) moveleft(Ba26(Aa13(x0)))
Ca14(moveleft(Ba26(x0))) moveleft(Ba26(Aa14(x0)))
Ca15(moveleft(Ba26(x0))) moveleft(Ba26(Aa15(x0)))
Ca16(moveleft(Ba26(x0))) moveleft(Ba26(Aa16(x0)))
Ca23(moveleft(Ba26(x0))) moveleft(Ba26(Aa23(x0)))
Ca24(moveleft(Ba26(x0))) moveleft(Ba26(Aa24(x0)))
Ca25(moveleft(Ba26(x0))) moveleft(Ba26(Aa25(x0)))
Ca26(moveleft(Ba26(x0))) moveleft(Ba26(Aa26(x0)))
Ca34(moveleft(Ba26(x0))) moveleft(Ba26(Aa34(x0)))
Ca35(moveleft(Ba26(x0))) moveleft(Ba26(Aa35(x0)))
Ca36(moveleft(Ba26(x0))) moveleft(Ba26(Aa36(x0)))
Ca45(moveleft(Ba26(x0))) moveleft(Ba26(Aa45(x0)))
Ca46(moveleft(Ba26(x0))) moveleft(Ba26(Aa46(x0)))
Ca56(moveleft(Ba26(x0))) moveleft(Ba26(Aa56(x0)))
Ca12(moveleft(Ba34(x0))) moveleft(Ba34(Aa12(x0)))
Ca13(moveleft(Ba34(x0))) moveleft(Ba34(Aa13(x0)))
Ca14(moveleft(Ba34(x0))) moveleft(Ba34(Aa14(x0)))
Ca15(moveleft(Ba34(x0))) moveleft(Ba34(Aa15(x0)))
Ca16(moveleft(Ba34(x0))) moveleft(Ba34(Aa16(x0)))
Ca23(moveleft(Ba34(x0))) moveleft(Ba34(Aa23(x0)))
Ca24(moveleft(Ba34(x0))) moveleft(Ba34(Aa24(x0)))
Ca25(moveleft(Ba34(x0))) moveleft(Ba34(Aa25(x0)))
Ca26(moveleft(Ba34(x0))) moveleft(Ba34(Aa26(x0)))
Ca34(moveleft(Ba34(x0))) moveleft(Ba34(Aa34(x0)))
Ca35(moveleft(Ba34(x0))) moveleft(Ba34(Aa35(x0)))
Ca36(moveleft(Ba34(x0))) moveleft(Ba34(Aa36(x0)))
Ca45(moveleft(Ba34(x0))) moveleft(Ba34(Aa45(x0)))
Ca46(moveleft(Ba34(x0))) moveleft(Ba34(Aa46(x0)))
Ca56(moveleft(Ba34(x0))) moveleft(Ba34(Aa56(x0)))
Ca12(moveleft(Ba35(x0))) moveleft(Ba35(Aa12(x0)))
Ca13(moveleft(Ba35(x0))) moveleft(Ba35(Aa13(x0)))
Ca14(moveleft(Ba35(x0))) moveleft(Ba35(Aa14(x0)))
Ca15(moveleft(Ba35(x0))) moveleft(Ba35(Aa15(x0)))
Ca16(moveleft(Ba35(x0))) moveleft(Ba35(Aa16(x0)))
Ca23(moveleft(Ba35(x0))) moveleft(Ba35(Aa23(x0)))
Ca24(moveleft(Ba35(x0))) moveleft(Ba35(Aa24(x0)))
Ca25(moveleft(Ba35(x0))) moveleft(Ba35(Aa25(x0)))
Ca26(moveleft(Ba35(x0))) moveleft(Ba35(Aa26(x0)))
Ca34(moveleft(Ba35(x0))) moveleft(Ba35(Aa34(x0)))
Ca35(moveleft(Ba35(x0))) moveleft(Ba35(Aa35(x0)))
Ca36(moveleft(Ba35(x0))) moveleft(Ba35(Aa36(x0)))
Ca45(moveleft(Ba35(x0))) moveleft(Ba35(Aa45(x0)))
Ca46(moveleft(Ba35(x0))) moveleft(Ba35(Aa46(x0)))
Ca56(moveleft(Ba35(x0))) moveleft(Ba35(Aa56(x0)))
Ca12(moveleft(Ba36(x0))) moveleft(Ba36(Aa12(x0)))
Ca13(moveleft(Ba36(x0))) moveleft(Ba36(Aa13(x0)))
Ca14(moveleft(Ba36(x0))) moveleft(Ba36(Aa14(x0)))
Ca15(moveleft(Ba36(x0))) moveleft(Ba36(Aa15(x0)))
Ca16(moveleft(Ba36(x0))) moveleft(Ba36(Aa16(x0)))
Ca23(moveleft(Ba36(x0))) moveleft(Ba36(Aa23(x0)))
Ca24(moveleft(Ba36(x0))) moveleft(Ba36(Aa24(x0)))
Ca25(moveleft(Ba36(x0))) moveleft(Ba36(Aa25(x0)))
Ca26(moveleft(Ba36(x0))) moveleft(Ba36(Aa26(x0)))
Ca34(moveleft(Ba36(x0))) moveleft(Ba36(Aa34(x0)))
Ca35(moveleft(Ba36(x0))) moveleft(Ba36(Aa35(x0)))
Ca36(moveleft(Ba36(x0))) moveleft(Ba36(Aa36(x0)))
Ca45(moveleft(Ba36(x0))) moveleft(Ba36(Aa45(x0)))
Ca46(moveleft(Ba36(x0))) moveleft(Ba36(Aa46(x0)))
Ca56(moveleft(Ba36(x0))) moveleft(Ba36(Aa56(x0)))
Ca12(moveleft(Ba45(x0))) moveleft(Ba45(Aa12(x0)))
Ca13(moveleft(Ba45(x0))) moveleft(Ba45(Aa13(x0)))
Ca14(moveleft(Ba45(x0))) moveleft(Ba45(Aa14(x0)))
Ca15(moveleft(Ba45(x0))) moveleft(Ba45(Aa15(x0)))
Ca16(moveleft(Ba45(x0))) moveleft(Ba45(Aa16(x0)))
Ca23(moveleft(Ba45(x0))) moveleft(Ba45(Aa23(x0)))
Ca24(moveleft(Ba45(x0))) moveleft(Ba45(Aa24(x0)))
Ca25(moveleft(Ba45(x0))) moveleft(Ba45(Aa25(x0)))
Ca26(moveleft(Ba45(x0))) moveleft(Ba45(Aa26(x0)))
Ca34(moveleft(Ba45(x0))) moveleft(Ba45(Aa34(x0)))
Ca35(moveleft(Ba45(x0))) moveleft(Ba45(Aa35(x0)))
Ca36(moveleft(Ba45(x0))) moveleft(Ba45(Aa36(x0)))
Ca45(moveleft(Ba45(x0))) moveleft(Ba45(Aa45(x0)))
Ca46(moveleft(Ba45(x0))) moveleft(Ba45(Aa46(x0)))
Ca56(moveleft(Ba45(x0))) moveleft(Ba45(Aa56(x0)))
Ca12(moveleft(Ba46(x0))) moveleft(Ba46(Aa12(x0)))
Ca13(moveleft(Ba46(x0))) moveleft(Ba46(Aa13(x0)))
Ca14(moveleft(Ba46(x0))) moveleft(Ba46(Aa14(x0)))
Ca15(moveleft(Ba46(x0))) moveleft(Ba46(Aa15(x0)))
Ca16(moveleft(Ba46(x0))) moveleft(Ba46(Aa16(x0)))
Ca23(moveleft(Ba46(x0))) moveleft(Ba46(Aa23(x0)))
Ca24(moveleft(Ba46(x0))) moveleft(Ba46(Aa24(x0)))
Ca25(moveleft(Ba46(x0))) moveleft(Ba46(Aa25(x0)))
Ca26(moveleft(Ba46(x0))) moveleft(Ba46(Aa26(x0)))
Ca34(moveleft(Ba46(x0))) moveleft(Ba46(Aa34(x0)))
Ca35(moveleft(Ba46(x0))) moveleft(Ba46(Aa35(x0)))
Ca36(moveleft(Ba46(x0))) moveleft(Ba46(Aa36(x0)))
Ca45(moveleft(Ba46(x0))) moveleft(Ba46(Aa45(x0)))
Ca46(moveleft(Ba46(x0))) moveleft(Ba46(Aa46(x0)))
Ca56(moveleft(Ba46(x0))) moveleft(Ba46(Aa56(x0)))
Ca12(moveleft(Ba56(x0))) moveleft(Ba56(Aa12(x0)))
Ca13(moveleft(Ba56(x0))) moveleft(Ba56(Aa13(x0)))
Ca14(moveleft(Ba56(x0))) moveleft(Ba56(Aa14(x0)))
Ca15(moveleft(Ba56(x0))) moveleft(Ba56(Aa15(x0)))
Ca16(moveleft(Ba56(x0))) moveleft(Ba56(Aa16(x0)))
Ca23(moveleft(Ba56(x0))) moveleft(Ba56(Aa23(x0)))
Ca24(moveleft(Ba56(x0))) moveleft(Ba56(Aa24(x0)))
Ca25(moveleft(Ba56(x0))) moveleft(Ba56(Aa25(x0)))
Ca26(moveleft(Ba56(x0))) moveleft(Ba56(Aa26(x0)))
Ca34(moveleft(Ba56(x0))) moveleft(Ba56(Aa34(x0)))
Ca35(moveleft(Ba56(x0))) moveleft(Ba56(Aa35(x0)))
Ca36(moveleft(Ba56(x0))) moveleft(Ba56(Aa36(x0)))
Ca45(moveleft(Ba56(x0))) moveleft(Ba56(Aa45(x0)))
Ca46(moveleft(Ba56(x0))) moveleft(Ba56(Aa46(x0)))
Ca56(moveleft(Ba56(x0))) moveleft(Ba56(Aa56(x0)))
cut(moveleft(Ba12(x0))) Da12(cut(goright(x0)))
cut(moveleft(Ba13(x0))) Da13(cut(goright(x0)))
cut(moveleft(Ba14(x0))) Da14(cut(goright(x0)))
cut(moveleft(Ba15(x0))) Da15(cut(goright(x0)))
cut(moveleft(Ba16(x0))) Da16(cut(goright(x0)))
cut(moveleft(Ba23(x0))) Da23(cut(goright(x0)))
cut(moveleft(Ba24(x0))) Da24(cut(goright(x0)))
cut(moveleft(Ba25(x0))) Da25(cut(goright(x0)))
cut(moveleft(Ba26(x0))) Da26(cut(goright(x0)))
cut(moveleft(Ba34(x0))) Da34(cut(goright(x0)))
cut(moveleft(Ba35(x0))) Da35(cut(goright(x0)))
cut(moveleft(Ba36(x0))) Da36(cut(goright(x0)))
cut(moveleft(Ba45(x0))) Da45(cut(goright(x0)))
cut(moveleft(Ba46(x0))) Da46(cut(goright(x0)))
cut(moveleft(Ba56(x0))) Da56(cut(goright(x0)))
goright(Aa12(x0)) Ca12(goright(x0))
goright(Aa13(x0)) Ca13(goright(x0))
goright(Aa14(x0)) Ca14(goright(x0))
goright(Aa15(x0)) Ca15(goright(x0))
goright(Aa16(x0)) Ca16(goright(x0))
goright(Aa23(x0)) Ca23(goright(x0))
goright(Aa24(x0)) Ca24(goright(x0))
goright(Aa25(x0)) Ca25(goright(x0))
goright(Aa26(x0)) Ca26(goright(x0))
goright(Aa34(x0)) Ca34(goright(x0))
goright(Aa35(x0)) Ca35(goright(x0))
goright(Aa36(x0)) Ca36(goright(x0))
goright(Aa45(x0)) Ca45(goright(x0))
goright(Aa46(x0)) Ca46(goright(x0))
goright(Aa56(x0)) Ca56(goright(x0))
goright(wait(a12(x0))) moveleft(Ba12(wait(x0)))
goright(wait(a13(x0))) moveleft(Ba13(wait(x0)))
goright(wait(a14(x0))) moveleft(Ba14(wait(x0)))
goright(wait(a15(x0))) moveleft(Ba15(wait(x0)))
goright(wait(a16(x0))) moveleft(Ba16(wait(x0)))
goright(wait(a23(x0))) moveleft(Ba23(wait(x0)))
goright(wait(a24(x0))) moveleft(Ba24(wait(x0)))
goright(wait(a25(x0))) moveleft(Ba25(wait(x0)))
goright(wait(a26(x0))) moveleft(Ba26(wait(x0)))
goright(wait(a34(x0))) moveleft(Ba34(wait(x0)))
goright(wait(a35(x0))) moveleft(Ba35(wait(x0)))
goright(wait(a36(x0))) moveleft(Ba36(wait(x0)))
goright(wait(a45(x0))) moveleft(Ba45(wait(x0)))
goright(wait(a46(x0))) moveleft(Ba46(wait(x0)))
goright(wait(a56(x0))) moveleft(Ba56(wait(x0)))
goright(wait(end(x0))) finish(end(x0))
Ca12(finish(x0)) finish(a12(x0))
Ca13(finish(x0)) finish(a13(x0))
Ca14(finish(x0)) finish(a14(x0))
Ca15(finish(x0)) finish(a15(x0))
Ca16(finish(x0)) finish(a16(x0))
Ca23(finish(x0)) finish(a23(x0))
Ca24(finish(x0)) finish(a24(x0))
Ca25(finish(x0)) finish(a25(x0))
Ca26(finish(x0)) finish(a26(x0))
Ca34(finish(x0)) finish(a34(x0))
Ca35(finish(x0)) finish(a35(x0))
Ca36(finish(x0)) finish(a36(x0))
Ca45(finish(x0)) finish(a45(x0))
Ca46(finish(x0)) finish(a46(x0))
Ca56(finish(x0)) finish(a56(x0))
cut(finish(x0)) finish2(x0)
Da12(finish2(x0)) finish2(a12(x0))
Da13(finish2(x0)) finish2(a13(x0))
Da14(finish2(x0)) finish2(a14(x0))
Da15(finish2(x0)) finish2(a15(x0))
Da16(finish2(x0)) finish2(a16(x0))
Da23(finish2(x0)) finish2(a23(x0))
Da24(finish2(x0)) finish2(a24(x0))
Da25(finish2(x0)) finish2(a25(x0))
Da26(finish2(x0)) finish2(a26(x0))
Da34(finish2(x0)) finish2(a34(x0))
Da35(finish2(x0)) finish2(a35(x0))
Da36(finish2(x0)) finish2(a36(x0))
Da45(finish2(x0)) finish2(a45(x0))
Da46(finish2(x0)) finish2(a46(x0))
Da56(finish2(x0)) finish2(a56(x0))
rotate(finish2(x0)) rewrite(x0)
rewrite(a12(a12(a12(a12(x0))))) begin(x0)
rewrite(a13(a13(a13(a13(x0))))) begin(x0)
rewrite(a14(a14(a14(a14(x0))))) begin(x0)
rewrite(a15(a15(a15(a15(x0))))) begin(x0)
rewrite(a16(a16(a16(a16(x0))))) begin(x0)
rewrite(a23(a23(a23(a23(x0))))) begin(x0)
rewrite(a24(a24(a24(a24(x0))))) begin(x0)
rewrite(a25(a25(a25(a25(x0))))) begin(x0)
rewrite(a26(a26(a26(a26(x0))))) begin(x0)
rewrite(a34(a34(a34(a34(x0))))) begin(x0)
rewrite(a35(a35(a35(a35(x0))))) begin(x0)
rewrite(a36(a36(a36(a36(x0))))) begin(x0)
rewrite(a45(a45(a45(a45(x0))))) begin(x0)
rewrite(a46(a46(a46(a46(x0))))) begin(x0)
rewrite(a56(a56(a56(a56(x0))))) begin(x0)
rewrite(a13(a13(x0))) begin(a12(a12(a23(a23(a12(a12(x0)))))))
rewrite(a14(a14(x0))) begin(a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x0)))))))))))
rewrite(a15(a15(x0))) begin(a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x0)))))))))))))))
rewrite(a16(a16(x0))) begin(a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x0)))))))))))))))))))
rewrite(a24(a24(x0))) begin(a23(a23(a34(a34(a23(a23(x0)))))))
rewrite(a25(a25(x0))) begin(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x0)))))))))))
rewrite(a26(a26(x0))) begin(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x0)))))))))))))))
rewrite(a35(a35(x0))) begin(a34(a34(a45(a45(a34(a34(x0)))))))
rewrite(a36(a36(x0))) begin(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x0)))))))))))
rewrite(a46(a46(x0))) begin(a45(a45(a56(a56(a45(a45(x0)))))))
rewrite(a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x0))))))))))))) begin(x0)
rewrite(a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x0))))))))))))) begin(x0)
rewrite(a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x0))))))))))))) begin(x0)
rewrite(a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x0))))))))))))) begin(x0)
rewrite(a12(a12(a34(a34(x0))))) begin(a34(a34(a12(a12(x0)))))
rewrite(a12(a12(a45(a45(x0))))) begin(a45(a45(a12(a12(x0)))))
rewrite(a12(a12(a56(a56(x0))))) begin(a56(a56(a12(a12(x0)))))
rewrite(a23(a23(a45(a45(x0))))) begin(a45(a45(a23(a23(x0)))))
rewrite(a23(a23(a56(a56(x0))))) begin(a56(a56(a23(a23(x0)))))
rewrite(a34(a34(a56(a56(x0))))) begin(a56(a56(a34(a34(x0)))))

Proof

1 Termination Assumption

We assume termination of the following TRS
begin(end(x0)) rewrite(end(x0))
begin(a12(x0)) rotate(cut(Ca12(guess(x0))))
begin(a13(x0)) rotate(cut(Ca13(guess(x0))))
begin(a14(x0)) rotate(cut(Ca14(guess(x0))))
begin(a15(x0)) rotate(cut(Ca15(guess(x0))))
begin(a16(x0)) rotate(cut(Ca16(guess(x0))))
begin(a23(x0)) rotate(cut(Ca23(guess(x0))))
begin(a24(x0)) rotate(cut(Ca24(guess(x0))))
begin(a25(x0)) rotate(cut(Ca25(guess(x0))))
begin(a26(x0)) rotate(cut(Ca26(guess(x0))))
begin(a34(x0)) rotate(cut(Ca34(guess(x0))))
begin(a35(x0)) rotate(cut(Ca35(guess(x0))))
begin(a36(x0)) rotate(cut(Ca36(guess(x0))))
begin(a45(x0)) rotate(cut(Ca45(guess(x0))))
begin(a46(x0)) rotate(cut(Ca46(guess(x0))))
begin(a56(x0)) rotate(cut(Ca56(guess(x0))))
guess(a12(x0)) Ca12(guess(x0))
guess(a13(x0)) Ca13(guess(x0))
guess(a14(x0)) Ca14(guess(x0))
guess(a15(x0)) Ca15(guess(x0))
guess(a16(x0)) Ca16(guess(x0))
guess(a23(x0)) Ca23(guess(x0))
guess(a24(x0)) Ca24(guess(x0))
guess(a25(x0)) Ca25(guess(x0))
guess(a26(x0)) Ca26(guess(x0))
guess(a34(x0)) Ca34(guess(x0))
guess(a35(x0)) Ca35(guess(x0))
guess(a36(x0)) Ca36(guess(x0))
guess(a45(x0)) Ca45(guess(x0))
guess(a46(x0)) Ca46(guess(x0))
guess(a56(x0)) Ca56(guess(x0))
guess(a12(x0)) moveleft(Ba12(wait(x0)))
guess(a13(x0)) moveleft(Ba13(wait(x0)))
guess(a14(x0)) moveleft(Ba14(wait(x0)))
guess(a15(x0)) moveleft(Ba15(wait(x0)))
guess(a16(x0)) moveleft(Ba16(wait(x0)))
guess(a23(x0)) moveleft(Ba23(wait(x0)))
guess(a24(x0)) moveleft(Ba24(wait(x0)))
guess(a25(x0)) moveleft(Ba25(wait(x0)))
guess(a26(x0)) moveleft(Ba26(wait(x0)))
guess(a34(x0)) moveleft(Ba34(wait(x0)))
guess(a35(x0)) moveleft(Ba35(wait(x0)))
guess(a36(x0)) moveleft(Ba36(wait(x0)))
guess(a45(x0)) moveleft(Ba45(wait(x0)))
guess(a46(x0)) moveleft(Ba46(wait(x0)))
guess(a56(x0)) moveleft(Ba56(wait(x0)))
guess(end(x0)) finish(end(x0))
Ca12(moveleft(Ba12(x0))) moveleft(Ba12(Aa12(x0)))
Ca13(moveleft(Ba12(x0))) moveleft(Ba12(Aa13(x0)))
Ca14(moveleft(Ba12(x0))) moveleft(Ba12(Aa14(x0)))
Ca15(moveleft(Ba12(x0))) moveleft(Ba12(Aa15(x0)))
Ca16(moveleft(Ba12(x0))) moveleft(Ba12(Aa16(x0)))
Ca23(moveleft(Ba12(x0))) moveleft(Ba12(Aa23(x0)))
Ca24(moveleft(Ba12(x0))) moveleft(Ba12(Aa24(x0)))
Ca25(moveleft(Ba12(x0))) moveleft(Ba12(Aa25(x0)))
Ca26(moveleft(Ba12(x0))) moveleft(Ba12(Aa26(x0)))
Ca34(moveleft(Ba12(x0))) moveleft(Ba12(Aa34(x0)))
Ca35(moveleft(Ba12(x0))) moveleft(Ba12(Aa35(x0)))
Ca36(moveleft(Ba12(x0))) moveleft(Ba12(Aa36(x0)))
Ca45(moveleft(Ba12(x0))) moveleft(Ba12(Aa45(x0)))
Ca46(moveleft(Ba12(x0))) moveleft(Ba12(Aa46(x0)))
Ca56(moveleft(Ba12(x0))) moveleft(Ba12(Aa56(x0)))
Ca12(moveleft(Ba13(x0))) moveleft(Ba13(Aa12(x0)))
Ca13(moveleft(Ba13(x0))) moveleft(Ba13(Aa13(x0)))
Ca14(moveleft(Ba13(x0))) moveleft(Ba13(Aa14(x0)))
Ca15(moveleft(Ba13(x0))) moveleft(Ba13(Aa15(x0)))
Ca16(moveleft(Ba13(x0))) moveleft(Ba13(Aa16(x0)))
Ca23(moveleft(Ba13(x0))) moveleft(Ba13(Aa23(x0)))
Ca24(moveleft(Ba13(x0))) moveleft(Ba13(Aa24(x0)))
Ca25(moveleft(Ba13(x0))) moveleft(Ba13(Aa25(x0)))
Ca26(moveleft(Ba13(x0))) moveleft(Ba13(Aa26(x0)))
Ca34(moveleft(Ba13(x0))) moveleft(Ba13(Aa34(x0)))
Ca35(moveleft(Ba13(x0))) moveleft(Ba13(Aa35(x0)))
Ca36(moveleft(Ba13(x0))) moveleft(Ba13(Aa36(x0)))
Ca45(moveleft(Ba13(x0))) moveleft(Ba13(Aa45(x0)))
Ca46(moveleft(Ba13(x0))) moveleft(Ba13(Aa46(x0)))
Ca56(moveleft(Ba13(x0))) moveleft(Ba13(Aa56(x0)))
Ca12(moveleft(Ba14(x0))) moveleft(Ba14(Aa12(x0)))
Ca13(moveleft(Ba14(x0))) moveleft(Ba14(Aa13(x0)))
Ca14(moveleft(Ba14(x0))) moveleft(Ba14(Aa14(x0)))
Ca15(moveleft(Ba14(x0))) moveleft(Ba14(Aa15(x0)))
Ca16(moveleft(Ba14(x0))) moveleft(Ba14(Aa16(x0)))
Ca23(moveleft(Ba14(x0))) moveleft(Ba14(Aa23(x0)))
Ca24(moveleft(Ba14(x0))) moveleft(Ba14(Aa24(x0)))
Ca25(moveleft(Ba14(x0))) moveleft(Ba14(Aa25(x0)))
Ca26(moveleft(Ba14(x0))) moveleft(Ba14(Aa26(x0)))
Ca34(moveleft(Ba14(x0))) moveleft(Ba14(Aa34(x0)))
Ca35(moveleft(Ba14(x0))) moveleft(Ba14(Aa35(x0)))
Ca36(moveleft(Ba14(x0))) moveleft(Ba14(Aa36(x0)))
Ca45(moveleft(Ba14(x0))) moveleft(Ba14(Aa45(x0)))
Ca46(moveleft(Ba14(x0))) moveleft(Ba14(Aa46(x0)))
Ca56(moveleft(Ba14(x0))) moveleft(Ba14(Aa56(x0)))
Ca12(moveleft(Ba15(x0))) moveleft(Ba15(Aa12(x0)))
Ca13(moveleft(Ba15(x0))) moveleft(Ba15(Aa13(x0)))
Ca14(moveleft(Ba15(x0))) moveleft(Ba15(Aa14(x0)))
Ca15(moveleft(Ba15(x0))) moveleft(Ba15(Aa15(x0)))
Ca16(moveleft(Ba15(x0))) moveleft(Ba15(Aa16(x0)))
Ca23(moveleft(Ba15(x0))) moveleft(Ba15(Aa23(x0)))
Ca24(moveleft(Ba15(x0))) moveleft(Ba15(Aa24(x0)))
Ca25(moveleft(Ba15(x0))) moveleft(Ba15(Aa25(x0)))
Ca26(moveleft(Ba15(x0))) moveleft(Ba15(Aa26(x0)))
Ca34(moveleft(Ba15(x0))) moveleft(Ba15(Aa34(x0)))
Ca35(moveleft(Ba15(x0))) moveleft(Ba15(Aa35(x0)))
Ca36(moveleft(Ba15(x0))) moveleft(Ba15(Aa36(x0)))
Ca45(moveleft(Ba15(x0))) moveleft(Ba15(Aa45(x0)))
Ca46(moveleft(Ba15(x0))) moveleft(Ba15(Aa46(x0)))
Ca56(moveleft(Ba15(x0))) moveleft(Ba15(Aa56(x0)))
Ca12(moveleft(Ba16(x0))) moveleft(Ba16(Aa12(x0)))
Ca13(moveleft(Ba16(x0))) moveleft(Ba16(Aa13(x0)))
Ca14(moveleft(Ba16(x0))) moveleft(Ba16(Aa14(x0)))
Ca15(moveleft(Ba16(x0))) moveleft(Ba16(Aa15(x0)))
Ca16(moveleft(Ba16(x0))) moveleft(Ba16(Aa16(x0)))
Ca23(moveleft(Ba16(x0))) moveleft(Ba16(Aa23(x0)))
Ca24(moveleft(Ba16(x0))) moveleft(Ba16(Aa24(x0)))
Ca25(moveleft(Ba16(x0))) moveleft(Ba16(Aa25(x0)))
Ca26(moveleft(Ba16(x0))) moveleft(Ba16(Aa26(x0)))
Ca34(moveleft(Ba16(x0))) moveleft(Ba16(Aa34(x0)))
Ca35(moveleft(Ba16(x0))) moveleft(Ba16(Aa35(x0)))
Ca36(moveleft(Ba16(x0))) moveleft(Ba16(Aa36(x0)))
Ca45(moveleft(Ba16(x0))) moveleft(Ba16(Aa45(x0)))
Ca46(moveleft(Ba16(x0))) moveleft(Ba16(Aa46(x0)))
Ca56(moveleft(Ba16(x0))) moveleft(Ba16(Aa56(x0)))
Ca12(moveleft(Ba23(x0))) moveleft(Ba23(Aa12(x0)))
Ca13(moveleft(Ba23(x0))) moveleft(Ba23(Aa13(x0)))
Ca14(moveleft(Ba23(x0))) moveleft(Ba23(Aa14(x0)))
Ca15(moveleft(Ba23(x0))) moveleft(Ba23(Aa15(x0)))
Ca16(moveleft(Ba23(x0))) moveleft(Ba23(Aa16(x0)))
Ca23(moveleft(Ba23(x0))) moveleft(Ba23(Aa23(x0)))
Ca24(moveleft(Ba23(x0))) moveleft(Ba23(Aa24(x0)))
Ca25(moveleft(Ba23(x0))) moveleft(Ba23(Aa25(x0)))
Ca26(moveleft(Ba23(x0))) moveleft(Ba23(Aa26(x0)))
Ca34(moveleft(Ba23(x0))) moveleft(Ba23(Aa34(x0)))
Ca35(moveleft(Ba23(x0))) moveleft(Ba23(Aa35(x0)))
Ca36(moveleft(Ba23(x0))) moveleft(Ba23(Aa36(x0)))
Ca45(moveleft(Ba23(x0))) moveleft(Ba23(Aa45(x0)))
Ca46(moveleft(Ba23(x0))) moveleft(Ba23(Aa46(x0)))
Ca56(moveleft(Ba23(x0))) moveleft(Ba23(Aa56(x0)))
Ca12(moveleft(Ba24(x0))) moveleft(Ba24(Aa12(x0)))
Ca13(moveleft(Ba24(x0))) moveleft(Ba24(Aa13(x0)))
Ca14(moveleft(Ba24(x0))) moveleft(Ba24(Aa14(x0)))
Ca15(moveleft(Ba24(x0))) moveleft(Ba24(Aa15(x0)))
Ca16(moveleft(Ba24(x0))) moveleft(Ba24(Aa16(x0)))
Ca23(moveleft(Ba24(x0))) moveleft(Ba24(Aa23(x0)))
Ca24(moveleft(Ba24(x0))) moveleft(Ba24(Aa24(x0)))
Ca25(moveleft(Ba24(x0))) moveleft(Ba24(Aa25(x0)))
Ca26(moveleft(Ba24(x0))) moveleft(Ba24(Aa26(x0)))
Ca34(moveleft(Ba24(x0))) moveleft(Ba24(Aa34(x0)))
Ca35(moveleft(Ba24(x0))) moveleft(Ba24(Aa35(x0)))
Ca36(moveleft(Ba24(x0))) moveleft(Ba24(Aa36(x0)))
Ca45(moveleft(Ba24(x0))) moveleft(Ba24(Aa45(x0)))
Ca46(moveleft(Ba24(x0))) moveleft(Ba24(Aa46(x0)))
Ca56(moveleft(Ba24(x0))) moveleft(Ba24(Aa56(x0)))
Ca12(moveleft(Ba25(x0))) moveleft(Ba25(Aa12(x0)))
Ca13(moveleft(Ba25(x0))) moveleft(Ba25(Aa13(x0)))
Ca14(moveleft(Ba25(x0))) moveleft(Ba25(Aa14(x0)))
Ca15(moveleft(Ba25(x0))) moveleft(Ba25(Aa15(x0)))
Ca16(moveleft(Ba25(x0))) moveleft(Ba25(Aa16(x0)))
Ca23(moveleft(Ba25(x0))) moveleft(Ba25(Aa23(x0)))
Ca24(moveleft(Ba25(x0))) moveleft(Ba25(Aa24(x0)))
Ca25(moveleft(Ba25(x0))) moveleft(Ba25(Aa25(x0)))
Ca26(moveleft(Ba25(x0))) moveleft(Ba25(Aa26(x0)))
Ca34(moveleft(Ba25(x0))) moveleft(Ba25(Aa34(x0)))
Ca35(moveleft(Ba25(x0))) moveleft(Ba25(Aa35(x0)))
Ca36(moveleft(Ba25(x0))) moveleft(Ba25(Aa36(x0)))
Ca45(moveleft(Ba25(x0))) moveleft(Ba25(Aa45(x0)))
Ca46(moveleft(Ba25(x0))) moveleft(Ba25(Aa46(x0)))
Ca56(moveleft(Ba25(x0))) moveleft(Ba25(Aa56(x0)))
Ca12(moveleft(Ba26(x0))) moveleft(Ba26(Aa12(x0)))
Ca13(moveleft(Ba26(x0))) moveleft(Ba26(Aa13(x0)))
Ca14(moveleft(Ba26(x0))) moveleft(Ba26(Aa14(x0)))
Ca15(moveleft(Ba26(x0))) moveleft(Ba26(Aa15(x0)))
Ca16(moveleft(Ba26(x0))) moveleft(Ba26(Aa16(x0)))
Ca23(moveleft(Ba26(x0))) moveleft(Ba26(Aa23(x0)))
Ca24(moveleft(Ba26(x0))) moveleft(Ba26(Aa24(x0)))
Ca25(moveleft(Ba26(x0))) moveleft(Ba26(Aa25(x0)))
Ca26(moveleft(Ba26(x0))) moveleft(Ba26(Aa26(x0)))
Ca34(moveleft(Ba26(x0))) moveleft(Ba26(Aa34(x0)))
Ca35(moveleft(Ba26(x0))) moveleft(Ba26(Aa35(x0)))
Ca36(moveleft(Ba26(x0))) moveleft(Ba26(Aa36(x0)))
Ca45(moveleft(Ba26(x0))) moveleft(Ba26(Aa45(x0)))
Ca46(moveleft(Ba26(x0))) moveleft(Ba26(Aa46(x0)))
Ca56(moveleft(Ba26(x0))) moveleft(Ba26(Aa56(x0)))
Ca12(moveleft(Ba34(x0))) moveleft(Ba34(Aa12(x0)))
Ca13(moveleft(Ba34(x0))) moveleft(Ba34(Aa13(x0)))
Ca14(moveleft(Ba34(x0))) moveleft(Ba34(Aa14(x0)))
Ca15(moveleft(Ba34(x0))) moveleft(Ba34(Aa15(x0)))
Ca16(moveleft(Ba34(x0))) moveleft(Ba34(Aa16(x0)))
Ca23(moveleft(Ba34(x0))) moveleft(Ba34(Aa23(x0)))
Ca24(moveleft(Ba34(x0))) moveleft(Ba34(Aa24(x0)))
Ca25(moveleft(Ba34(x0))) moveleft(Ba34(Aa25(x0)))
Ca26(moveleft(Ba34(x0))) moveleft(Ba34(Aa26(x0)))
Ca34(moveleft(Ba34(x0))) moveleft(Ba34(Aa34(x0)))
Ca35(moveleft(Ba34(x0))) moveleft(Ba34(Aa35(x0)))
Ca36(moveleft(Ba34(x0))) moveleft(Ba34(Aa36(x0)))
Ca45(moveleft(Ba34(x0))) moveleft(Ba34(Aa45(x0)))
Ca46(moveleft(Ba34(x0))) moveleft(Ba34(Aa46(x0)))
Ca56(moveleft(Ba34(x0))) moveleft(Ba34(Aa56(x0)))
Ca12(moveleft(Ba35(x0))) moveleft(Ba35(Aa12(x0)))
Ca13(moveleft(Ba35(x0))) moveleft(Ba35(Aa13(x0)))
Ca14(moveleft(Ba35(x0))) moveleft(Ba35(Aa14(x0)))
Ca15(moveleft(Ba35(x0))) moveleft(Ba35(Aa15(x0)))
Ca16(moveleft(Ba35(x0))) moveleft(Ba35(Aa16(x0)))
Ca23(moveleft(Ba35(x0))) moveleft(Ba35(Aa23(x0)))
Ca24(moveleft(Ba35(x0))) moveleft(Ba35(Aa24(x0)))
Ca25(moveleft(Ba35(x0))) moveleft(Ba35(Aa25(x0)))
Ca26(moveleft(Ba35(x0))) moveleft(Ba35(Aa26(x0)))
Ca34(moveleft(Ba35(x0))) moveleft(Ba35(Aa34(x0)))
Ca35(moveleft(Ba35(x0))) moveleft(Ba35(Aa35(x0)))
Ca36(moveleft(Ba35(x0))) moveleft(Ba35(Aa36(x0)))
Ca45(moveleft(Ba35(x0))) moveleft(Ba35(Aa45(x0)))
Ca46(moveleft(Ba35(x0))) moveleft(Ba35(Aa46(x0)))
Ca56(moveleft(Ba35(x0))) moveleft(Ba35(Aa56(x0)))
Ca12(moveleft(Ba36(x0))) moveleft(Ba36(Aa12(x0)))
Ca13(moveleft(Ba36(x0))) moveleft(Ba36(Aa13(x0)))
Ca14(moveleft(Ba36(x0))) moveleft(Ba36(Aa14(x0)))
Ca15(moveleft(Ba36(x0))) moveleft(Ba36(Aa15(x0)))
Ca16(moveleft(Ba36(x0))) moveleft(Ba36(Aa16(x0)))
Ca23(moveleft(Ba36(x0))) moveleft(Ba36(Aa23(x0)))
Ca24(moveleft(Ba36(x0))) moveleft(Ba36(Aa24(x0)))
Ca25(moveleft(Ba36(x0))) moveleft(Ba36(Aa25(x0)))
Ca26(moveleft(Ba36(x0))) moveleft(Ba36(Aa26(x0)))
Ca34(moveleft(Ba36(x0))) moveleft(Ba36(Aa34(x0)))
Ca35(moveleft(Ba36(x0))) moveleft(Ba36(Aa35(x0)))
Ca36(moveleft(Ba36(x0))) moveleft(Ba36(Aa36(x0)))
Ca45(moveleft(Ba36(x0))) moveleft(Ba36(Aa45(x0)))
Ca46(moveleft(Ba36(x0))) moveleft(Ba36(Aa46(x0)))
Ca56(moveleft(Ba36(x0))) moveleft(Ba36(Aa56(x0)))
Ca12(moveleft(Ba45(x0))) moveleft(Ba45(Aa12(x0)))
Ca13(moveleft(Ba45(x0))) moveleft(Ba45(Aa13(x0)))
Ca14(moveleft(Ba45(x0))) moveleft(Ba45(Aa14(x0)))
Ca15(moveleft(Ba45(x0))) moveleft(Ba45(Aa15(x0)))
Ca16(moveleft(Ba45(x0))) moveleft(Ba45(Aa16(x0)))
Ca23(moveleft(Ba45(x0))) moveleft(Ba45(Aa23(x0)))
Ca24(moveleft(Ba45(x0))) moveleft(Ba45(Aa24(x0)))
Ca25(moveleft(Ba45(x0))) moveleft(Ba45(Aa25(x0)))
Ca26(moveleft(Ba45(x0))) moveleft(Ba45(Aa26(x0)))
Ca34(moveleft(Ba45(x0))) moveleft(Ba45(Aa34(x0)))
Ca35(moveleft(Ba45(x0))) moveleft(Ba45(Aa35(x0)))
Ca36(moveleft(Ba45(x0))) moveleft(Ba45(Aa36(x0)))
Ca45(moveleft(Ba45(x0))) moveleft(Ba45(Aa45(x0)))
Ca46(moveleft(Ba45(x0))) moveleft(Ba45(Aa46(x0)))
Ca56(moveleft(Ba45(x0))) moveleft(Ba45(Aa56(x0)))
Ca12(moveleft(Ba46(x0))) moveleft(Ba46(Aa12(x0)))
Ca13(moveleft(Ba46(x0))) moveleft(Ba46(Aa13(x0)))
Ca14(moveleft(Ba46(x0))) moveleft(Ba46(Aa14(x0)))
Ca15(moveleft(Ba46(x0))) moveleft(Ba46(Aa15(x0)))
Ca16(moveleft(Ba46(x0))) moveleft(Ba46(Aa16(x0)))
Ca23(moveleft(Ba46(x0))) moveleft(Ba46(Aa23(x0)))
Ca24(moveleft(Ba46(x0))) moveleft(Ba46(Aa24(x0)))
Ca25(moveleft(Ba46(x0))) moveleft(Ba46(Aa25(x0)))
Ca26(moveleft(Ba46(x0))) moveleft(Ba46(Aa26(x0)))
Ca34(moveleft(Ba46(x0))) moveleft(Ba46(Aa34(x0)))
Ca35(moveleft(Ba46(x0))) moveleft(Ba46(Aa35(x0)))
Ca36(moveleft(Ba46(x0))) moveleft(Ba46(Aa36(x0)))
Ca45(moveleft(Ba46(x0))) moveleft(Ba46(Aa45(x0)))
Ca46(moveleft(Ba46(x0))) moveleft(Ba46(Aa46(x0)))
Ca56(moveleft(Ba46(x0))) moveleft(Ba46(Aa56(x0)))
Ca12(moveleft(Ba56(x0))) moveleft(Ba56(Aa12(x0)))
Ca13(moveleft(Ba56(x0))) moveleft(Ba56(Aa13(x0)))
Ca14(moveleft(Ba56(x0))) moveleft(Ba56(Aa14(x0)))
Ca15(moveleft(Ba56(x0))) moveleft(Ba56(Aa15(x0)))
Ca16(moveleft(Ba56(x0))) moveleft(Ba56(Aa16(x0)))
Ca23(moveleft(Ba56(x0))) moveleft(Ba56(Aa23(x0)))
Ca24(moveleft(Ba56(x0))) moveleft(Ba56(Aa24(x0)))
Ca25(moveleft(Ba56(x0))) moveleft(Ba56(Aa25(x0)))
Ca26(moveleft(Ba56(x0))) moveleft(Ba56(Aa26(x0)))
Ca34(moveleft(Ba56(x0))) moveleft(Ba56(Aa34(x0)))
Ca35(moveleft(Ba56(x0))) moveleft(Ba56(Aa35(x0)))
Ca36(moveleft(Ba56(x0))) moveleft(Ba56(Aa36(x0)))
Ca45(moveleft(Ba56(x0))) moveleft(Ba56(Aa45(x0)))
Ca46(moveleft(Ba56(x0))) moveleft(Ba56(Aa46(x0)))
Ca56(moveleft(Ba56(x0))) moveleft(Ba56(Aa56(x0)))
cut(moveleft(Ba12(x0))) Da12(cut(goright(x0)))
cut(moveleft(Ba13(x0))) Da13(cut(goright(x0)))
cut(moveleft(Ba14(x0))) Da14(cut(goright(x0)))
cut(moveleft(Ba15(x0))) Da15(cut(goright(x0)))
cut(moveleft(Ba16(x0))) Da16(cut(goright(x0)))
cut(moveleft(Ba23(x0))) Da23(cut(goright(x0)))
cut(moveleft(Ba24(x0))) Da24(cut(goright(x0)))
cut(moveleft(Ba25(x0))) Da25(cut(goright(x0)))
cut(moveleft(Ba26(x0))) Da26(cut(goright(x0)))
cut(moveleft(Ba34(x0))) Da34(cut(goright(x0)))
cut(moveleft(Ba35(x0))) Da35(cut(goright(x0)))
cut(moveleft(Ba36(x0))) Da36(cut(goright(x0)))
cut(moveleft(Ba45(x0))) Da45(cut(goright(x0)))
cut(moveleft(Ba46(x0))) Da46(cut(goright(x0)))
cut(moveleft(Ba56(x0))) Da56(cut(goright(x0)))
goright(Aa12(x0)) Ca12(goright(x0))
goright(Aa13(x0)) Ca13(goright(x0))
goright(Aa14(x0)) Ca14(goright(x0))
goright(Aa15(x0)) Ca15(goright(x0))
goright(Aa16(x0)) Ca16(goright(x0))
goright(Aa23(x0)) Ca23(goright(x0))
goright(Aa24(x0)) Ca24(goright(x0))
goright(Aa25(x0)) Ca25(goright(x0))
goright(Aa26(x0)) Ca26(goright(x0))
goright(Aa34(x0)) Ca34(goright(x0))
goright(Aa35(x0)) Ca35(goright(x0))
goright(Aa36(x0)) Ca36(goright(x0))
goright(Aa45(x0)) Ca45(goright(x0))
goright(Aa46(x0)) Ca46(goright(x0))
goright(Aa56(x0)) Ca56(goright(x0))
goright(wait(a12(x0))) moveleft(Ba12(wait(x0)))
goright(wait(a13(x0))) moveleft(Ba13(wait(x0)))
goright(wait(a14(x0))) moveleft(Ba14(wait(x0)))
goright(wait(a15(x0))) moveleft(Ba15(wait(x0)))
goright(wait(a16(x0))) moveleft(Ba16(wait(x0)))
goright(wait(a23(x0))) moveleft(Ba23(wait(x0)))
goright(wait(a24(x0))) moveleft(Ba24(wait(x0)))
goright(wait(a25(x0))) moveleft(Ba25(wait(x0)))
goright(wait(a26(x0))) moveleft(Ba26(wait(x0)))
goright(wait(a34(x0))) moveleft(Ba34(wait(x0)))
goright(wait(a35(x0))) moveleft(Ba35(wait(x0)))
goright(wait(a36(x0))) moveleft(Ba36(wait(x0)))
goright(wait(a45(x0))) moveleft(Ba45(wait(x0)))
goright(wait(a46(x0))) moveleft(Ba46(wait(x0)))
goright(wait(a56(x0))) moveleft(Ba56(wait(x0)))
goright(wait(end(x0))) finish(end(x0))
Ca12(finish(x0)) finish(a12(x0))
Ca13(finish(x0)) finish(a13(x0))
Ca14(finish(x0)) finish(a14(x0))
Ca15(finish(x0)) finish(a15(x0))
Ca16(finish(x0)) finish(a16(x0))
Ca23(finish(x0)) finish(a23(x0))
Ca24(finish(x0)) finish(a24(x0))
Ca25(finish(x0)) finish(a25(x0))
Ca26(finish(x0)) finish(a26(x0))
Ca34(finish(x0)) finish(a34(x0))
Ca35(finish(x0)) finish(a35(x0))
Ca36(finish(x0)) finish(a36(x0))
Ca45(finish(x0)) finish(a45(x0))
Ca46(finish(x0)) finish(a46(x0))
Ca56(finish(x0)) finish(a56(x0))
cut(finish(x0)) finish2(x0)
Da12(finish2(x0)) finish2(a12(x0))
Da13(finish2(x0)) finish2(a13(x0))
Da14(finish2(x0)) finish2(a14(x0))
Da15(finish2(x0)) finish2(a15(x0))
Da16(finish2(x0)) finish2(a16(x0))
Da23(finish2(x0)) finish2(a23(x0))
Da24(finish2(x0)) finish2(a24(x0))
Da25(finish2(x0)) finish2(a25(x0))
Da26(finish2(x0)) finish2(a26(x0))
Da34(finish2(x0)) finish2(a34(x0))
Da35(finish2(x0)) finish2(a35(x0))
Da36(finish2(x0)) finish2(a36(x0))
Da45(finish2(x0)) finish2(a45(x0))
Da46(finish2(x0)) finish2(a46(x0))
Da56(finish2(x0)) finish2(a56(x0))
rotate(finish2(x0)) rewrite(x0)
rewrite(a12(a12(a12(a12(x0))))) begin(x0)
rewrite(a13(a13(a13(a13(x0))))) begin(x0)
rewrite(a14(a14(a14(a14(x0))))) begin(x0)
rewrite(a15(a15(a15(a15(x0))))) begin(x0)
rewrite(a16(a16(a16(a16(x0))))) begin(x0)
rewrite(a23(a23(a23(a23(x0))))) begin(x0)
rewrite(a24(a24(a24(a24(x0))))) begin(x0)
rewrite(a25(a25(a25(a25(x0))))) begin(x0)
rewrite(a26(a26(a26(a26(x0))))) begin(x0)
rewrite(a34(a34(a34(a34(x0))))) begin(x0)
rewrite(a35(a35(a35(a35(x0))))) begin(x0)
rewrite(a36(a36(a36(a36(x0))))) begin(x0)
rewrite(a45(a45(a45(a45(x0))))) begin(x0)
rewrite(a46(a46(a46(a46(x0))))) begin(x0)
rewrite(a56(a56(a56(a56(x0))))) begin(x0)
rewrite(a13(a13(x0))) begin(a12(a12(a23(a23(a12(a12(x0)))))))
rewrite(a14(a14(x0))) begin(a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x0)))))))))))
rewrite(a15(a15(x0))) begin(a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x0)))))))))))))))
rewrite(a16(a16(x0))) begin(a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x0)))))))))))))))))))
rewrite(a24(a24(x0))) begin(a23(a23(a34(a34(a23(a23(x0)))))))
rewrite(a25(a25(x0))) begin(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x0)))))))))))
rewrite(a26(a26(x0))) begin(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x0)))))))))))))))
rewrite(a35(a35(x0))) begin(a34(a34(a45(a45(a34(a34(x0)))))))
rewrite(a36(a36(x0))) begin(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x0)))))))))))
rewrite(a46(a46(x0))) begin(a45(a45(a56(a56(a45(a45(x0)))))))
rewrite(a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x0))))))))))))) begin(x0)
rewrite(a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x0))))))))))))) begin(x0)
rewrite(a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x0))))))))))))) begin(x0)
rewrite(a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x0))))))))))))) begin(x0)
rewrite(a12(a12(a34(a34(x0))))) begin(a34(a34(a12(a12(x0)))))
rewrite(a12(a12(a45(a45(x0))))) begin(a45(a45(a12(a12(x0)))))
rewrite(a12(a12(a56(a56(x0))))) begin(a56(a56(a12(a12(x0)))))
rewrite(a23(a23(a45(a45(x0))))) begin(a45(a45(a23(a23(x0)))))
rewrite(a23(a23(a56(a56(x0))))) begin(a56(a56(a23(a23(x0)))))
rewrite(a34(a34(a56(a56(x0))))) begin(a56(a56(a34(a34(x0)))))