by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(r(x0)) | → | Wait(Right1(x0)) |
| Begin(s(x0)) | → | Wait(Right2(x0)) |
| Begin(n(x0)) | → | Wait(Right3(x0)) |
| Begin(b(x0)) | → | Wait(Right4(x0)) |
| Begin(u(x0)) | → | Wait(Right5(x0)) |
| Begin(u(x0)) | → | Wait(Right6(x0)) |
| Begin(u(x0)) | → | Wait(Right7(x0)) |
| Begin(r(u(x0))) | → | Wait(Right8(x0)) |
| Begin(u(x0)) | → | Wait(Right9(x0)) |
| Begin(s(u(x0))) | → | Wait(Right10(x0)) |
| Begin(u(x0)) | → | Wait(Right11(x0)) |
| Begin(n(u(x0))) | → | Wait(Right12(x0)) |
| Begin(u(x0)) | → | Wait(Right13(x0)) |
| Begin(u(x0)) | → | Wait(Right14(x0)) |
| Begin(s(x0)) | → | Wait(Right15(x0)) |
| Begin(r(x0)) | → | Wait(Right16(x0)) |
| Begin(n(x0)) | → | Wait(Right17(x0)) |
| Begin(n(x0)) | → | Wait(Right18(x0)) |
| Right1(r(End(x0))) | → | Left(s(r(End(x0)))) |
| Right2(r(End(x0))) | → | Left(s(r(End(x0)))) |
| Right3(r(End(x0))) | → | Left(s(r(End(x0)))) |
| Right4(r(End(x0))) | → | Left(u(s(b(End(x0))))) |
| Right5(r(End(x0))) | → | Left(u(r(End(x0)))) |
| Right6(s(End(x0))) | → | Left(u(s(End(x0)))) |
| Right7(n(End(x0))) | → | Left(u(n(End(x0)))) |
| Right8(t(End(x0))) | → | Left(t(c(r(End(x0))))) |
| Right9(t(r(End(x0)))) | → | Left(t(c(r(End(x0))))) |
| Right10(t(End(x0))) | → | Left(t(c(r(End(x0))))) |
| Right11(t(s(End(x0)))) | → | Left(t(c(r(End(x0))))) |
| Right12(t(End(x0))) | → | Left(t(c(r(End(x0))))) |
| Right13(t(n(End(x0)))) | → | Left(t(c(r(End(x0))))) |
| Right14(c(End(x0))) | → | Left(u(c(End(x0)))) |
| Right15(c(End(x0))) | → | Left(s(c(End(x0)))) |
| Right16(c(End(x0))) | → | Left(r(c(End(x0)))) |
| Right17(c(End(x0))) | → | Left(n(c(End(x0)))) |
| Right18(c(End(x0))) | → | Left(n(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)) |
| Right9(r(x0)) | → | Ar(Right9(x0)) |
| Right10(r(x0)) | → | Ar(Right10(x0)) |
| Right11(r(x0)) | → | Ar(Right11(x0)) |
| Right12(r(x0)) | → | Ar(Right12(x0)) |
| Right13(r(x0)) | → | Ar(Right13(x0)) |
| Right14(r(x0)) | → | Ar(Right14(x0)) |
| Right15(r(x0)) | → | Ar(Right15(x0)) |
| Right16(r(x0)) | → | Ar(Right16(x0)) |
| Right17(r(x0)) | → | Ar(Right17(x0)) |
| Right18(r(x0)) | → | Ar(Right18(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)) |
| Right9(s(x0)) | → | As(Right9(x0)) |
| Right10(s(x0)) | → | As(Right10(x0)) |
| Right11(s(x0)) | → | As(Right11(x0)) |
| Right12(s(x0)) | → | As(Right12(x0)) |
| Right13(s(x0)) | → | As(Right13(x0)) |
| Right14(s(x0)) | → | As(Right14(x0)) |
| Right15(s(x0)) | → | As(Right15(x0)) |
| Right16(s(x0)) | → | As(Right16(x0)) |
| Right17(s(x0)) | → | As(Right17(x0)) |
| Right18(s(x0)) | → | As(Right18(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)) |
| Right9(n(x0)) | → | An(Right9(x0)) |
| Right10(n(x0)) | → | An(Right10(x0)) |
| Right11(n(x0)) | → | An(Right11(x0)) |
| Right12(n(x0)) | → | An(Right12(x0)) |
| Right13(n(x0)) | → | An(Right13(x0)) |
| Right14(n(x0)) | → | An(Right14(x0)) |
| Right15(n(x0)) | → | An(Right15(x0)) |
| Right16(n(x0)) | → | An(Right16(x0)) |
| Right17(n(x0)) | → | An(Right17(x0)) |
| Right18(n(x0)) | → | An(Right18(x0)) |
| Right1(b(x0)) | → | Ab(Right1(x0)) |
| Right2(b(x0)) | → | Ab(Right2(x0)) |
| Right3(b(x0)) | → | Ab(Right3(x0)) |
| Right4(b(x0)) | → | Ab(Right4(x0)) |
| Right5(b(x0)) | → | Ab(Right5(x0)) |
| Right6(b(x0)) | → | Ab(Right6(x0)) |
| Right7(b(x0)) | → | Ab(Right7(x0)) |
| Right8(b(x0)) | → | Ab(Right8(x0)) |
| Right9(b(x0)) | → | Ab(Right9(x0)) |
| Right10(b(x0)) | → | Ab(Right10(x0)) |
| Right11(b(x0)) | → | Ab(Right11(x0)) |
| Right12(b(x0)) | → | Ab(Right12(x0)) |
| Right13(b(x0)) | → | Ab(Right13(x0)) |
| Right14(b(x0)) | → | Ab(Right14(x0)) |
| Right15(b(x0)) | → | Ab(Right15(x0)) |
| Right16(b(x0)) | → | Ab(Right16(x0)) |
| Right17(b(x0)) | → | Ab(Right17(x0)) |
| Right18(b(x0)) | → | Ab(Right18(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)) |
| Right9(u(x0)) | → | Au(Right9(x0)) |
| Right10(u(x0)) | → | Au(Right10(x0)) |
| Right11(u(x0)) | → | Au(Right11(x0)) |
| Right12(u(x0)) | → | Au(Right12(x0)) |
| Right13(u(x0)) | → | Au(Right13(x0)) |
| Right14(u(x0)) | → | Au(Right14(x0)) |
| Right15(u(x0)) | → | Au(Right15(x0)) |
| Right16(u(x0)) | → | Au(Right16(x0)) |
| Right17(u(x0)) | → | Au(Right17(x0)) |
| Right18(u(x0)) | → | Au(Right18(x0)) |
| Right1(t(x0)) | → | At(Right1(x0)) |
| Right2(t(x0)) | → | At(Right2(x0)) |
| Right3(t(x0)) | → | At(Right3(x0)) |
| Right4(t(x0)) | → | At(Right4(x0)) |
| Right5(t(x0)) | → | At(Right5(x0)) |
| Right6(t(x0)) | → | At(Right6(x0)) |
| Right7(t(x0)) | → | At(Right7(x0)) |
| Right8(t(x0)) | → | At(Right8(x0)) |
| Right9(t(x0)) | → | At(Right9(x0)) |
| Right10(t(x0)) | → | At(Right10(x0)) |
| Right11(t(x0)) | → | At(Right11(x0)) |
| Right12(t(x0)) | → | At(Right12(x0)) |
| Right13(t(x0)) | → | At(Right13(x0)) |
| Right14(t(x0)) | → | At(Right14(x0)) |
| Right15(t(x0)) | → | At(Right15(x0)) |
| Right16(t(x0)) | → | At(Right16(x0)) |
| Right17(t(x0)) | → | At(Right17(x0)) |
| Right18(t(x0)) | → | At(Right18(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)) |
| Right9(c(x0)) | → | Ac(Right9(x0)) |
| Right10(c(x0)) | → | Ac(Right10(x0)) |
| Right11(c(x0)) | → | Ac(Right11(x0)) |
| Right12(c(x0)) | → | Ac(Right12(x0)) |
| Right13(c(x0)) | → | Ac(Right13(x0)) |
| Right14(c(x0)) | → | Ac(Right14(x0)) |
| Right15(c(x0)) | → | Ac(Right15(x0)) |
| Right16(c(x0)) | → | Ac(Right16(x0)) |
| Right17(c(x0)) | → | Ac(Right17(x0)) |
| Right18(c(x0)) | → | Ac(Right18(x0)) |
| Ar(Left(x0)) | → | Left(r(x0)) |
| As(Left(x0)) | → | Left(s(x0)) |
| An(Left(x0)) | → | Left(n(x0)) |
| Ab(Left(x0)) | → | Left(b(x0)) |
| Au(Left(x0)) | → | Left(u(x0)) |
| At(Left(x0)) | → | Left(t(x0)) |
| Ac(Left(x0)) | → | Left(c(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| r(r(x0)) | → | s(r(x0)) |
| r(s(x0)) | → | s(r(x0)) |
| r(n(x0)) | → | s(r(x0)) |
| r(b(x0)) | → | u(s(b(x0))) |
| r(u(x0)) | → | u(r(x0)) |
| s(u(x0)) | → | u(s(x0)) |
| n(u(x0)) | → | u(n(x0)) |
| t(r(u(x0))) | → | t(c(r(x0))) |
| t(s(u(x0))) | → | t(c(r(x0))) |
| t(n(u(x0))) | → | t(c(r(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)) |
| c(n(x0)) | → | n(x0) |
| t0 | = | Begin(s(r(End(x81975)))) |
| →ε | Wait(Right2(r(End(x81975)))) | |
| →1 | Wait(Left(s(r(End(x81975))))) | |
| →ε | Begin(s(r(End(x81975)))) | |
| = | t3 |