by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(Q(Q(x0))) | → | Wait(Right1(x0)) |
| Begin(Q(x0)) | → | Wait(Right2(x0)) |
| Begin(p(q(x0))) | → | Wait(Right3(x0)) |
| Begin(q(x0)) | → | Wait(Right4(x0)) |
| Begin(q(p(x0))) | → | Wait(Right5(x0)) |
| Begin(p(x0)) | → | Wait(Right6(x0)) |
| Right1(p(End(x0))) | → | Left(Q(Q(p(End(x0))))) |
| Right2(p(Q(End(x0)))) | → | Left(Q(Q(p(End(x0))))) |
| Right3(Q(End(x0))) | → | Left(q(p(Q(End(x0))))) |
| Right4(Q(p(End(x0)))) | → | Left(q(p(Q(End(x0))))) |
| Right5(q(End(x0))) | → | Left(p(q(q(End(x0))))) |
| Right6(q(q(End(x0)))) | → | Left(p(q(q(End(x0))))) |
| Right1(p(x0)) | → | Ap(Right1(x0)) |
| Right2(p(x0)) | → | Ap(Right2(x0)) |
| Right3(p(x0)) | → | Ap(Right3(x0)) |
| Right4(p(x0)) | → | Ap(Right4(x0)) |
| Right5(p(x0)) | → | Ap(Right5(x0)) |
| Right6(p(x0)) | → | Ap(Right6(x0)) |
| Right1(Q(x0)) | → | AQ(Right1(x0)) |
| Right2(Q(x0)) | → | AQ(Right2(x0)) |
| Right3(Q(x0)) | → | AQ(Right3(x0)) |
| Right4(Q(x0)) | → | AQ(Right4(x0)) |
| Right5(Q(x0)) | → | AQ(Right5(x0)) |
| Right6(Q(x0)) | → | AQ(Right6(x0)) |
| Right1(q(x0)) | → | Aq(Right1(x0)) |
| Right2(q(x0)) | → | Aq(Right2(x0)) |
| Right3(q(x0)) | → | Aq(Right3(x0)) |
| Right4(q(x0)) | → | Aq(Right4(x0)) |
| Right5(q(x0)) | → | Aq(Right5(x0)) |
| Right6(q(x0)) | → | Aq(Right6(x0)) |
| Ap(Left(x0)) | → | Left(p(x0)) |
| AQ(Left(x0)) | → | Left(Q(x0)) |
| Aq(Left(x0)) | → | Left(q(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| p(Q(Q(x0))) | → | Q(Q(p(x0))) |
| Q(p(q(x0))) | → | q(p(Q(x0))) |
| q(q(p(x0))) | → | p(q(q(x0))) |
| t0 | = | Begin(Q(Q(p(End(x3522))))) |
| →ε | Wait(Right1(p(End(x3522)))) | |
| →1 | Wait(Left(Q(Q(p(End(x3522)))))) | |
| →ε | Begin(Q(Q(p(End(x3522))))) | |
| = | t3 |