by ttt2 (version ttt2 1.15)
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(x0))) | → | begin(x0) |
| rewrite(a13(a13(x0))) | → | begin(x0) |
| rewrite(a14(a14(x0))) | → | begin(x0) |
| rewrite(a15(a15(x0))) | → | begin(x0) |
| rewrite(a16(a16(x0))) | → | begin(x0) |
| rewrite(a23(a23(x0))) | → | begin(x0) |
| rewrite(a24(a24(x0))) | → | begin(x0) |
| rewrite(a25(a25(x0))) | → | begin(x0) |
| rewrite(a26(a26(x0))) | → | begin(x0) |
| rewrite(a34(a34(x0))) | → | begin(x0) |
| rewrite(a35(a35(x0))) | → | begin(x0) |
| rewrite(a36(a36(x0))) | → | begin(x0) |
| rewrite(a45(a45(x0))) | → | begin(x0) |
| rewrite(a46(a46(x0))) | → | begin(x0) |
| rewrite(a56(a56(x0))) | → | begin(x0) |
| rewrite(a13(x0)) | → | begin(a12(a23(a12(x0)))) |
| rewrite(a14(x0)) | → | begin(a12(a23(a34(a23(a12(x0)))))) |
| rewrite(a15(x0)) | → | begin(a12(a23(a34(a45(a34(a23(a12(x0)))))))) |
| rewrite(a16(x0)) | → | begin(a12(a23(a34(a45(a56(a45(a34(a23(a12(x0)))))))))) |
| rewrite(a24(x0)) | → | begin(a23(a34(a23(x0)))) |
| rewrite(a25(x0)) | → | begin(a23(a34(a45(a34(a23(x0)))))) |
| rewrite(a26(x0)) | → | begin(a23(a34(a45(a56(a45(a34(a23(x0)))))))) |
| rewrite(a35(x0)) | → | begin(a34(a45(a34(x0)))) |
| rewrite(a36(x0)) | → | begin(a34(a45(a56(a45(a34(x0)))))) |
| rewrite(a46(x0)) | → | begin(a45(a56(a45(x0)))) |
| rewrite(a12(a23(a12(a23(a12(a23(x0))))))) | → | begin(x0) |
| rewrite(a23(a34(a23(a34(a23(a34(x0))))))) | → | begin(x0) |
| rewrite(a34(a45(a34(a45(a34(a45(x0))))))) | → | begin(x0) |
| rewrite(a45(a56(a45(a56(a45(a56(x0))))))) | → | begin(x0) |
| rewrite(a12(a34(x0))) | → | begin(a34(a12(x0))) |
| rewrite(a12(a45(x0))) | → | begin(a45(a12(x0))) |
| rewrite(a12(a56(x0))) | → | begin(a56(a12(x0))) |
| rewrite(a23(a45(x0))) | → | begin(a45(a23(x0))) |
| rewrite(a23(a56(x0))) | → | begin(a56(a23(x0))) |
| rewrite(a34(a56(x0))) | → | begin(a56(a34(x0))) |
| 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(x0))) | → | begin(x0) |
| rewrite(a13(a13(x0))) | → | begin(x0) |
| rewrite(a14(a14(x0))) | → | begin(x0) |
| rewrite(a15(a15(x0))) | → | begin(x0) |
| rewrite(a16(a16(x0))) | → | begin(x0) |
| rewrite(a23(a23(x0))) | → | begin(x0) |
| rewrite(a24(a24(x0))) | → | begin(x0) |
| rewrite(a25(a25(x0))) | → | begin(x0) |
| rewrite(a26(a26(x0))) | → | begin(x0) |
| rewrite(a34(a34(x0))) | → | begin(x0) |
| rewrite(a35(a35(x0))) | → | begin(x0) |
| rewrite(a36(a36(x0))) | → | begin(x0) |
| rewrite(a45(a45(x0))) | → | begin(x0) |
| rewrite(a46(a46(x0))) | → | begin(x0) |
| rewrite(a56(a56(x0))) | → | begin(x0) |
| rewrite(a13(x0)) | → | begin(a12(a23(a12(x0)))) |
| rewrite(a14(x0)) | → | begin(a12(a23(a34(a23(a12(x0)))))) |
| rewrite(a15(x0)) | → | begin(a12(a23(a34(a45(a34(a23(a12(x0)))))))) |
| rewrite(a16(x0)) | → | begin(a12(a23(a34(a45(a56(a45(a34(a23(a12(x0)))))))))) |
| rewrite(a24(x0)) | → | begin(a23(a34(a23(x0)))) |
| rewrite(a25(x0)) | → | begin(a23(a34(a45(a34(a23(x0)))))) |
| rewrite(a26(x0)) | → | begin(a23(a34(a45(a56(a45(a34(a23(x0)))))))) |
| rewrite(a35(x0)) | → | begin(a34(a45(a34(x0)))) |
| rewrite(a36(x0)) | → | begin(a34(a45(a56(a45(a34(x0)))))) |
| rewrite(a46(x0)) | → | begin(a45(a56(a45(x0)))) |
| rewrite(a12(a23(a12(a23(a12(a23(x0))))))) | → | begin(x0) |
| rewrite(a23(a34(a23(a34(a23(a34(x0))))))) | → | begin(x0) |
| rewrite(a34(a45(a34(a45(a34(a45(x0))))))) | → | begin(x0) |
| rewrite(a45(a56(a45(a56(a45(a56(x0))))))) | → | begin(x0) |
| rewrite(a12(a34(x0))) | → | begin(a34(a12(x0))) |
| rewrite(a12(a45(x0))) | → | begin(a45(a12(x0))) |
| rewrite(a12(a56(x0))) | → | begin(a56(a12(x0))) |
| rewrite(a23(a45(x0))) | → | begin(a45(a23(x0))) |
| rewrite(a23(a56(x0))) | → | begin(a56(a23(x0))) |
| rewrite(a34(a56(x0))) | → | begin(a56(a34(x0))) |