by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(*(x0)) | → | Wait(Right1(x0)) |
| Begin(*(x0)) | → | Wait(Right2(x0)) |
| Begin(0(x0)) | → | Wait(Right3(x0)) |
| Begin(1(x0)) | → | Wait(Right4(x0)) |
| Begin($(x0)) | → | Wait(Right5(x0)) |
| Begin(#(x0)) | → | Wait(Right6(x0)) |
| Begin(*(x0)) | → | Wait(Right7(x0)) |
| Right1(0(End(x0))) | → | Left(*(1(End(x0)))) |
| Right2(1(End(x0))) | → | Left(0(#(End(x0)))) |
| Right3(#(End(x0))) | → | Left(0(#(End(x0)))) |
| Right4(#(End(x0))) | → | Left(1(#(End(x0)))) |
| Right5(#(End(x0))) | → | Left(*($(End(x0)))) |
| Right6(#(End(x0))) | → | Left(#(End(x0))) |
| Right7(#(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)) |
| 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)) |
| 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)) |
| 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)) |
| 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)) |
| 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(*(x0)) | → | *(1(x0)) |
| 1(*(x0)) | → | 0(#(x0)) |
| #(0(x0)) | → | 0(#(x0)) |
| #(1(x0)) | → | 1(#(x0)) |
| #($(x0)) | → | *($(x0)) |
| #(#(x0)) | → | #(x0) |
| #(*(x0)) | → | *(x0) |
| t0 | = | Begin(0(#(End(x11046)))) |
| →ε | Wait(Right3(#(End(x11046)))) | |
| →1 | Wait(Left(0(#(End(x11046))))) | |
| →ε | Begin(0(#(End(x11046)))) | |
| = | t3 |