by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(s(x0)) | → | Wait(Right1(x0)) |
| Begin(u(x0)) | → | Wait(Right2(x0)) |
| Begin(u(x0)) | → | Wait(Right3(x0)) |
| Begin(u(x0)) | → | Wait(Right4(x0)) |
| Begin(u(x0)) | → | Wait(Right5(x0)) |
| Begin(s(x0)) | → | Wait(Right6(x0)) |
| Begin(r(x0)) | → | Wait(Right7(x0)) |
| Begin(n(x0)) | → | Wait(Right8(x0)) |
| Right1(r(End(x0))) | → | Left(s(r(End(x0)))) |
| Right2(r(End(x0))) | → | Left(u(r(End(x0)))) |
| Right3(s(End(x0))) | → | Left(u(s(End(x0)))) |
| Right4(n(End(x0))) | → | Left(u(n(End(x0)))) |
| Right5(c(End(x0))) | → | Left(u(c(End(x0)))) |
| Right6(c(End(x0))) | → | Left(s(c(End(x0)))) |
| Right7(c(End(x0))) | → | Left(r(c(End(x0)))) |
| Right8(c(End(x0))) | → | Left(n(c(End(x0)))) |
| Right1(r(x0)) | → | Ar(Right1(x0)) |
| Right2(r(x0)) | → | Ar(Right2(x0)) |
| Right3(r(x0)) | → | Ar(Right3(x0)) |
| Right4(r(x0)) | → | Ar(Right4(x0)) |
| Right5(r(x0)) | → | Ar(Right5(x0)) |
| Right6(r(x0)) | → | Ar(Right6(x0)) |
| Right7(r(x0)) | → | Ar(Right7(x0)) |
| Right8(r(x0)) | → | Ar(Right8(x0)) |
| Right1(s(x0)) | → | As(Right1(x0)) |
| Right2(s(x0)) | → | As(Right2(x0)) |
| Right3(s(x0)) | → | As(Right3(x0)) |
| Right4(s(x0)) | → | As(Right4(x0)) |
| Right5(s(x0)) | → | As(Right5(x0)) |
| Right6(s(x0)) | → | As(Right6(x0)) |
| Right7(s(x0)) | → | As(Right7(x0)) |
| Right8(s(x0)) | → | As(Right8(x0)) |
| Right1(u(x0)) | → | Au(Right1(x0)) |
| Right2(u(x0)) | → | Au(Right2(x0)) |
| Right3(u(x0)) | → | Au(Right3(x0)) |
| Right4(u(x0)) | → | Au(Right4(x0)) |
| Right5(u(x0)) | → | Au(Right5(x0)) |
| Right6(u(x0)) | → | Au(Right6(x0)) |
| Right7(u(x0)) | → | Au(Right7(x0)) |
| Right8(u(x0)) | → | Au(Right8(x0)) |
| Right1(n(x0)) | → | An(Right1(x0)) |
| Right2(n(x0)) | → | An(Right2(x0)) |
| Right3(n(x0)) | → | An(Right3(x0)) |
| Right4(n(x0)) | → | An(Right4(x0)) |
| Right5(n(x0)) | → | An(Right5(x0)) |
| Right6(n(x0)) | → | An(Right6(x0)) |
| Right7(n(x0)) | → | An(Right7(x0)) |
| Right8(n(x0)) | → | An(Right8(x0)) |
| Right1(c(x0)) | → | Ac(Right1(x0)) |
| Right2(c(x0)) | → | Ac(Right2(x0)) |
| Right3(c(x0)) | → | Ac(Right3(x0)) |
| Right4(c(x0)) | → | Ac(Right4(x0)) |
| Right5(c(x0)) | → | Ac(Right5(x0)) |
| Right6(c(x0)) | → | Ac(Right6(x0)) |
| Right7(c(x0)) | → | Ac(Right7(x0)) |
| Right8(c(x0)) | → | Ac(Right8(x0)) |
| Ar(Left(x0)) | → | Left(r(x0)) |
| As(Left(x0)) | → | Left(s(x0)) |
| Au(Left(x0)) | → | Left(u(x0)) |
| An(Left(x0)) | → | Left(n(x0)) |
| Ac(Left(x0)) | → | Left(c(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| r(s(x0)) | → | s(r(x0)) |
| r(u(x0)) | → | u(r(x0)) |
| s(u(x0)) | → | u(s(x0)) |
| n(u(x0)) | → | u(n(x0)) |
| c(u(x0)) | → | u(c(x0)) |
| c(s(x0)) | → | s(c(x0)) |
| c(r(x0)) | → | r(c(x0)) |
| c(n(x0)) | → | n(c(x0)) |
| t0 | = | Begin(s(r(End(x10929)))) |
| →ε | Wait(Right1(r(End(x10929)))) | |
| →1 | Wait(Left(s(r(End(x10929))))) | |
| →ε | Begin(s(r(End(x10929)))) | |
| = | t3 |