by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| begin(end(x0)) | → | rewrite(end(x0)) |
| begin(r1(x0)) | → | rotate(cut(Cr1(guess(x0)))) |
| begin(a(x0)) | → | rotate(cut(Ca(guess(x0)))) |
| begin(r2(x0)) | → | rotate(cut(Cr2(guess(x0)))) |
| begin(l1(x0)) | → | rotate(cut(Cl1(guess(x0)))) |
| begin(l2(x0)) | → | rotate(cut(Cl2(guess(x0)))) |
| begin(b(x0)) | → | rotate(cut(Cb(guess(x0)))) |
| guess(r1(x0)) | → | Cr1(guess(x0)) |
| guess(a(x0)) | → | Ca(guess(x0)) |
| guess(r2(x0)) | → | Cr2(guess(x0)) |
| guess(l1(x0)) | → | Cl1(guess(x0)) |
| guess(l2(x0)) | → | Cl2(guess(x0)) |
| guess(b(x0)) | → | Cb(guess(x0)) |
| guess(r1(x0)) | → | moveleft(Br1(wait(x0))) |
| guess(a(x0)) | → | moveleft(Ba(wait(x0))) |
| guess(r2(x0)) | → | moveleft(Br2(wait(x0))) |
| guess(l1(x0)) | → | moveleft(Bl1(wait(x0))) |
| guess(l2(x0)) | → | moveleft(Bl2(wait(x0))) |
| guess(b(x0)) | → | moveleft(Bb(wait(x0))) |
| guess(end(x0)) | → | finish(end(x0)) |
| Cr1(moveleft(Br1(x0))) | → | moveleft(Br1(Ar1(x0))) |
| Ca(moveleft(Br1(x0))) | → | moveleft(Br1(Aa(x0))) |
| Cr2(moveleft(Br1(x0))) | → | moveleft(Br1(Ar2(x0))) |
| Cl1(moveleft(Br1(x0))) | → | moveleft(Br1(Al1(x0))) |
| Cl2(moveleft(Br1(x0))) | → | moveleft(Br1(Al2(x0))) |
| Cb(moveleft(Br1(x0))) | → | moveleft(Br1(Ab(x0))) |
| Cr1(moveleft(Ba(x0))) | → | moveleft(Ba(Ar1(x0))) |
| Ca(moveleft(Ba(x0))) | → | moveleft(Ba(Aa(x0))) |
| Cr2(moveleft(Ba(x0))) | → | moveleft(Ba(Ar2(x0))) |
| Cl1(moveleft(Ba(x0))) | → | moveleft(Ba(Al1(x0))) |
| Cl2(moveleft(Ba(x0))) | → | moveleft(Ba(Al2(x0))) |
| Cb(moveleft(Ba(x0))) | → | moveleft(Ba(Ab(x0))) |
| Cr1(moveleft(Br2(x0))) | → | moveleft(Br2(Ar1(x0))) |
| Ca(moveleft(Br2(x0))) | → | moveleft(Br2(Aa(x0))) |
| Cr2(moveleft(Br2(x0))) | → | moveleft(Br2(Ar2(x0))) |
| Cl1(moveleft(Br2(x0))) | → | moveleft(Br2(Al1(x0))) |
| Cl2(moveleft(Br2(x0))) | → | moveleft(Br2(Al2(x0))) |
| Cb(moveleft(Br2(x0))) | → | moveleft(Br2(Ab(x0))) |
| Cr1(moveleft(Bl1(x0))) | → | moveleft(Bl1(Ar1(x0))) |
| Ca(moveleft(Bl1(x0))) | → | moveleft(Bl1(Aa(x0))) |
| Cr2(moveleft(Bl1(x0))) | → | moveleft(Bl1(Ar2(x0))) |
| Cl1(moveleft(Bl1(x0))) | → | moveleft(Bl1(Al1(x0))) |
| Cl2(moveleft(Bl1(x0))) | → | moveleft(Bl1(Al2(x0))) |
| Cb(moveleft(Bl1(x0))) | → | moveleft(Bl1(Ab(x0))) |
| Cr1(moveleft(Bl2(x0))) | → | moveleft(Bl2(Ar1(x0))) |
| Ca(moveleft(Bl2(x0))) | → | moveleft(Bl2(Aa(x0))) |
| Cr2(moveleft(Bl2(x0))) | → | moveleft(Bl2(Ar2(x0))) |
| Cl1(moveleft(Bl2(x0))) | → | moveleft(Bl2(Al1(x0))) |
| Cl2(moveleft(Bl2(x0))) | → | moveleft(Bl2(Al2(x0))) |
| Cb(moveleft(Bl2(x0))) | → | moveleft(Bl2(Ab(x0))) |
| Cr1(moveleft(Bb(x0))) | → | moveleft(Bb(Ar1(x0))) |
| Ca(moveleft(Bb(x0))) | → | moveleft(Bb(Aa(x0))) |
| Cr2(moveleft(Bb(x0))) | → | moveleft(Bb(Ar2(x0))) |
| Cl1(moveleft(Bb(x0))) | → | moveleft(Bb(Al1(x0))) |
| Cl2(moveleft(Bb(x0))) | → | moveleft(Bb(Al2(x0))) |
| Cb(moveleft(Bb(x0))) | → | moveleft(Bb(Ab(x0))) |
| cut(moveleft(Br1(x0))) | → | Dr1(cut(goright(x0))) |
| cut(moveleft(Ba(x0))) | → | Da(cut(goright(x0))) |
| cut(moveleft(Br2(x0))) | → | Dr2(cut(goright(x0))) |
| cut(moveleft(Bl1(x0))) | → | Dl1(cut(goright(x0))) |
| cut(moveleft(Bl2(x0))) | → | Dl2(cut(goright(x0))) |
| cut(moveleft(Bb(x0))) | → | Db(cut(goright(x0))) |
| goright(Ar1(x0)) | → | Cr1(goright(x0)) |
| goright(Aa(x0)) | → | Ca(goright(x0)) |
| goright(Ar2(x0)) | → | Cr2(goright(x0)) |
| goright(Al1(x0)) | → | Cl1(goright(x0)) |
| goright(Al2(x0)) | → | Cl2(goright(x0)) |
| goright(Ab(x0)) | → | Cb(goright(x0)) |
| goright(wait(r1(x0))) | → | moveleft(Br1(wait(x0))) |
| goright(wait(a(x0))) | → | moveleft(Ba(wait(x0))) |
| goright(wait(r2(x0))) | → | moveleft(Br2(wait(x0))) |
| goright(wait(l1(x0))) | → | moveleft(Bl1(wait(x0))) |
| goright(wait(l2(x0))) | → | moveleft(Bl2(wait(x0))) |
| goright(wait(b(x0))) | → | moveleft(Bb(wait(x0))) |
| goright(wait(end(x0))) | → | finish(end(x0)) |
| Cr1(finish(x0)) | → | finish(r1(x0)) |
| Ca(finish(x0)) | → | finish(a(x0)) |
| Cr2(finish(x0)) | → | finish(r2(x0)) |
| Cl1(finish(x0)) | → | finish(l1(x0)) |
| Cl2(finish(x0)) | → | finish(l2(x0)) |
| Cb(finish(x0)) | → | finish(b(x0)) |
| cut(finish(x0)) | → | finish2(x0) |
| Dr1(finish2(x0)) | → | finish2(r1(x0)) |
| Da(finish2(x0)) | → | finish2(a(x0)) |
| Dr2(finish2(x0)) | → | finish2(r2(x0)) |
| Dl1(finish2(x0)) | → | finish2(l1(x0)) |
| Dl2(finish2(x0)) | → | finish2(l2(x0)) |
| Db(finish2(x0)) | → | finish2(b(x0)) |
| rotate(finish2(x0)) | → | rewrite(x0) |
| rewrite(r1(a(x0))) | → | begin(a(a(a(r1(x0))))) |
| rewrite(r2(a(x0))) | → | begin(a(a(a(r2(x0))))) |
| rewrite(a(l1(x0))) | → | begin(l1(a(a(a(x0))))) |
| rewrite(a(a(l2(x0)))) | → | begin(l2(a(a(x0)))) |
| rewrite(r1(b(x0))) | → | begin(l1(b(x0))) |
| rewrite(r2(b(x0))) | → | begin(l2(a(b(x0)))) |
| rewrite(b(l1(x0))) | → | begin(b(r2(x0))) |
| rewrite(b(l2(x0))) | → | begin(b(r1(x0))) |
| rewrite(a(a(x0))) | → | begin(x0) |
| begin(end(x0)) | → | rewrite(end(x0)) |
| begin(r1(x0)) | → | rotate(cut(Cr1(guess(x0)))) |
| begin(a(x0)) | → | rotate(cut(Ca(guess(x0)))) |
| begin(r2(x0)) | → | rotate(cut(Cr2(guess(x0)))) |
| begin(l1(x0)) | → | rotate(cut(Cl1(guess(x0)))) |
| begin(l2(x0)) | → | rotate(cut(Cl2(guess(x0)))) |
| begin(b(x0)) | → | rotate(cut(Cb(guess(x0)))) |
| guess(r1(x0)) | → | Cr1(guess(x0)) |
| guess(a(x0)) | → | Ca(guess(x0)) |
| guess(r2(x0)) | → | Cr2(guess(x0)) |
| guess(l1(x0)) | → | Cl1(guess(x0)) |
| guess(l2(x0)) | → | Cl2(guess(x0)) |
| guess(b(x0)) | → | Cb(guess(x0)) |
| guess(r1(x0)) | → | moveleft(Br1(wait(x0))) |
| guess(a(x0)) | → | moveleft(Ba(wait(x0))) |
| guess(r2(x0)) | → | moveleft(Br2(wait(x0))) |
| guess(l1(x0)) | → | moveleft(Bl1(wait(x0))) |
| guess(l2(x0)) | → | moveleft(Bl2(wait(x0))) |
| guess(b(x0)) | → | moveleft(Bb(wait(x0))) |
| guess(end(x0)) | → | finish(end(x0)) |
| Cr1(moveleft(Br1(x0))) | → | moveleft(Br1(Ar1(x0))) |
| Ca(moveleft(Br1(x0))) | → | moveleft(Br1(Aa(x0))) |
| Cr2(moveleft(Br1(x0))) | → | moveleft(Br1(Ar2(x0))) |
| Cl1(moveleft(Br1(x0))) | → | moveleft(Br1(Al1(x0))) |
| Cl2(moveleft(Br1(x0))) | → | moveleft(Br1(Al2(x0))) |
| Cb(moveleft(Br1(x0))) | → | moveleft(Br1(Ab(x0))) |
| Cr1(moveleft(Ba(x0))) | → | moveleft(Ba(Ar1(x0))) |
| Ca(moveleft(Ba(x0))) | → | moveleft(Ba(Aa(x0))) |
| Cr2(moveleft(Ba(x0))) | → | moveleft(Ba(Ar2(x0))) |
| Cl1(moveleft(Ba(x0))) | → | moveleft(Ba(Al1(x0))) |
| Cl2(moveleft(Ba(x0))) | → | moveleft(Ba(Al2(x0))) |
| Cb(moveleft(Ba(x0))) | → | moveleft(Ba(Ab(x0))) |
| Cr1(moveleft(Br2(x0))) | → | moveleft(Br2(Ar1(x0))) |
| Ca(moveleft(Br2(x0))) | → | moveleft(Br2(Aa(x0))) |
| Cr2(moveleft(Br2(x0))) | → | moveleft(Br2(Ar2(x0))) |
| Cl1(moveleft(Br2(x0))) | → | moveleft(Br2(Al1(x0))) |
| Cl2(moveleft(Br2(x0))) | → | moveleft(Br2(Al2(x0))) |
| Cb(moveleft(Br2(x0))) | → | moveleft(Br2(Ab(x0))) |
| Cr1(moveleft(Bl1(x0))) | → | moveleft(Bl1(Ar1(x0))) |
| Ca(moveleft(Bl1(x0))) | → | moveleft(Bl1(Aa(x0))) |
| Cr2(moveleft(Bl1(x0))) | → | moveleft(Bl1(Ar2(x0))) |
| Cl1(moveleft(Bl1(x0))) | → | moveleft(Bl1(Al1(x0))) |
| Cl2(moveleft(Bl1(x0))) | → | moveleft(Bl1(Al2(x0))) |
| Cb(moveleft(Bl1(x0))) | → | moveleft(Bl1(Ab(x0))) |
| Cr1(moveleft(Bl2(x0))) | → | moveleft(Bl2(Ar1(x0))) |
| Ca(moveleft(Bl2(x0))) | → | moveleft(Bl2(Aa(x0))) |
| Cr2(moveleft(Bl2(x0))) | → | moveleft(Bl2(Ar2(x0))) |
| Cl1(moveleft(Bl2(x0))) | → | moveleft(Bl2(Al1(x0))) |
| Cl2(moveleft(Bl2(x0))) | → | moveleft(Bl2(Al2(x0))) |
| Cb(moveleft(Bl2(x0))) | → | moveleft(Bl2(Ab(x0))) |
| Cr1(moveleft(Bb(x0))) | → | moveleft(Bb(Ar1(x0))) |
| Ca(moveleft(Bb(x0))) | → | moveleft(Bb(Aa(x0))) |
| Cr2(moveleft(Bb(x0))) | → | moveleft(Bb(Ar2(x0))) |
| Cl1(moveleft(Bb(x0))) | → | moveleft(Bb(Al1(x0))) |
| Cl2(moveleft(Bb(x0))) | → | moveleft(Bb(Al2(x0))) |
| Cb(moveleft(Bb(x0))) | → | moveleft(Bb(Ab(x0))) |
| cut(moveleft(Br1(x0))) | → | Dr1(cut(goright(x0))) |
| cut(moveleft(Ba(x0))) | → | Da(cut(goright(x0))) |
| cut(moveleft(Br2(x0))) | → | Dr2(cut(goright(x0))) |
| cut(moveleft(Bl1(x0))) | → | Dl1(cut(goright(x0))) |
| cut(moveleft(Bl2(x0))) | → | Dl2(cut(goright(x0))) |
| cut(moveleft(Bb(x0))) | → | Db(cut(goright(x0))) |
| goright(Ar1(x0)) | → | Cr1(goright(x0)) |
| goright(Aa(x0)) | → | Ca(goright(x0)) |
| goright(Ar2(x0)) | → | Cr2(goright(x0)) |
| goright(Al1(x0)) | → | Cl1(goright(x0)) |
| goright(Al2(x0)) | → | Cl2(goright(x0)) |
| goright(Ab(x0)) | → | Cb(goright(x0)) |
| goright(wait(r1(x0))) | → | moveleft(Br1(wait(x0))) |
| goright(wait(a(x0))) | → | moveleft(Ba(wait(x0))) |
| goright(wait(r2(x0))) | → | moveleft(Br2(wait(x0))) |
| goright(wait(l1(x0))) | → | moveleft(Bl1(wait(x0))) |
| goright(wait(l2(x0))) | → | moveleft(Bl2(wait(x0))) |
| goright(wait(b(x0))) | → | moveleft(Bb(wait(x0))) |
| goright(wait(end(x0))) | → | finish(end(x0)) |
| Cr1(finish(x0)) | → | finish(r1(x0)) |
| Ca(finish(x0)) | → | finish(a(x0)) |
| Cr2(finish(x0)) | → | finish(r2(x0)) |
| Cl1(finish(x0)) | → | finish(l1(x0)) |
| Cl2(finish(x0)) | → | finish(l2(x0)) |
| Cb(finish(x0)) | → | finish(b(x0)) |
| cut(finish(x0)) | → | finish2(x0) |
| Dr1(finish2(x0)) | → | finish2(r1(x0)) |
| Da(finish2(x0)) | → | finish2(a(x0)) |
| Dr2(finish2(x0)) | → | finish2(r2(x0)) |
| Dl1(finish2(x0)) | → | finish2(l1(x0)) |
| Dl2(finish2(x0)) | → | finish2(l2(x0)) |
| Db(finish2(x0)) | → | finish2(b(x0)) |
| rotate(finish2(x0)) | → | rewrite(x0) |
| rewrite(r1(a(x0))) | → | begin(a(a(a(r1(x0))))) |
| rewrite(r2(a(x0))) | → | begin(a(a(a(r2(x0))))) |
| rewrite(a(l1(x0))) | → | begin(l1(a(a(a(x0))))) |
| rewrite(a(a(l2(x0)))) | → | begin(l2(a(a(x0)))) |
| rewrite(r1(b(x0))) | → | begin(l1(b(x0))) |
| rewrite(r2(b(x0))) | → | begin(l2(a(b(x0)))) |
| rewrite(b(l1(x0))) | → | begin(b(r2(x0))) |
| rewrite(b(l2(x0))) | → | begin(b(r1(x0))) |
| rewrite(a(a(x0))) | → | begin(x0) |