by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(0(*(*(x0)))) | → | Wait(Right1(x0)) |
| Begin(*(*(x0))) | → | Wait(Right2(x0)) |
| Begin(*(x0)) | → | Wait(Right3(x0)) |
| Begin(1(*(*(x0)))) | → | Wait(Right4(x0)) |
| Begin(*(*(x0))) | → | Wait(Right5(x0)) |
| Begin(*(x0)) | → | Wait(Right6(x0)) |
| Begin(#(0(0(x0)))) | → | Wait(Right7(x0)) |
| Begin(0(0(x0))) | → | Wait(Right8(x0)) |
| Begin(0(x0)) | → | Wait(Right9(x0)) |
| Begin(#(1(1(x0)))) | → | Wait(Right10(x0)) |
| Begin(1(1(x0))) | → | Wait(Right11(x0)) |
| Begin(1(x0)) | → | Wait(Right12(x0)) |
| Begin(#($($(x0)))) | → | Wait(Right13(x0)) |
| Begin($($(x0))) | → | Wait(Right14(x0)) |
| Begin($(x0)) | → | Wait(Right15(x0)) |
| Right1(0(End(x0))) | → | Left(*(*(1(1(End(x0)))))) |
| Right2(0(0(End(x0)))) | → | Left(*(*(1(1(End(x0)))))) |
| Right3(0(0(*(End(x0))))) | → | Left(*(*(1(1(End(x0)))))) |
| Right4(1(End(x0))) | → | Left(0(0(#(#(End(x0)))))) |
| Right5(1(1(End(x0)))) | → | Left(0(0(#(#(End(x0)))))) |
| Right6(1(1(*(End(x0))))) | → | Left(0(0(#(#(End(x0)))))) |
| Right7(#(End(x0))) | → | Left(0(0(#(#(End(x0)))))) |
| Right8(#(#(End(x0)))) | → | Left(0(0(#(#(End(x0)))))) |
| Right9(#(#(0(End(x0))))) | → | Left(0(0(#(#(End(x0)))))) |
| Right10(#(End(x0))) | → | Left(1(1(#(#(End(x0)))))) |
| Right11(#(#(End(x0)))) | → | Left(1(1(#(#(End(x0)))))) |
| Right12(#(#(1(End(x0))))) | → | Left(1(1(#(#(End(x0)))))) |
| Right13(#(End(x0))) | → | Left(*(*($($(End(x0)))))) |
| Right14(#(#(End(x0)))) | → | Left(*(*($($(End(x0)))))) |
| Right15(#(#($(End(x0))))) | → | Left(*(*($($(End(x0)))))) |
| Right1(0(x0)) | → | A0(Right1(x0)) |
| Right2(0(x0)) | → | A0(Right2(x0)) |
| Right3(0(x0)) | → | A0(Right3(x0)) |
| Right4(0(x0)) | → | A0(Right4(x0)) |
| Right5(0(x0)) | → | A0(Right5(x0)) |
| Right6(0(x0)) | → | A0(Right6(x0)) |
| Right7(0(x0)) | → | A0(Right7(x0)) |
| Right8(0(x0)) | → | A0(Right8(x0)) |
| Right9(0(x0)) | → | A0(Right9(x0)) |
| Right10(0(x0)) | → | A0(Right10(x0)) |
| Right11(0(x0)) | → | A0(Right11(x0)) |
| Right12(0(x0)) | → | A0(Right12(x0)) |
| Right13(0(x0)) | → | A0(Right13(x0)) |
| Right14(0(x0)) | → | A0(Right14(x0)) |
| Right15(0(x0)) | → | A0(Right15(x0)) |
| Right1(*(x0)) | → | A*(Right1(x0)) |
| Right2(*(x0)) | → | A*(Right2(x0)) |
| Right3(*(x0)) | → | A*(Right3(x0)) |
| Right4(*(x0)) | → | A*(Right4(x0)) |
| Right5(*(x0)) | → | A*(Right5(x0)) |
| Right6(*(x0)) | → | A*(Right6(x0)) |
| Right7(*(x0)) | → | A*(Right7(x0)) |
| Right8(*(x0)) | → | A*(Right8(x0)) |
| Right9(*(x0)) | → | A*(Right9(x0)) |
| Right10(*(x0)) | → | A*(Right10(x0)) |
| Right11(*(x0)) | → | A*(Right11(x0)) |
| Right12(*(x0)) | → | A*(Right12(x0)) |
| Right13(*(x0)) | → | A*(Right13(x0)) |
| Right14(*(x0)) | → | A*(Right14(x0)) |
| Right15(*(x0)) | → | A*(Right15(x0)) |
| Right1(1(x0)) | → | A1(Right1(x0)) |
| Right2(1(x0)) | → | A1(Right2(x0)) |
| Right3(1(x0)) | → | A1(Right3(x0)) |
| Right4(1(x0)) | → | A1(Right4(x0)) |
| Right5(1(x0)) | → | A1(Right5(x0)) |
| Right6(1(x0)) | → | A1(Right6(x0)) |
| Right7(1(x0)) | → | A1(Right7(x0)) |
| Right8(1(x0)) | → | A1(Right8(x0)) |
| Right9(1(x0)) | → | A1(Right9(x0)) |
| Right10(1(x0)) | → | A1(Right10(x0)) |
| Right11(1(x0)) | → | A1(Right11(x0)) |
| Right12(1(x0)) | → | A1(Right12(x0)) |
| Right13(1(x0)) | → | A1(Right13(x0)) |
| Right14(1(x0)) | → | A1(Right14(x0)) |
| Right15(1(x0)) | → | A1(Right15(x0)) |
| Right1(#(x0)) | → | A#(Right1(x0)) |
| Right2(#(x0)) | → | A#(Right2(x0)) |
| Right3(#(x0)) | → | A#(Right3(x0)) |
| Right4(#(x0)) | → | A#(Right4(x0)) |
| Right5(#(x0)) | → | A#(Right5(x0)) |
| Right6(#(x0)) | → | A#(Right6(x0)) |
| Right7(#(x0)) | → | A#(Right7(x0)) |
| Right8(#(x0)) | → | A#(Right8(x0)) |
| Right9(#(x0)) | → | A#(Right9(x0)) |
| Right10(#(x0)) | → | A#(Right10(x0)) |
| Right11(#(x0)) | → | A#(Right11(x0)) |
| Right12(#(x0)) | → | A#(Right12(x0)) |
| Right13(#(x0)) | → | A#(Right13(x0)) |
| Right14(#(x0)) | → | A#(Right14(x0)) |
| Right15(#(x0)) | → | A#(Right15(x0)) |
| Right1($(x0)) | → | A$(Right1(x0)) |
| Right2($(x0)) | → | A$(Right2(x0)) |
| Right3($(x0)) | → | A$(Right3(x0)) |
| Right4($(x0)) | → | A$(Right4(x0)) |
| Right5($(x0)) | → | A$(Right5(x0)) |
| Right6($(x0)) | → | A$(Right6(x0)) |
| Right7($(x0)) | → | A$(Right7(x0)) |
| Right8($(x0)) | → | A$(Right8(x0)) |
| Right9($(x0)) | → | A$(Right9(x0)) |
| Right10($(x0)) | → | A$(Right10(x0)) |
| Right11($(x0)) | → | A$(Right11(x0)) |
| Right12($(x0)) | → | A$(Right12(x0)) |
| Right13($(x0)) | → | A$(Right13(x0)) |
| Right14($(x0)) | → | A$(Right14(x0)) |
| Right15($(x0)) | → | A$(Right15(x0)) |
| A0(Left(x0)) | → | Left(0(x0)) |
| A*(Left(x0)) | → | Left(*(x0)) |
| A1(Left(x0)) | → | Left(1(x0)) |
| A#(Left(x0)) | → | Left(#(x0)) |
| A$(Left(x0)) | → | Left($(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| 0(0(*(*(x0)))) | → | *(*(1(1(x0)))) |
| 1(1(*(*(x0)))) | → | 0(0(#(#(x0)))) |
| #(#(0(0(x0)))) | → | 0(0(#(#(x0)))) |
| #(#(1(1(x0)))) | → | 1(1(#(#(x0)))) |
| #(#($($(x0)))) | → | *(*($($(x0)))) |
| t0 | = | Begin(0(0(#(#(End(x54543)))))) |
| →ε | Wait(Right8(#(#(End(x54543))))) | |
| →1 | Wait(Left(0(0(#(#(End(x54543))))))) | |
| →ε | Begin(0(0(#(#(End(x54543)))))) | |
| = | t3 |