YES
by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
Begin(a(a(a(b(b(x0)))))) | → | Wait(Right1(x0)) |
Begin(a(a(b(b(x0))))) | → | Wait(Right2(x0)) |
Begin(a(b(b(x0)))) | → | Wait(Right3(x0)) |
Begin(b(b(x0))) | → | Wait(Right4(x0)) |
Begin(b(x0)) | → | Wait(Right5(x0)) |
Right1(b(End(x0))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right2(b(a(End(x0)))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right3(b(a(a(End(x0))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right4(b(a(a(a(End(x0)))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right5(b(a(a(a(b(End(x0))))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right1(b(x0)) | → | Ab(Right1(x0)) |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(x0)) |
Right5(b(x0)) | → | Ab(Right5(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
Wait(Left(x0)) | → | Begin(x0) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
[Wait(x1)] | = |
|
||||||||||||||||||
[Right5(x1)] | = |
|
||||||||||||||||||
[a(x1)] | = |
|
||||||||||||||||||
[Right1(x1)] | = |
|
||||||||||||||||||
[Right2(x1)] | = |
|
||||||||||||||||||
[Left(x1)] | = |
|
||||||||||||||||||
[b(x1)] | = |
|
||||||||||||||||||
[Right4(x1)] | = |
|
||||||||||||||||||
[Aa(x1)] | = |
|
||||||||||||||||||
[Ab(x1)] | = |
|
||||||||||||||||||
[End(x1)] | = |
|
||||||||||||||||||
[Right3(x1)] | = |
|
||||||||||||||||||
[Begin(x1)] | = |
|
Begin(a(a(a(b(b(x0)))))) | → | Wait(Right1(x0)) |
Begin(a(a(b(b(x0))))) | → | Wait(Right2(x0)) |
Begin(a(b(b(x0)))) | → | Wait(Right3(x0)) |
Begin(b(b(x0))) | → | Wait(Right4(x0)) |
Begin(b(x0)) | → | Wait(Right5(x0)) |
Right2(b(a(End(x0)))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right3(b(a(a(End(x0))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right4(b(a(a(a(End(x0)))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right1(b(x0)) | → | Ab(Right1(x0)) |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(x0)) |
Right5(b(x0)) | → | Ab(Right5(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
Wait(Left(x0)) | → | Begin(x0) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
[Wait(x1)] | = | 0 · x1 + -∞ |
[Right5(x1)] | = | 5 · x1 + -∞ |
[a(x1)] | = | 0 · x1 + -∞ |
[Right1(x1)] | = | 8 · x1 + -∞ |
[Right2(x1)] | = | 8 · x1 + -∞ |
[Left(x1)] | = | 6 · x1 + -∞ |
[b(x1)] | = | 1 · x1 + -∞ |
[Right4(x1)] | = | 8 · x1 + -∞ |
[Aa(x1)] | = | 0 · x1 + -∞ |
[Ab(x1)] | = | 1 · x1 + -∞ |
[End(x1)] | = | 6 · x1 + -∞ |
[Right3(x1)] | = | 8 · x1 + -∞ |
[Begin(x1)] | = | 6 · x1 + -∞ |
Begin(a(a(a(b(b(x0)))))) | → | Wait(Right1(x0)) |
Begin(a(a(b(b(x0))))) | → | Wait(Right2(x0)) |
Begin(a(b(b(x0)))) | → | Wait(Right3(x0)) |
Begin(b(b(x0))) | → | Wait(Right4(x0)) |
Right2(b(a(End(x0)))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right3(b(a(a(End(x0))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right4(b(a(a(a(End(x0)))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right1(b(x0)) | → | Ab(Right1(x0)) |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(x0)) |
Right5(b(x0)) | → | Ab(Right5(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
Wait(Left(x0)) | → | Begin(x0) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
[Wait(x1)] | = | 0 · x1 + -∞ |
[Right5(x1)] | = | 0 · x1 + -∞ |
[a(x1)] | = | 0 · x1 + -∞ |
[Right1(x1)] | = | 0 · x1 + -∞ |
[Right2(x1)] | = | 1 · x1 + -∞ |
[Left(x1)] | = | 1 · x1 + -∞ |
[b(x1)] | = | 0 · x1 + -∞ |
[Right4(x1)] | = | 1 · x1 + -∞ |
[Aa(x1)] | = | 0 · x1 + -∞ |
[Ab(x1)] | = | 0 · x1 + -∞ |
[End(x1)] | = | 0 · x1 + -∞ |
[Right3(x1)] | = | 1 · x1 + -∞ |
[Begin(x1)] | = | 1 · x1 + -∞ |
Begin(a(a(b(b(x0))))) | → | Wait(Right2(x0)) |
Begin(a(b(b(x0)))) | → | Wait(Right3(x0)) |
Begin(b(b(x0))) | → | Wait(Right4(x0)) |
Right2(b(a(End(x0)))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right3(b(a(a(End(x0))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right4(b(a(a(a(End(x0)))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right1(b(x0)) | → | Ab(Right1(x0)) |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(x0)) |
Right5(b(x0)) | → | Ab(Right5(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
Wait(Left(x0)) | → | Begin(x0) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
b(b(a(a(Begin(x0))))) | → | Right2(Wait(x0)) |
b(b(a(Begin(x0)))) | → | Right3(Wait(x0)) |
b(b(Begin(x0))) | → | Right4(Wait(x0)) |
End(a(b(Right2(x0)))) | → | End(a(b(b(a(a(b(a(Left(x0))))))))) |
End(a(a(b(Right3(x0))))) | → | End(a(b(b(a(a(b(a(Left(x0))))))))) |
End(a(a(a(b(Right4(x0)))))) | → | End(a(b(b(a(a(b(a(Left(x0))))))))) |
b(Right1(x0)) | → | Right1(Ab(x0)) |
b(Right2(x0)) | → | Right2(Ab(x0)) |
b(Right3(x0)) | → | Right3(Ab(x0)) |
b(Right4(x0)) | → | Right4(Ab(x0)) |
b(Right5(x0)) | → | Right5(Ab(x0)) |
a(Right1(x0)) | → | Right1(Aa(x0)) |
a(Right2(x0)) | → | Right2(Aa(x0)) |
a(Right3(x0)) | → | Right3(Aa(x0)) |
a(Right4(x0)) | → | Right4(Aa(x0)) |
a(Right5(x0)) | → | Right5(Aa(x0)) |
Left(Ab(x0)) | → | b(Left(x0)) |
Left(Aa(x0)) | → | a(Left(x0)) |
Left(Wait(x0)) | → | Begin(x0) |
b(b(a(a(a(b(x0)))))) | → | a(b(b(a(a(b(a(x0))))))) |
[Wait(x1)] | = | 4 · x1 + 0 |
[Right5(x1)] | = | 1 · x1 + 0 |
[a(x1)] | = | 1 · x1 + 0 |
[Right1(x1)] | = | 6 · x1 + 8 |
[Right2(x1)] | = | 4 · x1 + 0 |
[Left(x1)] | = | 1 · x1 + 0 |
[b(x1)] | = | 2 · x1 + 0 |
[Right4(x1)] | = | 4 · x1 + 0 |
[Aa(x1)] | = | 1 · x1 + 0 |
[Ab(x1)] | = | 2 · x1 + 0 |
[End(x1)] | = | 2 · x1 + 0 |
[Right3(x1)] | = | 4 · x1 + 0 |
[Begin(x1)] | = | 4 · x1 + 0 |
b(b(a(a(Begin(x0))))) | → | Right2(Wait(x0)) |
b(b(a(Begin(x0)))) | → | Right3(Wait(x0)) |
b(b(Begin(x0))) | → | Right4(Wait(x0)) |
End(a(b(Right2(x0)))) | → | End(a(b(b(a(a(b(a(Left(x0))))))))) |
End(a(a(b(Right3(x0))))) | → | End(a(b(b(a(a(b(a(Left(x0))))))))) |
End(a(a(a(b(Right4(x0)))))) | → | End(a(b(b(a(a(b(a(Left(x0))))))))) |
b(Right2(x0)) | → | Right2(Ab(x0)) |
b(Right3(x0)) | → | Right3(Ab(x0)) |
b(Right4(x0)) | → | Right4(Ab(x0)) |
b(Right5(x0)) | → | Right5(Ab(x0)) |
a(Right1(x0)) | → | Right1(Aa(x0)) |
a(Right2(x0)) | → | Right2(Aa(x0)) |
a(Right3(x0)) | → | Right3(Aa(x0)) |
a(Right4(x0)) | → | Right4(Aa(x0)) |
a(Right5(x0)) | → | Right5(Aa(x0)) |
Left(Ab(x0)) | → | b(Left(x0)) |
Left(Aa(x0)) | → | a(Left(x0)) |
Left(Wait(x0)) | → | Begin(x0) |
b(b(a(a(a(b(x0)))))) | → | a(b(b(a(a(b(a(x0))))))) |
Begin(a(a(b(b(x0))))) | → | Wait(Right2(x0)) |
Begin(a(b(b(x0)))) | → | Wait(Right3(x0)) |
Begin(b(b(x0))) | → | Wait(Right4(x0)) |
Right2(b(a(End(x0)))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right3(b(a(a(End(x0))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right4(b(a(a(a(End(x0)))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(x0)) |
Right5(b(x0)) | → | Ab(Right5(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
Wait(Left(x0)) | → | Begin(x0) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
[Wait(x1)] | = | 4 · x1 + 0 |
[Right5(x1)] | = | 4 · x1 + 2 |
[a(x1)] | = | 1 · x1 + 0 |
[Right1(x1)] | = | 1 · x1 + 0 |
[Right2(x1)] | = | 4 · x1 + 3 |
[Left(x1)] | = | 1 · x1 + 0 |
[b(x1)] | = | 2 · x1 + 1 |
[Right4(x1)] | = | 4 · x1 + 3 |
[Aa(x1)] | = | 1 · x1 + 0 |
[Ab(x1)] | = | 2 · x1 + 1 |
[End(x1)] | = | 1 · x1 + 1 |
[Right3(x1)] | = | 4 · x1 + 3 |
[Begin(x1)] | = | 4 · x1 + 0 |
Begin(a(a(b(b(x0))))) | → | Wait(Right2(x0)) |
Begin(a(b(b(x0)))) | → | Wait(Right3(x0)) |
Begin(b(b(x0))) | → | Wait(Right4(x0)) |
Right2(b(a(End(x0)))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right3(b(a(a(End(x0))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right4(b(a(a(a(End(x0)))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
Wait(Left(x0)) | → | Begin(x0) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
[Wait(x1)] | = |
|
||||||||||||||||||
[Right5(x1)] | = |
|
||||||||||||||||||
[a(x1)] | = |
|
||||||||||||||||||
[Right1(x1)] | = |
|
||||||||||||||||||
[Right2(x1)] | = |
|
||||||||||||||||||
[Left(x1)] | = |
|
||||||||||||||||||
[b(x1)] | = |
|
||||||||||||||||||
[Right4(x1)] | = |
|
||||||||||||||||||
[Aa(x1)] | = |
|
||||||||||||||||||
[Ab(x1)] | = |
|
||||||||||||||||||
[End(x1)] | = |
|
||||||||||||||||||
[Right3(x1)] | = |
|
||||||||||||||||||
[Begin(x1)] | = |
|
Begin(a(a(b(b(x0))))) | → | Wait(Right2(x0)) |
Right3(b(a(a(End(x0))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right4(b(a(a(a(End(x0)))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
Wait(Left(x0)) | → | Begin(x0) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
[Wait(x1)] | = | 0 · x1 + -∞ |
[Right5(x1)] | = | 0 · x1 + -∞ |
[a(x1)] | = | 0 · x1 + -∞ |
[Right1(x1)] | = | 12 · x1 + -∞ |
[Right2(x1)] | = | 10 · x1 + -∞ |
[Left(x1)] | = | 10 · x1 + -∞ |
[b(x1)] | = | 0 · x1 + -∞ |
[Right4(x1)] | = | 10 · x1 + -∞ |
[Aa(x1)] | = | 0 · x1 + -∞ |
[Ab(x1)] | = | 0 · x1 + -∞ |
[End(x1)] | = | 6 · x1 + -∞ |
[Right3(x1)] | = | 14 · x1 + -∞ |
[Begin(x1)] | = | 10 · x1 + -∞ |
Begin(a(a(b(b(x0))))) | → | Wait(Right2(x0)) |
Right4(b(a(a(a(End(x0)))))) | → | Left(a(b(a(a(b(b(a(End(x0))))))))) |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
Wait(Left(x0)) | → | Begin(x0) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
[Wait(x1)] | = | 0 · x1 + -∞ |
[Right5(x1)] | = | 4 · x1 + -∞ |
[a(x1)] | = | 0 · x1 + -∞ |
[Right1(x1)] | = | 7 · x1 + -∞ |
[Right2(x1)] | = | 0 · x1 + -∞ |
[Left(x1)] | = | 0 · x1 + -∞ |
[b(x1)] | = | 0 · x1 + -∞ |
[Right4(x1)] | = | 4 · x1 + -∞ |
[Aa(x1)] | = | 0 · x1 + -∞ |
[Ab(x1)] | = | 0 · x1 + -∞ |
[End(x1)] | = | 0 · x1 + -∞ |
[Right3(x1)] | = | 0 · x1 + -∞ |
[Begin(x1)] | = | 0 · x1 + -∞ |
Begin(a(a(b(b(x0))))) | → | Wait(Right2(x0)) |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
Wait(Left(x0)) | → | Begin(x0) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
[Wait(x1)] | = | 0 · x1 + -∞ |
[Right5(x1)] | = | 0 · x1 + -∞ |
[a(x1)] | = | 0 · x1 + -∞ |
[Right1(x1)] | = | 0 · x1 + -∞ |
[Right2(x1)] | = | 0 · x1 + -∞ |
[Left(x1)] | = | 11 · x1 + -∞ |
[b(x1)] | = | 1 · x1 + -∞ |
[Right4(x1)] | = | 11 · x1 + -∞ |
[Aa(x1)] | = | 0 · x1 + -∞ |
[Ab(x1)] | = | 1 · x1 + -∞ |
[Right3(x1)] | = | 4 · x1 + -∞ |
[Begin(x1)] | = | 8 · x1 + -∞ |
Right2(b(x0)) | → | Ab(Right2(x0)) |
Right3(b(x0)) | → | Ab(Right3(x0)) |
Right4(b(x0)) | → | Ab(Right4(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)) |
Ab(Left(x0)) | → | Left(b(x0)) |
Aa(Left(x0)) | → | Left(a(x0)) |
b(a(a(a(b(b(x0)))))) | → | a(b(a(a(b(b(a(x0))))))) |
final states:
{19, 17, 15, 13, 12, 11, 10, 8, 6, 4, 1}
transitions:
10 | → | 3 |
1 | → | 3 |
8 | → | 9 |
13 | → | 14 |
6 | → | 7 |
11 | → | 5 |
4 | → | 5 |
12 | → | 7 |
19 | → | 20 |
19 | → | 16 |
b0(18) | → | 20 |
b0(2) | → | 16 |
b0(23) | → | 24 |
b0(20) | → | 21 |
Left0(16) | → | 15 |
Left0(18) | → | 17 |
Right30(2) | → | 5 |
Aa0(7) | → | 12 |
Aa0(14) | → | 13 |
Aa0(9) | → | 8 |
Aa0(5) | → | 11 |
Aa0(3) | → | 10 |
Right40(2) | → | 7 |
f130 | → | 2 |
Ab0(7) | → | 6 |
Ab0(3) | → | 1 |
Ab0(5) | → | 4 |
Right20(2) | → | 3 |
a0(2) | → | 18 |
a0(21) | → | 22 |
a0(24) | → | 19 |
a0(22) | → | 23 |
Right50(2) | → | 14 |
Right10(2) | → | 9 |