YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(E(x0)) → Wait(Right1(x0))
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Begin(L(x0)) → Wait(Right6(x0))
Right1(R(End(x0))) → Left(L(E(End(x0))))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right6(a(End(x0))) → Left(b(R(End(x0))))
Right1(R(x0)) → AR(Right1(x0))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right6(R(x0)) → AR(Right6(x0))
Right1(E(x0)) → AE(Right1(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right4(E(x0)) → AE(Right4(x0))
Right5(E(x0)) → AE(Right5(x0))
Right6(E(x0)) → AE(Right6(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right6(a(x0)) → AAa(Right6(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right6(Aa(x0)) → AAAa(Right6(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
R(E(x0)) → L(E(x0))
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
a(L(x0)) → b(R(x0))

Proof

1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[AE(x1)] = 0 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 4 · x1 + -∞
[Right4(x1)] = 4 · x1 + -∞
[Begin(x1)] = 0 · x1 + -∞
[Wait(x1)] = 0 · x1 + -∞
[b(x1)] = 0 · x1 + -∞
[AAAa(x1)] = 4 · x1 + -∞
[AL(x1)] = 0 · x1 + -∞
[AR(x1)] = 0 · x1 + -∞
[AAb(x1)] = 0 · x1 + -∞
[Right2(x1)] = 0 · x1 + -∞
[Right5(x1)] = 0 · x1 + -∞
[E(x1)] = 0 · x1 + -∞
[Aa(x1)] = 4 · x1 + -∞
[AAa(x1)] = 4 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[End(x1)] = 0 · x1 + -∞
[AAAb(x1)] = 0 · x1 + -∞
[Right6(x1)] = 0 · x1 + -∞
[Ab(x1)] = 0 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[Right3(x1)] = 0 · x1 + -∞
[Right1(x1)] = 0 · x1 + -∞
the rules
Begin(E(x0)) → Wait(Right1(x0))
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Begin(L(x0)) → Wait(Right6(x0))
Right1(R(End(x0))) → Left(L(E(End(x0))))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right1(R(x0)) → AR(Right1(x0))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right6(R(x0)) → AR(Right6(x0))
Right1(E(x0)) → AE(Right1(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right4(E(x0)) → AE(Right4(x0))
Right5(E(x0)) → AE(Right5(x0))
Right6(E(x0)) → AE(Right6(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right6(a(x0)) → AAa(Right6(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right6(Aa(x0)) → AAAa(Right6(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
R(E(x0)) → L(E(x0))
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
remain.

1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[AE(x1)] = 6 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 0 · x1 + -∞
[Right4(x1)] = 2 · x1 + -∞
[Begin(x1)] = 8 · x1 + -∞
[Wait(x1)] = 6 · x1 + -∞
[b(x1)] = 4 · x1 + -∞
[AAAa(x1)] = 0 · x1 + -∞
[AL(x1)] = 0 · x1 + -∞
[AR(x1)] = 0 · x1 + -∞
[AAb(x1)] = 4 · x1 + -∞
[Right2(x1)] = 2 · x1 + -∞
[Right5(x1)] = 6 · x1 + -∞
[E(x1)] = 6 · x1 + -∞
[Aa(x1)] = 0 · x1 + -∞
[AAa(x1)] = 0 · x1 + -∞
[Left(x1)] = 2 · x1 + -∞
[End(x1)] = 0 · x1 + -∞
[AAAb(x1)] = 4 · x1 + -∞
[Right6(x1)] = 0 · x1 + -∞
[Ab(x1)] = 4 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[Right3(x1)] = 2 · x1 + -∞
[Right1(x1)] = 8 · x1 + -∞
the rules
Begin(E(x0)) → Wait(Right1(x0))
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right1(R(End(x0))) → Left(L(E(End(x0))))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right1(R(x0)) → AR(Right1(x0))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right6(R(x0)) → AR(Right6(x0))
Right1(E(x0)) → AE(Right1(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right4(E(x0)) → AE(Right4(x0))
Right5(E(x0)) → AE(Right5(x0))
Right6(E(x0)) → AE(Right6(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right6(a(x0)) → AAa(Right6(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right6(Aa(x0)) → AAAa(Right6(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
R(E(x0)) → L(E(x0))
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
remain.

1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[AE(x1)] = 9 · x1 + -∞
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 0 · x1 + -∞
[Right4(x1)] = 0 · x1 + -∞
[Begin(x1)] = 3 · x1 + -∞
[Wait(x1)] = 3 · x1 + -∞
[b(x1)] = 0 · x1 + -∞
[AAAa(x1)] = 0 · x1 + -∞
[AL(x1)] = 0 · x1 + -∞
[AR(x1)] = 8 · x1 + -∞
[AAb(x1)] = 0 · x1 + -∞
[Right2(x1)] = 0 · x1 + -∞
[Right5(x1)] = 0 · x1 + -∞
[E(x1)] = 9 · x1 + -∞
[Aa(x1)] = 0 · x1 + -∞
[AAa(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[End(x1)] = 0 · x1 + -∞
[AAAb(x1)] = 0 · x1 + -∞
[Right6(x1)] = 0 · x1 + -∞
[Ab(x1)] = 0 · x1 + -∞
[R(x1)] = 8 · x1 + -∞
[Right3(x1)] = 0 · x1 + -∞
[Right1(x1)] = 5 · x1 + -∞
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right1(R(x0)) → AR(Right1(x0))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right6(R(x0)) → AR(Right6(x0))
Right1(E(x0)) → AE(Right1(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right4(E(x0)) → AE(Right4(x0))
Right5(E(x0)) → AE(Right5(x0))
Right6(E(x0)) → AE(Right6(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right6(a(x0)) → AAa(Right6(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right6(Aa(x0)) → AAAa(Right6(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
remain.

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[AE(x1)] = 1 · x1 + 6
[L(x1)] = 1 · x1 + 0
[a(x1)] = 2 · x1 + 0
[Right4(x1)] = 2 · x1 + 0
[Begin(x1)] = 8 · x1 + 0
[Wait(x1)] = 8 · x1 + 0
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 2 · x1 + 0
[AL(x1)] = 1 · x1 + 0
[AR(x1)] = 8 · x1 + 0
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 1 · x1 + 0
[Right5(x1)] = 1 · x1 + 0
[E(x1)] = 1 · x1 + 6
[Aa(x1)] = 2 · x1 + 0
[AAa(x1)] = 2 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[End(x1)] = 1 · x1 + 0
[AAAb(x1)] = 1 · x1 + 0
[Right6(x1)] = 1 · x1 + 0
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 8 · x1 + 0
[Right3(x1)] = 1 · x1 + 0
[Right1(x1)] = 2 · x1 + 0
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right1(R(x0)) → AR(Right1(x0))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right6(R(x0)) → AR(Right6(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right5(E(x0)) → AE(Right5(x0))
Right6(E(x0)) → AE(Right6(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right6(a(x0)) → AAa(Right6(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right6(Aa(x0)) → AAAa(Right6(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
remain.

1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right1(x0)) → Right1(AR(x0))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
R(Right6(x0)) → Right6(AR(x0))
E(Right2(x0)) → Right2(AE(x0))
E(Right3(x0)) → Right3(AE(x0))
E(Right5(x0)) → Right5(AE(x0))
E(Right6(x0)) → Right6(AE(x0))
L(Right1(x0)) → Right1(AL(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
L(Right6(x0)) → Right6(AL(x0))
a(Right1(x0)) → Right1(AAa(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
a(Right6(x0)) → Right6(AAa(x0))
Aa(Right1(x0)) → Right1(AAAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
Aa(Right6(x0)) → Right6(AAAa(x0))
b(Right1(x0)) → Right1(AAb(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
b(Right6(x0)) → Right6(AAb(x0))
Ab(Right1(x0)) → Right1(AAAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Ab(Right6(x0)) → Right6(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AE(x0)) → E(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[AE(x1)] = 1 · x1 + 4
[L(x1)] = 1 · x1 + 0
[a(x1)] = 1 · x1 + 0
[Right4(x1)] = 2 · x1 + 0
[Begin(x1)] = 2 · x1 + 0
[Wait(x1)] = 1 · x1 + 0
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 1 · x1 + 0
[AL(x1)] = 1 · x1 + 0
[AR(x1)] = 8 · x1 + 0
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 2 · x1 + 0
[Right5(x1)] = 2 · x1 + 0
[E(x1)] = 1 · x1 + 8
[Aa(x1)] = 1 · x1 + 0
[AAa(x1)] = 1 · x1 + 0
[Left(x1)] = 2 · x1 + 0
[End(x1)] = 1 · x1 + 2
[AAAb(x1)] = 1 · x1 + 0
[Right6(x1)] = 2 · x1 + 0
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 8 · x1 + 0
[Right3(x1)] = 2 · x1 + 0
[Right1(x1)] = 2 · x1 + 2
the rules
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
R(Right6(x0)) → Right6(AR(x0))
E(Right2(x0)) → Right2(AE(x0))
E(Right3(x0)) → Right3(AE(x0))
E(Right5(x0)) → Right5(AE(x0))
E(Right6(x0)) → Right6(AE(x0))
L(Right1(x0)) → Right1(AL(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
L(Right6(x0)) → Right6(AL(x0))
a(Right1(x0)) → Right1(AAa(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
a(Right6(x0)) → Right6(AAa(x0))
Aa(Right1(x0)) → Right1(AAAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
Aa(Right6(x0)) → Right6(AAAa(x0))
b(Right1(x0)) → Right1(AAb(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
b(Right6(x0)) → Right6(AAb(x0))
Ab(Right1(x0)) → Right1(AAAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Ab(Right6(x0)) → Right6(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AE(x0)) → E(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))
remain.

1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right6(R(x0)) → AR(Right6(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right5(E(x0)) → AE(Right5(x0))
Right6(E(x0)) → AE(Right6(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right6(a(x0)) → AAa(Right6(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right6(Aa(x0)) → AAAa(Right6(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[AE(x1)] = 2 · x1 + 14
[L(x1)] = 1 · x1 + 0
[a(x1)] = 1 · x1 + 0
[Right4(x1)] = 8 · x1 + 2
[Begin(x1)] = 8 · x1 + 2
[Wait(x1)] = 1 · x1 + 0
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 1 · x1 + 0
[AL(x1)] = 1 · x1 + 0
[AR(x1)] = 1 · x1 + 8
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 8 · x1 + 2
[Right5(x1)] = 8 · x1 + 2
[E(x1)] = 2 · x1 + 2
[Aa(x1)] = 1 · x1 + 0
[AAa(x1)] = 1 · x1 + 0
[Left(x1)] = 8 · x1 + 2
[End(x1)] = 1 · x1 + 2
[AAAb(x1)] = 1 · x1 + 0
[Right6(x1)] = 8 · x1 + 0
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 1 · x1 + 1
[Right3(x1)] = 8 · x1 + 2
[Right1(x1)] = 1 · x1 + 0
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right6(R(x0)) → AR(Right6(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right5(E(x0)) → AE(Right5(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right6(a(x0)) → AAa(Right6(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right6(Aa(x0)) → AAAa(Right6(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
remain.

1.1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
R(Right6(x0)) → Right6(AR(x0))
E(Right2(x0)) → Right2(AE(x0))
E(Right3(x0)) → Right3(AE(x0))
E(Right5(x0)) → Right5(AE(x0))
L(Right1(x0)) → Right1(AL(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
L(Right6(x0)) → Right6(AL(x0))
a(Right1(x0)) → Right1(AAa(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
a(Right6(x0)) → Right6(AAa(x0))
Aa(Right1(x0)) → Right1(AAAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
Aa(Right6(x0)) → Right6(AAAa(x0))
b(Right1(x0)) → Right1(AAb(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
b(Right6(x0)) → Right6(AAb(x0))
Ab(Right1(x0)) → Right1(AAAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Ab(Right6(x0)) → Right6(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AE(x0)) → E(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[AE(x1)] = 1 · x1 + 0
[L(x1)] = 1 · x1 + 0
[a(x1)] = 1 · x1 + 8
[Right4(x1)] = 8 · x1 + 8
[Begin(x1)] = 8 · x1 + 0
[Wait(x1)] = 1 · x1 + 0
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 1 · x1 + 1
[AL(x1)] = 1 · x1 + 0
[AR(x1)] = 1 · x1 + 0
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 8 · x1 + 0
[Right5(x1)] = 8 · x1 + 0
[E(x1)] = 1 · x1 + 0
[Aa(x1)] = 1 · x1 + 8
[AAa(x1)] = 1 · x1 + 1
[Left(x1)] = 8 · x1 + 0
[End(x1)] = 1 · x1 + 0
[AAAb(x1)] = 1 · x1 + 0
[Right6(x1)] = 4 · x1 + 2
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 1 · x1 + 0
[Right3(x1)] = 8 · x1 + 0
[Right1(x1)] = 8 · x1 + 10
the rules
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
R(Right6(x0)) → Right6(AR(x0))
E(Right2(x0)) → Right2(AE(x0))
E(Right3(x0)) → Right3(AE(x0))
E(Right5(x0)) → Right5(AE(x0))
L(Right1(x0)) → Right1(AL(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
L(Right6(x0)) → Right6(AL(x0))
a(Right1(x0)) → Right1(AAa(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right1(x0)) → Right1(AAAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right1(x0)) → Right1(AAb(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
b(Right6(x0)) → Right6(AAb(x0))
Ab(Right1(x0)) → Right1(AAAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Ab(Right6(x0)) → Right6(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AE(x0)) → E(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right6(R(x0)) → AR(Right6(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right5(E(x0)) → AE(Right5(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))

1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[AE(x1)] = 1 · x1 + 0
[L(x1)] = 1 · x1 + 0
[a(x1)] = 1 · x1 + 0
[Right4(x1)] = 1 · x1 + 0
[Begin(x1)] = 2 · x1 + 0
[Wait(x1)] = 2 · x1 + 0
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 1 · x1 + 0
[AL(x1)] = 1 · x1 + 0
[AR(x1)] = 4 · x1 + 8
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 1 · x1 + 0
[Right5(x1)] = 1 · x1 + 0
[E(x1)] = 1 · x1 + 0
[Aa(x1)] = 1 · x1 + 0
[AAa(x1)] = 1 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[End(x1)] = 6 · x1 + 0
[AAAb(x1)] = 1 · x1 + 0
[Right6(x1)] = 2 · x1 + 1
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 4 · x1 + 8
[Right3(x1)] = 1 · x1 + 0
[Right1(x1)] = 8 · x1 + 0
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right5(E(x0)) → AE(Right5(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[AE(x1)] = 4 · x1 + 2
[L(x1)] = 4 · x1 + 0
[a(x1)] = 2 · x1 + 0
[Right4(x1)] = 2 · x1 + 0
[Begin(x1)] = 1 · x1 + 0
[Wait(x1)] = 1 · x1 + 0
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 2 · x1 + 0
[AL(x1)] = 4 · x1 + 0
[AR(x1)] = 1 · x1 + 0
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 4 · x1 + 0
[Right5(x1)] = 1 · x1 + 0
[E(x1)] = 4 · x1 + 2
[Aa(x1)] = 2 · x1 + 0
[AAa(x1)] = 2 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[End(x1)] = 2 · x1 + 0
[AAAb(x1)] = 1 · x1 + 0
[Right6(x1)] = 2 · x1 + 0
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 1 · x1 + 0
[Right3(x1)] = 4 · x1 + 0
[Right1(x1)] = 2 · x1 + 0
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right5(E(x0)) → AE(Right5(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
E(Right5(x0)) → Right5(AE(x0))
L(Right1(x0)) → Right1(AL(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
L(Right6(x0)) → Right6(AL(x0))
a(Right1(x0)) → Right1(AAa(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right1(x0)) → Right1(AAAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right1(x0)) → Right1(AAb(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
b(Right6(x0)) → Right6(AAb(x0))
Ab(Right1(x0)) → Right1(AAAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Ab(Right6(x0)) → Right6(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AE(x0)) → E(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[AE(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[L(x1)] =
1 0 1
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[a(x1)] =
1 0 0
1 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[Right4(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Begin(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
1 0 0
1 0 0
0 0 0
[Wait(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
1 0 0
1 0 0
0 0 0
[b(x1)] =
1 0 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[AAAa(x1)] =
1 0 0
1 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AL(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AR(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AAb(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right2(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right5(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[E(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Aa(x1)] =
1 0 0
1 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AAa(x1)] =
1 0 0
1 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Left(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[End(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[AAAb(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[Right6(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
1 0 0
1 0 0
[Ab(x1)] =
1 0 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[R(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right3(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right1(x1)] =
1 0 1
0 0 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
the rules
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
E(Right5(x0)) → Right5(AE(x0))
L(Right1(x0)) → Right1(AL(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
a(Right1(x0)) → Right1(AAa(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right1(x0)) → Right1(AAAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right1(x0)) → Right1(AAb(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
b(Right6(x0)) → Right6(AAb(x0))
Ab(Right1(x0)) → Right1(AAAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Ab(Right6(x0)) → Right6(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AE(x0)) → E(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[AE(x1)] = 1 · x1 + 0
[L(x1)] = 1 · x1 + 0
[a(x1)] = 1 · x1 + 0
[Right4(x1)] = 4 · x1 + 0
[Begin(x1)] = 8 · x1 + 0
[Wait(x1)] = 2 · x1 + 0
[b(x1)] = 2 · x1 + 0
[AAAa(x1)] = 1 · x1 + 0
[AL(x1)] = 1 · x1 + 0
[AR(x1)] = 1 · x1 + 0
[AAb(x1)] = 2 · x1 + 0
[Right2(x1)] = 4 · x1 + 0
[Right5(x1)] = 8 · x1 + 0
[E(x1)] = 1 · x1 + 0
[Aa(x1)] = 1 · x1 + 0
[AAa(x1)] = 1 · x1 + 0
[Left(x1)] = 4 · x1 + 0
[End(x1)] = 1 · x1 + 0
[AAAb(x1)] = 2 · x1 + 0
[Right6(x1)] = 8 · x1 + 7
[Ab(x1)] = 2 · x1 + 0
[R(x1)] = 1 · x1 + 0
[Right3(x1)] = 4 · x1 + 0
[Right1(x1)] = 1 · x1 + 3
the rules
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
E(Right5(x0)) → Right5(AE(x0))
L(Right1(x0)) → Right1(AL(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
a(Right1(x0)) → Right1(AAa(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right1(x0)) → Right1(AAAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AE(x0)) → E(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[AE(x1)] = 4 · x1 + 12
[L(x1)] = 1 · x1 + 0
[a(x1)] = 2 · x1 + 1
[Right4(x1)] = 2 · x1 + 1
[Begin(x1)] = 2 · x1 + 0
[Wait(x1)] = 2 · x1 + 0
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 2 · x1 + 1
[AL(x1)] = 1 · x1 + 0
[AR(x1)] = 8 · x1 + 7
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 1 · x1 + 0
[Right5(x1)] = 1 · x1 + 0
[E(x1)] = 4 · x1 + 12
[Aa(x1)] = 2 · x1 + 1
[AAa(x1)] = 2 · x1 + 1
[Left(x1)] = 1 · x1 + 0
[End(x1)] = 1 · x1 + 0
[AAAb(x1)] = 1 · x1 + 0
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 8 · x1 + 7
[Right3(x1)] = 1 · x1 + 0
[Right1(x1)] = 3 · x1 + 9
the rules
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
E(Right5(x0)) → Right5(AE(x0))
L(Right1(x0)) → Right1(AL(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AE(x0)) → E(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right5(E(x0)) → AE(Right5(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[AE(x1)] = 2 · x1 + 13
[L(x1)] = 4 · x1 + 3
[a(x1)] = 4 · x1 + 3
[Right4(x1)] = 4 · x1 + 3
[Begin(x1)] = 2 · x1 + 0
[Wait(x1)] = 2 · x1 + 0
[b(x1)] = 2 · x1 + 1
[AAAa(x1)] = 4 · x1 + 3
[AL(x1)] = 4 · x1 + 3
[AR(x1)] = 5 · x1 + 4
[AAb(x1)] = 2 · x1 + 1
[Right2(x1)] = 4 · x1 + 3
[Right5(x1)] = 2 · x1 + 1
[E(x1)] = 2 · x1 + 8
[Aa(x1)] = 4 · x1 + 3
[AAa(x1)] = 4 · x1 + 3
[Left(x1)] = 1 · x1 + 0
[End(x1)] = 1 · x1 + 0
[AAAb(x1)] = 2 · x1 + 1
[Ab(x1)] = 2 · x1 + 1
[R(x1)] = 5 · x1 + 4
[Right3(x1)] = 4 · x1 + 3
[Right1(x1)] = 1 · x1 + 0
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
L(Right1(x0)) → Right1(AL(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[L(x1)] = 4 · x1 + 0
[a(x1)] = 1 · x1 + 0
[Right4(x1)] = 1 · x1 + 0
[Begin(x1)] = 1 · x1 + 0
[Wait(x1)] = 1 · x1 + 0
[b(x1)] = 2 · x1 + 0
[AAAa(x1)] = 1 · x1 + 0
[AL(x1)] = 4 · x1 + 0
[AR(x1)] = 4 · x1 + 0
[AAb(x1)] = 2 · x1 + 0
[Right2(x1)] = 4 · x1 + 0
[Right5(x1)] = 2 · x1 + 0
[Aa(x1)] = 1 · x1 + 0
[AAa(x1)] = 1 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[End(x1)] = 1 · x1 + 0
[AAAb(x1)] = 2 · x1 + 0
[Ab(x1)] = 2 · x1 + 0
[R(x1)] = 4 · x1 + 0
[Right3(x1)] = 4 · x1 + 0
[Right1(x1)] = 2 · x1 + 4
the rules
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
Ab(R(x0)) → R(b(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[L(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[Right4(x1)] =
1 0 0
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[Begin(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[Wait(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[b(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AAAa(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AL(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AR(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[AAb(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right2(x1)] =
1 0 0
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right5(x1)] =
1 0 0
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[Aa(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[AAa(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[Left(x1)] =
1 0 0
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[End(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AAAb(x1)] =
1 1 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Ab(x1)] =
1 0 1
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[R(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[Right3(x1)] =
1 0 0
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
the rules
L(Begin(x0)) → Right2(Wait(x0))
L(Begin(x0)) → Right3(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(b(Right3(x0))) → End(Ab(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right2(x0)) → Right2(AR(x0))
R(Right3(x0)) → Right3(AR(x0))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[L(x1)] = 4 · x1 + 0
[a(x1)] = 1 · x1 + 0
[Right4(x1)] = 1 · x1 + 0
[Begin(x1)] = 1 · x1 + 5
[Wait(x1)] = 1 · x1 + 5
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 1 · x1 + 0
[AL(x1)] = 4 · x1 + 0
[AR(x1)] = 2 · x1 + 1
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 4 · x1 + 0
[Right5(x1)] = 1 · x1 + 0
[Aa(x1)] = 1 · x1 + 0
[AAa(x1)] = 1 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[End(x1)] = 4 · x1 + 0
[AAAb(x1)] = 1 · x1 + 0
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 2 · x1 + 1
[Right3(x1)] = 4 · x1 + 0
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[L(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right4(x1)] =
1 0 0
0 1 0
0 1 0
· x1 +
0 0 0
1 0 0
0 0 0
[Begin(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Wait(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[b(x1)] =
1 0 1
1 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AAAa(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[AL(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AR(x1)] =
1 0 0
1 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AAb(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right2(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right5(x1)] =
1 0 0
0 1 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Aa(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AAa(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Left(x1)] =
1 0 1
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[End(x1)] =
1 1 1
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[AAAb(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Ab(x1)] =
1 0 0
1 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[R(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right3(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
1 0 0
0 0 0
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[L(x1)] = 8 · x1 + -∞
[a(x1)] = 0 · x1 + -∞
[Right4(x1)] = 0 · x1 + -∞
[Begin(x1)] = 2 · x1 + -∞
[Wait(x1)] = 2 · x1 + -∞
[b(x1)] = 0 · x1 + -∞
[AAAa(x1)] = 0 · x1 + -∞
[AL(x1)] = 8 · x1 + -∞
[AR(x1)] = 0 · x1 + -∞
[AAb(x1)] = 0 · x1 + -∞
[Right2(x1)] = 8 · x1 + -∞
[Right5(x1)] = 0 · x1 + -∞
[Aa(x1)] = 0 · x1 + -∞
[AAa(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[End(x1)] = 4 · x1 + -∞
[AAAb(x1)] = 0 · x1 + -∞
[Ab(x1)] = 0 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[Right3(x1)] = 6 · x1 + -∞
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
L(Begin(x0)) → Right2(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right3(x0)) → Right3(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right3(x0)) → Right3(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[L(x1)] = 1 · x1 + 0
[a(x1)] = 1 · x1 + 0
[Right4(x1)] = 1 · x1 + 0
[Begin(x1)] = 1 · x1 + 0
[Wait(x1)] = 1 · x1 + 0
[b(x1)] = 2 · x1 + 0
[AAAa(x1)] = 1 · x1 + 0
[AL(x1)] = 1 · x1 + 0
[AR(x1)] = 1 · x1 + 0
[AAb(x1)] = 2 · x1 + 0
[Right2(x1)] = 1 · x1 + 0
[Right5(x1)] = 2 · x1 + 0
[Aa(x1)] = 1 · x1 + 0
[AAa(x1)] = 1 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[End(x1)] = 1 · x1 + 1
[AAAb(x1)] = 2 · x1 + 0
[Ab(x1)] = 2 · x1 + 0
[R(x1)] = 1 · x1 + 0
[Right3(x1)] = 1 · x1 + 8
the rules
L(Begin(x0)) → Right2(Wait(x0))
Aa(Begin(x0)) → Right4(Wait(x0))
Ab(Begin(x0)) → Right5(Wait(x0))
End(a(Right2(x0))) → End(Aa(L(Left(x0))))
End(R(Right4(x0))) → End(R(a(Left(x0))))
End(R(Right5(x0))) → End(R(b(Left(x0))))
R(Right4(x0)) → Right4(AR(x0))
R(Right5(x0)) → Right5(AR(x0))
L(Right2(x0)) → Right2(AL(x0))
L(Right3(x0)) → Right3(AL(x0))
L(Right4(x0)) → Right4(AL(x0))
L(Right5(x0)) → Right5(AL(x0))
a(Right2(x0)) → Right2(AAa(x0))
a(Right3(x0)) → Right3(AAa(x0))
a(Right4(x0)) → Right4(AAa(x0))
a(Right5(x0)) → Right5(AAa(x0))
Aa(Right2(x0)) → Right2(AAAa(x0))
Aa(Right3(x0)) → Right3(AAAa(x0))
Aa(Right4(x0)) → Right4(AAAa(x0))
Aa(Right5(x0)) → Right5(AAAa(x0))
b(Right2(x0)) → Right2(AAb(x0))
b(Right4(x0)) → Right4(AAb(x0))
b(Right5(x0)) → Right5(AAb(x0))
Ab(Right2(x0)) → Right2(AAAb(x0))
Ab(Right4(x0)) → Right4(AAAb(x0))
Ab(Right5(x0)) → Right5(AAAb(x0))
Left(AR(x0)) → R(Left(x0))
Left(AL(x0)) → L(Left(x0))
Left(AAa(x0)) → a(Left(x0))
Left(AAAa(x0)) → Aa(Left(x0))
Left(AAb(x0)) → b(Left(x0))
Left(AAAb(x0)) → Ab(Left(x0))
Left(Wait(x0)) → Begin(x0)
L(a(x0)) → Aa(L(x0))
L(b(x0)) → Ab(L(x0))
Aa(R(x0)) → R(a(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
Begin(L(x0)) → Wait(Right2(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[L(x1)] = 1 · x1 + 1
[a(x1)] = 1 · x1 + 0
[Right4(x1)] = 8 · x1 + 0
[Begin(x1)] = 8 · x1 + 0
[Wait(x1)] = 1 · x1 + 0
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 1 · x1 + 0
[AL(x1)] = 1 · x1 + 8
[AR(x1)] = 1 · x1 + 8
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 8 · x1 + 8
[Right5(x1)] = 8 · x1 + 0
[Aa(x1)] = 1 · x1 + 0
[AAa(x1)] = 1 · x1 + 0
[Left(x1)] = 8 · x1 + 0
[End(x1)] = 1 · x1 + 1
[AAAb(x1)] = 1 · x1 + 0
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 1 · x1 + 1
[Right3(x1)] = 10 · x1 + 2
the rules
Begin(L(x0)) → Wait(Right2(x0))
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right2(L(x0)) → AL(Right2(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[L(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right4(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[Begin(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[Wait(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[b(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[AAAa(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AL(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[AR(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AAb(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right2(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right5(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Aa(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AAa(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Left(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[End(x1)] =
1 1 0
0 1 1
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[AAAb(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[Ab(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[R(x1)] =
1 0 0
0 0 0
0 1 1
· x1 +
0 0 0
0 0 0
1 0 0
[Right3(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
the rules
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right2(L(x0)) → AL(Right2(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[L(x1)] = 7 · x1 + -∞
[a(x1)] = 0 · x1 + -∞
[Right4(x1)] = 0 · x1 + -∞
[Begin(x1)] = 0 · x1 + -∞
[Wait(x1)] = 0 · x1 + -∞
[b(x1)] = 0 · x1 + -∞
[AAAa(x1)] = 0 · x1 + -∞
[AL(x1)] = 7 · x1 + -∞
[AR(x1)] = 0 · x1 + -∞
[AAb(x1)] = 0 · x1 + -∞
[Right2(x1)] = 8 · x1 + -∞
[Right5(x1)] = 0 · x1 + -∞
[Aa(x1)] = 0 · x1 + -∞
[AAa(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[End(x1)] = 1 · x1 + -∞
[AAAb(x1)] = 0 · x1 + -∞
[Ab(x1)] = 0 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[Right3(x1)] = 0 · x1 + -∞
the rules
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right2(L(x0)) → AL(Right2(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[L(x1)] = 2 · x1 + 6
[a(x1)] = 4 · x1 + 0
[Right4(x1)] = 4 · x1 + 0
[Begin(x1)] = 4 · x1 + 14
[Wait(x1)] = 4 · x1 + 14
[b(x1)] = 1 · x1 + 0
[AAAa(x1)] = 4 · x1 + 0
[AL(x1)] = 2 · x1 + 6
[AR(x1)] = 1 · x1 + 0
[AAb(x1)] = 1 · x1 + 0
[Right2(x1)] = 4 · x1 + 0
[Right5(x1)] = 1 · x1 + 0
[Aa(x1)] = 4 · x1 + 0
[AAa(x1)] = 4 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[End(x1)] = 1 · x1 + 0
[AAAb(x1)] = 1 · x1 + 0
[Ab(x1)] = 1 · x1 + 0
[R(x1)] = 1 · x1 + 0
[Right3(x1)] = 1 · x1 + 0
the rules
Begin(Aa(x0)) → Wait(Right4(x0))
Begin(Ab(x0)) → Wait(Right5(x0))
Right4(R(End(x0))) → Left(a(R(End(x0))))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
b(L(x0)) → L(Ab(x0))
R(Aa(x0)) → a(R(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 0 · x1 + -∞
[Right4(x1)] = 1 · x1 + -∞
[Begin(x1)] = 0 · x1 + -∞
[Wait(x1)] = 0 · x1 + -∞
[b(x1)] = 0 · x1 + -∞
[AAAa(x1)] = 12 · x1 + -∞
[AL(x1)] = 0 · x1 + -∞
[AR(x1)] = 0 · x1 + -∞
[AAb(x1)] = 0 · x1 + -∞
[Right2(x1)] = 3 · x1 + -∞
[Right5(x1)] = 0 · x1 + -∞
[Aa(x1)] = 12 · x1 + -∞
[AAa(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[End(x1)] = 0 · x1 + -∞
[AAAb(x1)] = 0 · x1 + -∞
[Ab(x1)] = 0 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[Right3(x1)] = 2 · x1 + -∞
the rules
Begin(Ab(x0)) → Wait(Right5(x0))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right5(L(x0)) → AL(Right5(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AR(Left(x0)) → Left(R(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
b(L(x0)) → L(Ab(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[L(x1)] = 1 · x1 + 3
[a(x1)] = 2 · x1 + 3
[Right4(x1)] = 4 · x1 + 1
[Begin(x1)] = 8 · x1 + 7
[Wait(x1)] = 4 · x1 + 7
[b(x1)] = 3 · x1 + 2
[AAAa(x1)] = 4 · x1 + 8
[AL(x1)] = 1 · x1 + 6
[AR(x1)] = 4 · x1 + 12
[AAb(x1)] = 3 · x1 + 4
[Right2(x1)] = 6 · x1 + 4
[Right5(x1)] = 6 · x1 + 4
[Aa(x1)] = 4 · x1 + 4
[AAa(x1)] = 2 · x1 + 8
[Left(x1)] = 2 · x1 + 0
[End(x1)] = 1 · x1 + 0
[AAAb(x1)] = 3 · x1 + 4
[Ab(x1)] = 3 · x1 + 2
[R(x1)] = 4 · x1 + 4
[Right3(x1)] = 3 · x1 + 1
the rules
Begin(Ab(x0)) → Wait(Right5(x0))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right5(R(x0)) → AR(Right5(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AL(Left(x0)) → Left(L(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
Wait(Left(x0)) → Begin(x0)
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[L(x1)] = 3 · x1 + -∞
[a(x1)] = 10 · x1 + -∞
[Begin(x1)] = 14 · x1 + -∞
[Wait(x1)] = 8 · x1 + -∞
[b(x1)] = 1 · x1 + -∞
[AAAa(x1)] = 14 · x1 + -∞
[AL(x1)] = 3 · x1 + -∞
[AR(x1)] = 0 · x1 + -∞
[AAb(x1)] = 1 · x1 + -∞
[Right2(x1)] = 0 · x1 + -∞
[Right5(x1)] = 14 · x1 + -∞
[Aa(x1)] = 5 · x1 + -∞
[AAa(x1)] = 10 · x1 + -∞
[Left(x1)] = 13 · x1 + -∞
[End(x1)] = 1 · x1 + -∞
[AAAb(x1)] = 8 · x1 + -∞
[Ab(x1)] = 8 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[Right3(x1)] = 6 · x1 + -∞
the rules
Begin(Ab(x0)) → Wait(Right5(x0))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right5(R(x0)) → AR(Right5(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AL(Left(x0)) → Left(L(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[L(x1)] = 0 · x1 + -∞
[a(x1)] = 15 · x1 + -∞
[Begin(x1)] = 15 · x1 + -∞
[Wait(x1)] = 8 · x1 + -∞
[b(x1)] = 8 · x1 + -∞
[AL(x1)] = 0 · x1 + -∞
[AR(x1)] = 0 · x1 + -∞
[AAb(x1)] = 8 · x1 + -∞
[Right2(x1)] = 8 · x1 + -∞
[Right5(x1)] = 8 · x1 + -∞
[AAa(x1)] = 12 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[End(x1)] = 0 · x1 + -∞
[AAAb(x1)] = 1 · x1 + -∞
[Ab(x1)] = 1 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[Right3(x1)] = 1 · x1 + -∞
the rules
Begin(Ab(x0)) → Wait(Right5(x0))
Right5(R(End(x0))) → Left(b(R(End(x0))))
Right5(R(x0)) → AR(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AL(Left(x0)) → Left(L(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[L(x1)] = 0 · x1 + -∞
[Begin(x1)] = 13 · x1 + -∞
[Wait(x1)] = 11 · x1 + -∞
[b(x1)] = 0 · x1 + -∞
[AL(x1)] = 14 · x1 + -∞
[AR(x1)] = 0 · x1 + -∞
[AAb(x1)] = 0 · x1 + -∞
[Right2(x1)] = 1 · x1 + -∞
[Right5(x1)] = 2 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[End(x1)] = 0 · x1 + -∞
[AAAb(x1)] = 0 · x1 + -∞
[Ab(x1)] = 0 · x1 + -∞
[R(x1)] = 4 · x1 + -∞
the rules
Begin(Ab(x0)) → Wait(Right5(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Begin(x1)] = 14 · x1 + -∞
[Wait(x1)] = 8 · x1 + -∞
[b(x1)] = 15 · x1 + -∞
[AAb(x1)] = 15 · x1 + -∞
[Right2(x1)] = 12 · x1 + -∞
[Right5(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[AAAb(x1)] = 0 · x1 + -∞
[Ab(x1)] = 0 · x1 + -∞
the rules
Right2(b(x0)) → AAb(Right2(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight function
prec(AAAb) = 1 weight(AAAb) = 1
prec(AAb) = 4 weight(AAb) = 1
prec(b) = 7 weight(b) = 1
prec(Left) = 0 weight(Left) = 1
prec(Right5) = 6 weight(Right5) = 1
prec(Ab) = 0 weight(Ab) = 1
prec(Right2) = 5 weight(Right2) = 1
all rules could be removed.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.