MAYBE
by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
begin(end(x0)) | → | rewrite(end(x0)) |
begin(A(x0)) | → | rotate(cut(CA(guess(x0)))) |
begin(b(x0)) | → | rotate(cut(Cb(guess(x0)))) |
begin(a(x0)) | → | rotate(cut(Ca(guess(x0)))) |
begin(B(x0)) | → | rotate(cut(CB(guess(x0)))) |
guess(A(x0)) | → | CA(guess(x0)) |
guess(b(x0)) | → | Cb(guess(x0)) |
guess(a(x0)) | → | Ca(guess(x0)) |
guess(B(x0)) | → | CB(guess(x0)) |
guess(A(x0)) | → | moveleft(BA(wait(x0))) |
guess(b(x0)) | → | moveleft(Bb(wait(x0))) |
guess(a(x0)) | → | moveleft(Ba(wait(x0))) |
guess(B(x0)) | → | moveleft(BB(wait(x0))) |
guess(end(x0)) | → | finish(end(x0)) |
CA(moveleft(BA(x0))) | → | moveleft(BA(AA(x0))) |
Cb(moveleft(BA(x0))) | → | moveleft(BA(Ab(x0))) |
Ca(moveleft(BA(x0))) | → | moveleft(BA(Aa(x0))) |
CB(moveleft(BA(x0))) | → | moveleft(BA(AB(x0))) |
CA(moveleft(Bb(x0))) | → | moveleft(Bb(AA(x0))) |
Cb(moveleft(Bb(x0))) | → | moveleft(Bb(Ab(x0))) |
Ca(moveleft(Bb(x0))) | → | moveleft(Bb(Aa(x0))) |
CB(moveleft(Bb(x0))) | → | moveleft(Bb(AB(x0))) |
CA(moveleft(Ba(x0))) | → | moveleft(Ba(AA(x0))) |
Cb(moveleft(Ba(x0))) | → | moveleft(Ba(Ab(x0))) |
Ca(moveleft(Ba(x0))) | → | moveleft(Ba(Aa(x0))) |
CB(moveleft(Ba(x0))) | → | moveleft(Ba(AB(x0))) |
CA(moveleft(BB(x0))) | → | moveleft(BB(AA(x0))) |
Cb(moveleft(BB(x0))) | → | moveleft(BB(Ab(x0))) |
Ca(moveleft(BB(x0))) | → | moveleft(BB(Aa(x0))) |
CB(moveleft(BB(x0))) | → | moveleft(BB(AB(x0))) |
cut(moveleft(BA(x0))) | → | DA(cut(goright(x0))) |
cut(moveleft(Bb(x0))) | → | Db(cut(goright(x0))) |
cut(moveleft(Ba(x0))) | → | Da(cut(goright(x0))) |
cut(moveleft(BB(x0))) | → | DB(cut(goright(x0))) |
goright(AA(x0)) | → | CA(goright(x0)) |
goright(Ab(x0)) | → | Cb(goright(x0)) |
goright(Aa(x0)) | → | Ca(goright(x0)) |
goright(AB(x0)) | → | CB(goright(x0)) |
goright(wait(A(x0))) | → | moveleft(BA(wait(x0))) |
goright(wait(b(x0))) | → | moveleft(Bb(wait(x0))) |
goright(wait(a(x0))) | → | moveleft(Ba(wait(x0))) |
goright(wait(B(x0))) | → | moveleft(BB(wait(x0))) |
goright(wait(end(x0))) | → | finish(end(x0)) |
CA(finish(x0)) | → | finish(A(x0)) |
Cb(finish(x0)) | → | finish(b(x0)) |
Ca(finish(x0)) | → | finish(a(x0)) |
CB(finish(x0)) | → | finish(B(x0)) |
cut(finish(x0)) | → | finish2(x0) |
DA(finish2(x0)) | → | finish2(A(x0)) |
Db(finish2(x0)) | → | finish2(b(x0)) |
Da(finish2(x0)) | → | finish2(a(x0)) |
DB(finish2(x0)) | → | finish2(B(x0)) |
rotate(finish2(x0)) | → | rewrite(x0) |
rewrite(A(b(x0))) | → | begin(b(a(B(A(x0))))) |
rewrite(B(a(x0))) | → | begin(a(b(A(B(x0))))) |
rewrite(A(a(x0))) | → | begin(x0) |
rewrite(B(b(x0))) | → | begin(x0) |
begin(end(x0)) | → | rewrite(end(x0)) |
begin(A(x0)) | → | rotate(cut(CA(guess(x0)))) |
begin(b(x0)) | → | rotate(cut(Cb(guess(x0)))) |
begin(a(x0)) | → | rotate(cut(Ca(guess(x0)))) |
begin(B(x0)) | → | rotate(cut(CB(guess(x0)))) |
guess(A(x0)) | → | CA(guess(x0)) |
guess(b(x0)) | → | Cb(guess(x0)) |
guess(a(x0)) | → | Ca(guess(x0)) |
guess(B(x0)) | → | CB(guess(x0)) |
guess(A(x0)) | → | moveleft(BA(wait(x0))) |
guess(b(x0)) | → | moveleft(Bb(wait(x0))) |
guess(a(x0)) | → | moveleft(Ba(wait(x0))) |
guess(B(x0)) | → | moveleft(BB(wait(x0))) |
guess(end(x0)) | → | finish(end(x0)) |
CA(moveleft(BA(x0))) | → | moveleft(BA(AA(x0))) |
Cb(moveleft(BA(x0))) | → | moveleft(BA(Ab(x0))) |
Ca(moveleft(BA(x0))) | → | moveleft(BA(Aa(x0))) |
CB(moveleft(BA(x0))) | → | moveleft(BA(AB(x0))) |
CA(moveleft(Bb(x0))) | → | moveleft(Bb(AA(x0))) |
Cb(moveleft(Bb(x0))) | → | moveleft(Bb(Ab(x0))) |
Ca(moveleft(Bb(x0))) | → | moveleft(Bb(Aa(x0))) |
CB(moveleft(Bb(x0))) | → | moveleft(Bb(AB(x0))) |
CA(moveleft(Ba(x0))) | → | moveleft(Ba(AA(x0))) |
Cb(moveleft(Ba(x0))) | → | moveleft(Ba(Ab(x0))) |
Ca(moveleft(Ba(x0))) | → | moveleft(Ba(Aa(x0))) |
CB(moveleft(Ba(x0))) | → | moveleft(Ba(AB(x0))) |
CA(moveleft(BB(x0))) | → | moveleft(BB(AA(x0))) |
Cb(moveleft(BB(x0))) | → | moveleft(BB(Ab(x0))) |
Ca(moveleft(BB(x0))) | → | moveleft(BB(Aa(x0))) |
CB(moveleft(BB(x0))) | → | moveleft(BB(AB(x0))) |
cut(moveleft(BA(x0))) | → | DA(cut(goright(x0))) |
cut(moveleft(Bb(x0))) | → | Db(cut(goright(x0))) |
cut(moveleft(Ba(x0))) | → | Da(cut(goright(x0))) |
cut(moveleft(BB(x0))) | → | DB(cut(goright(x0))) |
goright(AA(x0)) | → | CA(goright(x0)) |
goright(Ab(x0)) | → | Cb(goright(x0)) |
goright(Aa(x0)) | → | Ca(goright(x0)) |
goright(AB(x0)) | → | CB(goright(x0)) |
goright(wait(A(x0))) | → | moveleft(BA(wait(x0))) |
goright(wait(b(x0))) | → | moveleft(Bb(wait(x0))) |
goright(wait(a(x0))) | → | moveleft(Ba(wait(x0))) |
goright(wait(B(x0))) | → | moveleft(BB(wait(x0))) |
goright(wait(end(x0))) | → | finish(end(x0)) |
CA(finish(x0)) | → | finish(A(x0)) |
Cb(finish(x0)) | → | finish(b(x0)) |
Ca(finish(x0)) | → | finish(a(x0)) |
CB(finish(x0)) | → | finish(B(x0)) |
cut(finish(x0)) | → | finish2(x0) |
DA(finish2(x0)) | → | finish2(A(x0)) |
Db(finish2(x0)) | → | finish2(b(x0)) |
Da(finish2(x0)) | → | finish2(a(x0)) |
DB(finish2(x0)) | → | finish2(B(x0)) |
rotate(finish2(x0)) | → | rewrite(x0) |
rewrite(A(b(x0))) | → | begin(b(a(B(A(x0))))) |
rewrite(B(a(x0))) | → | begin(a(b(A(B(x0))))) |
rewrite(A(a(x0))) | → | begin(x0) |
rewrite(B(b(x0))) | → | begin(x0) |