by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(a(x0)) | → | Wait(Right1(x0)) |
| Begin(y(x0)) | → | Wait(Right2(x0)) |
| Begin(q2(a(x0))) | → | Wait(Right3(x0)) |
| Begin(a(x0)) | → | Wait(Right4(x0)) |
| Begin(q2(y(x0))) | → | Wait(Right5(x0)) |
| Begin(y(x0)) | → | Wait(Right6(x0)) |
| Begin(q2(a(x0))) | → | Wait(Right7(x0)) |
| Begin(a(x0)) | → | Wait(Right8(x0)) |
| Begin(q2(y(x0))) | → | Wait(Right9(x0)) |
| Begin(y(x0)) | → | Wait(Right10(x0)) |
| Begin(y(x0)) | → | Wait(Right11(x0)) |
| Right1(q1(End(x0))) | → | Left(a(q1(End(x0)))) |
| Right2(q1(End(x0))) | → | Left(y(q1(End(x0)))) |
| Right3(a(End(x0))) | → | Left(q2(a(a(End(x0))))) |
| Right4(a(q2(End(x0)))) | → | Left(q2(a(a(End(x0))))) |
| Right5(a(End(x0))) | → | Left(q2(a(y(End(x0))))) |
| Right6(a(q2(End(x0)))) | → | Left(q2(a(y(End(x0))))) |
| Right7(y(End(x0))) | → | Left(q2(y(a(End(x0))))) |
| Right8(y(q2(End(x0)))) | → | Left(q2(y(a(End(x0))))) |
| Right9(y(End(x0))) | → | Left(q2(y(y(End(x0))))) |
| Right10(y(q2(End(x0)))) | → | Left(q2(y(y(End(x0))))) |
| Right11(q3(End(x0))) | → | Left(y(q3(End(x0)))) |
| Right1(q1(x0)) | → | Aq1(Right1(x0)) |
| Right2(q1(x0)) | → | Aq1(Right2(x0)) |
| Right3(q1(x0)) | → | Aq1(Right3(x0)) |
| Right4(q1(x0)) | → | Aq1(Right4(x0)) |
| Right5(q1(x0)) | → | Aq1(Right5(x0)) |
| Right6(q1(x0)) | → | Aq1(Right6(x0)) |
| Right7(q1(x0)) | → | Aq1(Right7(x0)) |
| Right8(q1(x0)) | → | Aq1(Right8(x0)) |
| Right9(q1(x0)) | → | Aq1(Right9(x0)) |
| Right10(q1(x0)) | → | Aq1(Right10(x0)) |
| Right11(q1(x0)) | → | Aq1(Right11(x0)) |
| Right1(a(x0)) | → | Aa(Right1(x0)) |
| Right2(a(x0)) | → | Aa(Right2(x0)) |
| Right3(a(x0)) | → | Aa(Right3(x0)) |
| Right4(a(x0)) | → | Aa(Right4(x0)) |
| Right5(a(x0)) | → | Aa(Right5(x0)) |
| Right6(a(x0)) | → | Aa(Right6(x0)) |
| Right7(a(x0)) | → | Aa(Right7(x0)) |
| Right8(a(x0)) | → | Aa(Right8(x0)) |
| Right9(a(x0)) | → | Aa(Right9(x0)) |
| Right10(a(x0)) | → | Aa(Right10(x0)) |
| Right11(a(x0)) | → | Aa(Right11(x0)) |
| Right1(y(x0)) | → | Ay(Right1(x0)) |
| Right2(y(x0)) | → | Ay(Right2(x0)) |
| Right3(y(x0)) | → | Ay(Right3(x0)) |
| Right4(y(x0)) | → | Ay(Right4(x0)) |
| Right5(y(x0)) | → | Ay(Right5(x0)) |
| Right6(y(x0)) | → | Ay(Right6(x0)) |
| Right7(y(x0)) | → | Ay(Right7(x0)) |
| Right8(y(x0)) | → | Ay(Right8(x0)) |
| Right9(y(x0)) | → | Ay(Right9(x0)) |
| Right10(y(x0)) | → | Ay(Right10(x0)) |
| Right11(y(x0)) | → | Ay(Right11(x0)) |
| Right1(q2(x0)) | → | Aq2(Right1(x0)) |
| Right2(q2(x0)) | → | Aq2(Right2(x0)) |
| Right3(q2(x0)) | → | Aq2(Right3(x0)) |
| Right4(q2(x0)) | → | Aq2(Right4(x0)) |
| Right5(q2(x0)) | → | Aq2(Right5(x0)) |
| Right6(q2(x0)) | → | Aq2(Right6(x0)) |
| Right7(q2(x0)) | → | Aq2(Right7(x0)) |
| Right8(q2(x0)) | → | Aq2(Right8(x0)) |
| Right9(q2(x0)) | → | Aq2(Right9(x0)) |
| Right10(q2(x0)) | → | Aq2(Right10(x0)) |
| Right11(q2(x0)) | → | Aq2(Right11(x0)) |
| Right1(q3(x0)) | → | Aq3(Right1(x0)) |
| Right2(q3(x0)) | → | Aq3(Right2(x0)) |
| Right3(q3(x0)) | → | Aq3(Right3(x0)) |
| Right4(q3(x0)) | → | Aq3(Right4(x0)) |
| Right5(q3(x0)) | → | Aq3(Right5(x0)) |
| Right6(q3(x0)) | → | Aq3(Right6(x0)) |
| Right7(q3(x0)) | → | Aq3(Right7(x0)) |
| Right8(q3(x0)) | → | Aq3(Right8(x0)) |
| Right9(q3(x0)) | → | Aq3(Right9(x0)) |
| Right10(q3(x0)) | → | Aq3(Right10(x0)) |
| Right11(q3(x0)) | → | Aq3(Right11(x0)) |
| Aq1(Left(x0)) | → | Left(q1(x0)) |
| Aa(Left(x0)) | → | Left(a(x0)) |
| Ay(Left(x0)) | → | Left(y(x0)) |
| Aq2(Left(x0)) | → | Left(q2(x0)) |
| Aq3(Left(x0)) | → | Left(q3(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| q1(a(x0)) | → | a(q1(x0)) |
| q1(y(x0)) | → | y(q1(x0)) |
| a(q2(a(x0))) | → | q2(a(a(x0))) |
| a(q2(y(x0))) | → | q2(a(y(x0))) |
| y(q2(a(x0))) | → | q2(y(a(x0))) |
| y(q2(y(x0))) | → | q2(y(y(x0))) |
| q3(y(x0)) | → | y(q3(x0)) |
| t0 | = | Begin(a(q1(End(x19272)))) |
| →ε | Wait(Right1(q1(End(x19272)))) | |
| →1 | Wait(Left(a(q1(End(x19272))))) | |
| →ε | Begin(a(q1(End(x19272)))) | |
| = | t3 |