by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| begin(end(x0)) | → | rewrite(end(x0)) |
| begin(log(x0)) | → | rotate(cut(Clog(guess(x0)))) |
| begin(s(x0)) | → | rotate(cut(Cs(guess(x0)))) |
| begin(half(x0)) | → | rotate(cut(Chalf(guess(x0)))) |
| begin(0(x0)) | → | rotate(cut(C0(guess(x0)))) |
| begin(p(x0)) | → | rotate(cut(Cp(guess(x0)))) |
| guess(log(x0)) | → | Clog(guess(x0)) |
| guess(s(x0)) | → | Cs(guess(x0)) |
| guess(half(x0)) | → | Chalf(guess(x0)) |
| guess(0(x0)) | → | C0(guess(x0)) |
| guess(p(x0)) | → | Cp(guess(x0)) |
| guess(log(x0)) | → | moveleft(Blog(wait(x0))) |
| guess(s(x0)) | → | moveleft(Bs(wait(x0))) |
| guess(half(x0)) | → | moveleft(Bhalf(wait(x0))) |
| guess(0(x0)) | → | moveleft(B0(wait(x0))) |
| guess(p(x0)) | → | moveleft(Bp(wait(x0))) |
| guess(end(x0)) | → | finish(end(x0)) |
| Clog(moveleft(Blog(x0))) | → | moveleft(Blog(Alog(x0))) |
| Cs(moveleft(Blog(x0))) | → | moveleft(Blog(As(x0))) |
| Chalf(moveleft(Blog(x0))) | → | moveleft(Blog(Ahalf(x0))) |
| C0(moveleft(Blog(x0))) | → | moveleft(Blog(A0(x0))) |
| Cp(moveleft(Blog(x0))) | → | moveleft(Blog(Ap(x0))) |
| Clog(moveleft(Bs(x0))) | → | moveleft(Bs(Alog(x0))) |
| Cs(moveleft(Bs(x0))) | → | moveleft(Bs(As(x0))) |
| Chalf(moveleft(Bs(x0))) | → | moveleft(Bs(Ahalf(x0))) |
| C0(moveleft(Bs(x0))) | → | moveleft(Bs(A0(x0))) |
| Cp(moveleft(Bs(x0))) | → | moveleft(Bs(Ap(x0))) |
| Clog(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(Alog(x0))) |
| Cs(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(As(x0))) |
| Chalf(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(Ahalf(x0))) |
| C0(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(A0(x0))) |
| Cp(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(Ap(x0))) |
| Clog(moveleft(B0(x0))) | → | moveleft(B0(Alog(x0))) |
| Cs(moveleft(B0(x0))) | → | moveleft(B0(As(x0))) |
| Chalf(moveleft(B0(x0))) | → | moveleft(B0(Ahalf(x0))) |
| C0(moveleft(B0(x0))) | → | moveleft(B0(A0(x0))) |
| Cp(moveleft(B0(x0))) | → | moveleft(B0(Ap(x0))) |
| Clog(moveleft(Bp(x0))) | → | moveleft(Bp(Alog(x0))) |
| Cs(moveleft(Bp(x0))) | → | moveleft(Bp(As(x0))) |
| Chalf(moveleft(Bp(x0))) | → | moveleft(Bp(Ahalf(x0))) |
| C0(moveleft(Bp(x0))) | → | moveleft(Bp(A0(x0))) |
| Cp(moveleft(Bp(x0))) | → | moveleft(Bp(Ap(x0))) |
| cut(moveleft(Blog(x0))) | → | Dlog(cut(goright(x0))) |
| cut(moveleft(Bs(x0))) | → | Ds(cut(goright(x0))) |
| cut(moveleft(Bhalf(x0))) | → | Dhalf(cut(goright(x0))) |
| cut(moveleft(B0(x0))) | → | D0(cut(goright(x0))) |
| cut(moveleft(Bp(x0))) | → | Dp(cut(goright(x0))) |
| goright(Alog(x0)) | → | Clog(goright(x0)) |
| goright(As(x0)) | → | Cs(goright(x0)) |
| goright(Ahalf(x0)) | → | Chalf(goright(x0)) |
| goright(A0(x0)) | → | C0(goright(x0)) |
| goright(Ap(x0)) | → | Cp(goright(x0)) |
| goright(wait(log(x0))) | → | moveleft(Blog(wait(x0))) |
| goright(wait(s(x0))) | → | moveleft(Bs(wait(x0))) |
| goright(wait(half(x0))) | → | moveleft(Bhalf(wait(x0))) |
| goright(wait(0(x0))) | → | moveleft(B0(wait(x0))) |
| goright(wait(p(x0))) | → | moveleft(Bp(wait(x0))) |
| goright(wait(end(x0))) | → | finish(end(x0)) |
| Clog(finish(x0)) | → | finish(log(x0)) |
| Cs(finish(x0)) | → | finish(s(x0)) |
| Chalf(finish(x0)) | → | finish(half(x0)) |
| C0(finish(x0)) | → | finish(0(x0)) |
| Cp(finish(x0)) | → | finish(p(x0)) |
| cut(finish(x0)) | → | finish2(x0) |
| Dlog(finish2(x0)) | → | finish2(log(x0)) |
| Ds(finish2(x0)) | → | finish2(s(x0)) |
| Dhalf(finish2(x0)) | → | finish2(half(x0)) |
| D0(finish2(x0)) | → | finish2(0(x0)) |
| Dp(finish2(x0)) | → | finish2(p(x0)) |
| rotate(finish2(x0)) | → | rewrite(x0) |
| rewrite(log(s(x0))) | → | begin(s(log(half(s(x0))))) |
| rewrite(half(0(x0))) | → | begin(0(s(s(half(x0))))) |
| rewrite(half(s(0(x0)))) | → | begin(0(x0)) |
| rewrite(half(s(s(x0)))) | → | begin(s(half(p(s(s(x0)))))) |
| rewrite(half(half(s(s(s(s(x0))))))) | → | begin(s(s(half(half(x0))))) |
| rewrite(p(s(s(s(x0))))) | → | begin(s(p(s(s(x0))))) |
| rewrite(s(s(p(s(x0))))) | → | begin(s(s(x0))) |
| rewrite(0(x0)) | → | begin(x0) |
| begin(end(x0)) | → | rewrite(end(x0)) |
| begin(log(x0)) | → | rotate(cut(Clog(guess(x0)))) |
| begin(s(x0)) | → | rotate(cut(Cs(guess(x0)))) |
| begin(half(x0)) | → | rotate(cut(Chalf(guess(x0)))) |
| begin(0(x0)) | → | rotate(cut(C0(guess(x0)))) |
| begin(p(x0)) | → | rotate(cut(Cp(guess(x0)))) |
| guess(log(x0)) | → | Clog(guess(x0)) |
| guess(s(x0)) | → | Cs(guess(x0)) |
| guess(half(x0)) | → | Chalf(guess(x0)) |
| guess(0(x0)) | → | C0(guess(x0)) |
| guess(p(x0)) | → | Cp(guess(x0)) |
| guess(log(x0)) | → | moveleft(Blog(wait(x0))) |
| guess(s(x0)) | → | moveleft(Bs(wait(x0))) |
| guess(half(x0)) | → | moveleft(Bhalf(wait(x0))) |
| guess(0(x0)) | → | moveleft(B0(wait(x0))) |
| guess(p(x0)) | → | moveleft(Bp(wait(x0))) |
| guess(end(x0)) | → | finish(end(x0)) |
| Clog(moveleft(Blog(x0))) | → | moveleft(Blog(Alog(x0))) |
| Cs(moveleft(Blog(x0))) | → | moveleft(Blog(As(x0))) |
| Chalf(moveleft(Blog(x0))) | → | moveleft(Blog(Ahalf(x0))) |
| C0(moveleft(Blog(x0))) | → | moveleft(Blog(A0(x0))) |
| Cp(moveleft(Blog(x0))) | → | moveleft(Blog(Ap(x0))) |
| Clog(moveleft(Bs(x0))) | → | moveleft(Bs(Alog(x0))) |
| Cs(moveleft(Bs(x0))) | → | moveleft(Bs(As(x0))) |
| Chalf(moveleft(Bs(x0))) | → | moveleft(Bs(Ahalf(x0))) |
| C0(moveleft(Bs(x0))) | → | moveleft(Bs(A0(x0))) |
| Cp(moveleft(Bs(x0))) | → | moveleft(Bs(Ap(x0))) |
| Clog(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(Alog(x0))) |
| Cs(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(As(x0))) |
| Chalf(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(Ahalf(x0))) |
| C0(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(A0(x0))) |
| Cp(moveleft(Bhalf(x0))) | → | moveleft(Bhalf(Ap(x0))) |
| Clog(moveleft(B0(x0))) | → | moveleft(B0(Alog(x0))) |
| Cs(moveleft(B0(x0))) | → | moveleft(B0(As(x0))) |
| Chalf(moveleft(B0(x0))) | → | moveleft(B0(Ahalf(x0))) |
| C0(moveleft(B0(x0))) | → | moveleft(B0(A0(x0))) |
| Cp(moveleft(B0(x0))) | → | moveleft(B0(Ap(x0))) |
| Clog(moveleft(Bp(x0))) | → | moveleft(Bp(Alog(x0))) |
| Cs(moveleft(Bp(x0))) | → | moveleft(Bp(As(x0))) |
| Chalf(moveleft(Bp(x0))) | → | moveleft(Bp(Ahalf(x0))) |
| C0(moveleft(Bp(x0))) | → | moveleft(Bp(A0(x0))) |
| Cp(moveleft(Bp(x0))) | → | moveleft(Bp(Ap(x0))) |
| cut(moveleft(Blog(x0))) | → | Dlog(cut(goright(x0))) |
| cut(moveleft(Bs(x0))) | → | Ds(cut(goright(x0))) |
| cut(moveleft(Bhalf(x0))) | → | Dhalf(cut(goright(x0))) |
| cut(moveleft(B0(x0))) | → | D0(cut(goright(x0))) |
| cut(moveleft(Bp(x0))) | → | Dp(cut(goright(x0))) |
| goright(Alog(x0)) | → | Clog(goright(x0)) |
| goright(As(x0)) | → | Cs(goright(x0)) |
| goright(Ahalf(x0)) | → | Chalf(goright(x0)) |
| goright(A0(x0)) | → | C0(goright(x0)) |
| goright(Ap(x0)) | → | Cp(goright(x0)) |
| goright(wait(log(x0))) | → | moveleft(Blog(wait(x0))) |
| goright(wait(s(x0))) | → | moveleft(Bs(wait(x0))) |
| goright(wait(half(x0))) | → | moveleft(Bhalf(wait(x0))) |
| goright(wait(0(x0))) | → | moveleft(B0(wait(x0))) |
| goright(wait(p(x0))) | → | moveleft(Bp(wait(x0))) |
| goright(wait(end(x0))) | → | finish(end(x0)) |
| Clog(finish(x0)) | → | finish(log(x0)) |
| Cs(finish(x0)) | → | finish(s(x0)) |
| Chalf(finish(x0)) | → | finish(half(x0)) |
| C0(finish(x0)) | → | finish(0(x0)) |
| Cp(finish(x0)) | → | finish(p(x0)) |
| cut(finish(x0)) | → | finish2(x0) |
| Dlog(finish2(x0)) | → | finish2(log(x0)) |
| Ds(finish2(x0)) | → | finish2(s(x0)) |
| Dhalf(finish2(x0)) | → | finish2(half(x0)) |
| D0(finish2(x0)) | → | finish2(0(x0)) |
| Dp(finish2(x0)) | → | finish2(p(x0)) |
| rotate(finish2(x0)) | → | rewrite(x0) |
| rewrite(log(s(x0))) | → | begin(s(log(half(s(x0))))) |
| rewrite(half(0(x0))) | → | begin(0(s(s(half(x0))))) |
| rewrite(half(s(0(x0)))) | → | begin(0(x0)) |
| rewrite(half(s(s(x0)))) | → | begin(s(half(p(s(s(x0)))))) |
| rewrite(half(half(s(s(s(s(x0))))))) | → | begin(s(s(half(half(x0))))) |
| rewrite(p(s(s(s(x0))))) | → | begin(s(p(s(s(x0))))) |
| rewrite(s(s(p(s(x0))))) | → | begin(s(s(x0))) |
| rewrite(0(x0)) | → | begin(x0) |