by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(p(x0)) | → | Wait(Right1(x0)) |
| Begin(Q(Q(x0))) | → | Wait(Right2(x0)) |
| Begin(Q(x0)) | → | Wait(Right3(x0)) |
| Begin(p(q(x0))) | → | Wait(Right4(x0)) |
| Begin(q(x0)) | → | Wait(Right5(x0)) |
| Begin(q(p(x0))) | → | Wait(Right6(x0)) |
| Begin(p(x0)) | → | Wait(Right7(x0)) |
| Begin(Q(x0)) | → | Wait(Right8(x0)) |
| Begin(q(x0)) | → | Wait(Right9(x0)) |
| Begin(P(x0)) | → | Wait(Right10(x0)) |
| Begin(p(x0)) | → | Wait(Right11(x0)) |
| Right1(p(End(x0))) | → | Left(q(q(End(x0)))) |
| Right2(p(End(x0))) | → | Left(Q(Q(p(End(x0))))) |
| Right3(p(Q(End(x0)))) | → | Left(Q(Q(p(End(x0))))) |
| Right4(Q(End(x0))) | → | Left(q(p(Q(End(x0))))) |
| Right5(Q(p(End(x0)))) | → | Left(q(p(Q(End(x0))))) |
| Right6(q(End(x0))) | → | Left(p(q(q(End(x0))))) |
| Right7(q(q(End(x0)))) | → | Left(p(q(q(End(x0))))) |
| Right8(q(End(x0))) | → | Left(End(x0)) |
| Right9(Q(End(x0))) | → | Left(End(x0)) |
| Right10(p(End(x0))) | → | Left(End(x0)) |
| Right11(P(End(x0))) | → | Left(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)) |
| Right7(P(x0)) | → | AP(Right7(x0)) |
| Right8(P(x0)) | → | AP(Right8(x0)) |
| Right9(P(x0)) | → | AP(Right9(x0)) |
| Right10(P(x0)) | → | AP(Right10(x0)) |
| Right11(P(x0)) | → | AP(Right11(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)) |
| Right7(Q(x0)) | → | AQ(Right7(x0)) |
| Right8(Q(x0)) | → | AQ(Right8(x0)) |
| Right9(Q(x0)) | → | AQ(Right9(x0)) |
| Right10(Q(x0)) | → | AQ(Right10(x0)) |
| Right11(Q(x0)) | → | AQ(Right11(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)) |
| Right7(p(x0)) | → | Ap(Right7(x0)) |
| Right8(p(x0)) | → | Ap(Right8(x0)) |
| Right9(p(x0)) | → | Ap(Right9(x0)) |
| Right10(p(x0)) | → | Ap(Right10(x0)) |
| Right11(p(x0)) | → | Ap(Right11(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)) |
| Right7(q(x0)) | → | Aq(Right7(x0)) |
| Right8(q(x0)) | → | Aq(Right8(x0)) |
| Right9(q(x0)) | → | Aq(Right9(x0)) |
| Right10(q(x0)) | → | Aq(Right10(x0)) |
| Right11(q(x0)) | → | Aq(Right11(x0)) |
| AP(Left(x0)) | → | Left(P(x0)) |
| AQ(Left(x0)) | → | Left(Q(x0)) |
| Ap(Left(x0)) | → | Left(p(x0)) |
| Aq(Left(x0)) | → | Left(q(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| P(x0) | → | Q(Q(p(x0))) |
| p(p(x0)) | → | q(q(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))) |
| q(Q(x0)) | → | x0 |
| Q(q(x0)) | → | x0 |
| p(P(x0)) | → | x0 |
| P(p(x0)) | → | x0 |
| t0 | = | Begin(Q(Q(p(End(x15613))))) |
| →ε | Wait(Right2(p(End(x15613)))) | |
| →1 | Wait(Left(Q(Q(p(End(x15613)))))) | |
| →ε | Begin(Q(Q(p(End(x15613))))) | |
| = | t3 |