by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(e(x0)) | → | Wait(Right1(x0)) |
| Begin(t(x0)) | → | Wait(Right2(x0)) |
| Begin(w(x0)) | → | Wait(Right3(x0)) |
| Begin(e(x0)) | → | Wait(Right4(x0)) |
| Begin(r(x0)) | → | Wait(Right5(x0)) |
| Begin(r(x0)) | → | Wait(Right6(x0)) |
| Begin(i(t(e(r(x0))))) | → | Wait(Right7(x0)) |
| Begin(t(e(r(x0)))) | → | Wait(Right8(x0)) |
| Begin(e(r(x0))) | → | Wait(Right9(x0)) |
| Begin(r(x0)) | → | Wait(Right10(x0)) |
| Right1(r(End(x0))) | → | Left(w(r(End(x0)))) |
| Right2(i(End(x0))) | → | Left(e(r(End(x0)))) |
| Right3(e(End(x0))) | → | Left(r(i(End(x0)))) |
| Right4(t(End(x0))) | → | Left(r(e(End(x0)))) |
| Right5(w(End(x0))) | → | Left(i(t(End(x0)))) |
| Right6(e(End(x0))) | → | Left(e(w(End(x0)))) |
| Right7(r(End(x0))) | → | Left(e(w(r(i(t(e(End(x0)))))))) |
| Right8(r(i(End(x0)))) | → | Left(e(w(r(i(t(e(End(x0)))))))) |
| Right9(r(i(t(End(x0))))) | → | Left(e(w(r(i(t(e(End(x0)))))))) |
| Right10(r(i(t(e(End(x0)))))) | → | Left(e(w(r(i(t(e(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)) |
| Right1(e(x0)) | → | Ae(Right1(x0)) |
| Right2(e(x0)) | → | Ae(Right2(x0)) |
| Right3(e(x0)) | → | Ae(Right3(x0)) |
| Right4(e(x0)) | → | Ae(Right4(x0)) |
| Right5(e(x0)) | → | Ae(Right5(x0)) |
| Right6(e(x0)) | → | Ae(Right6(x0)) |
| Right7(e(x0)) | → | Ae(Right7(x0)) |
| Right8(e(x0)) | → | Ae(Right8(x0)) |
| Right9(e(x0)) | → | Ae(Right9(x0)) |
| Right10(e(x0)) | → | Ae(Right10(x0)) |
| Right1(w(x0)) | → | Aw(Right1(x0)) |
| Right2(w(x0)) | → | Aw(Right2(x0)) |
| Right3(w(x0)) | → | Aw(Right3(x0)) |
| Right4(w(x0)) | → | Aw(Right4(x0)) |
| Right5(w(x0)) | → | Aw(Right5(x0)) |
| Right6(w(x0)) | → | Aw(Right6(x0)) |
| Right7(w(x0)) | → | Aw(Right7(x0)) |
| Right8(w(x0)) | → | Aw(Right8(x0)) |
| Right9(w(x0)) | → | Aw(Right9(x0)) |
| Right10(w(x0)) | → | Aw(Right10(x0)) |
| Right1(i(x0)) | → | Ai(Right1(x0)) |
| Right2(i(x0)) | → | Ai(Right2(x0)) |
| Right3(i(x0)) | → | Ai(Right3(x0)) |
| Right4(i(x0)) | → | Ai(Right4(x0)) |
| Right5(i(x0)) | → | Ai(Right5(x0)) |
| Right6(i(x0)) | → | Ai(Right6(x0)) |
| Right7(i(x0)) | → | Ai(Right7(x0)) |
| Right8(i(x0)) | → | Ai(Right8(x0)) |
| Right9(i(x0)) | → | Ai(Right9(x0)) |
| Right10(i(x0)) | → | Ai(Right10(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)) |
| Ar(Left(x0)) | → | Left(r(x0)) |
| Ae(Left(x0)) | → | Left(e(x0)) |
| Aw(Left(x0)) | → | Left(w(x0)) |
| Ai(Left(x0)) | → | Left(i(x0)) |
| At(Left(x0)) | → | Left(t(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| r(e(x0)) | → | w(r(x0)) |
| i(t(x0)) | → | e(r(x0)) |
| e(w(x0)) | → | r(i(x0)) |
| t(e(x0)) | → | r(e(x0)) |
| w(r(x0)) | → | i(t(x0)) |
| e(r(x0)) | → | e(w(x0)) |
| r(i(t(e(r(x0))))) | → | e(w(r(i(t(e(x0)))))) |
| Begin(e(x0)) | → | Wait(Right1(x0)) |
| Begin(t(x0)) | → | Wait(Right2(x0)) |
| Begin(w(x0)) | → | Wait(Right3(x0)) |
| Begin(e(x0)) | → | Wait(Right4(x0)) |
| Begin(r(x0)) | → | Wait(Right5(x0)) |
| Begin(r(x0)) | → | Wait(Right6(x0)) |
| Begin(i(t(e(r(x0))))) | → | Wait(Right7(x0)) |
| Begin(t(e(r(x0)))) | → | Wait(Right8(x0)) |
| Begin(e(r(x0))) | → | Wait(Right9(x0)) |
| Begin(r(x0)) | → | Wait(Right10(x0)) |
| Right1(r(End(x0))) | → | Left(w(r(End(x0)))) |
| Right2(i(End(x0))) | → | Left(e(r(End(x0)))) |
| Right3(e(End(x0))) | → | Left(r(i(End(x0)))) |
| Right4(t(End(x0))) | → | Left(r(e(End(x0)))) |
| Right5(w(End(x0))) | → | Left(i(t(End(x0)))) |
| Right6(e(End(x0))) | → | Left(e(w(End(x0)))) |
| Right7(r(End(x0))) | → | Left(e(w(r(i(t(e(End(x0)))))))) |
| Right8(r(i(End(x0)))) | → | Left(e(w(r(i(t(e(End(x0)))))))) |
| Right9(r(i(t(End(x0))))) | → | Left(e(w(r(i(t(e(End(x0)))))))) |
| Right10(r(i(t(e(End(x0)))))) | → | Left(e(w(r(i(t(e(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)) |
| Right1(e(x0)) | → | Ae(Right1(x0)) |
| Right2(e(x0)) | → | Ae(Right2(x0)) |
| Right3(e(x0)) | → | Ae(Right3(x0)) |
| Right4(e(x0)) | → | Ae(Right4(x0)) |
| Right5(e(x0)) | → | Ae(Right5(x0)) |
| Right6(e(x0)) | → | Ae(Right6(x0)) |
| Right7(e(x0)) | → | Ae(Right7(x0)) |
| Right8(e(x0)) | → | Ae(Right8(x0)) |
| Right9(e(x0)) | → | Ae(Right9(x0)) |
| Right10(e(x0)) | → | Ae(Right10(x0)) |
| Right1(w(x0)) | → | Aw(Right1(x0)) |
| Right2(w(x0)) | → | Aw(Right2(x0)) |
| Right3(w(x0)) | → | Aw(Right3(x0)) |
| Right4(w(x0)) | → | Aw(Right4(x0)) |
| Right5(w(x0)) | → | Aw(Right5(x0)) |
| Right6(w(x0)) | → | Aw(Right6(x0)) |
| Right7(w(x0)) | → | Aw(Right7(x0)) |
| Right8(w(x0)) | → | Aw(Right8(x0)) |
| Right9(w(x0)) | → | Aw(Right9(x0)) |
| Right10(w(x0)) | → | Aw(Right10(x0)) |
| Right1(i(x0)) | → | Ai(Right1(x0)) |
| Right2(i(x0)) | → | Ai(Right2(x0)) |
| Right3(i(x0)) | → | Ai(Right3(x0)) |
| Right4(i(x0)) | → | Ai(Right4(x0)) |
| Right5(i(x0)) | → | Ai(Right5(x0)) |
| Right6(i(x0)) | → | Ai(Right6(x0)) |
| Right7(i(x0)) | → | Ai(Right7(x0)) |
| Right8(i(x0)) | → | Ai(Right8(x0)) |
| Right9(i(x0)) | → | Ai(Right9(x0)) |
| Right10(i(x0)) | → | Ai(Right10(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)) |
| Ar(Left(x0)) | → | Left(r(x0)) |
| Ae(Left(x0)) | → | Left(e(x0)) |
| Aw(Left(x0)) | → | Left(w(x0)) |
| Ai(Left(x0)) | → | Left(i(x0)) |
| At(Left(x0)) | → | Left(t(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| r(e(x0)) | → | w(r(x0)) |
| i(t(x0)) | → | e(r(x0)) |
| e(w(x0)) | → | r(i(x0)) |
| t(e(x0)) | → | r(e(x0)) |
| w(r(x0)) | → | i(t(x0)) |
| e(r(x0)) | → | e(w(x0)) |
| r(i(t(e(r(x0))))) | → | e(w(r(i(t(e(x0)))))) |