by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(0(x0)) | → | Wait(Right1(x0)) |
| Begin(1(x0)) | → | Wait(Right2(x0)) |
| Right1(#(End(x0))) | → | Left(0(#(End(x0)))) |
| Right2(#(End(x0))) | → | Left(1(#(End(x0)))) |
| Right1(#(x0)) | → | A#(Right1(x0)) |
| Right2(#(x0)) | → | A#(Right2(x0)) |
| Right1(0(x0)) | → | A0(Right1(x0)) |
| Right2(0(x0)) | → | A0(Right2(x0)) |
| Right1(1(x0)) | → | A1(Right1(x0)) |
| Right2(1(x0)) | → | A1(Right2(x0)) |
| A#(Left(x0)) | → | Left(#(x0)) |
| A0(Left(x0)) | → | Left(0(x0)) |
| A1(Left(x0)) | → | Left(1(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| #(0(x0)) | → | 0(#(x0)) |
| #(1(x0)) | → | 1(#(x0)) |
| t0 | = | Begin(0(#(End(x579)))) |
| →ε | Wait(Right1(#(End(x579)))) | |
| →1 | Wait(Left(0(#(End(x579))))) | |
| →ε | Begin(0(#(End(x579)))) | |
| = | t3 |