YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(P(x0)) → Wait(Right1(x0))
Begin(P(x0)) → Wait(Right2(x0))
Begin(c(x0)) → Wait(Right3(x0))
Begin(c(x0)) → Wait(Right4(x0))
Begin(c(x0)) → Wait(Right5(x0))
Right1(0(End(x0))) → Left(1(P(End(x0))))
Right2(1(End(x0))) → Left(c(P(End(x0))))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right4(1(End(x0))) → Left(c(0(End(x0))))
Right5(P(End(x0))) → Left(P(End(x0)))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right5(0(x0)) → A0(Right5(x0))
Right1(P(x0)) → AP(Right1(x0))
Right2(P(x0)) → AP(Right2(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right5(P(x0)) → AP(Right5(x0))
Right1(1(x0)) → A1(Right1(x0))
Right2(1(x0)) → A1(Right2(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right5(1(x0)) → A1(Right5(x0))
Right1(c(x0)) → Ac(Right1(x0))
Right2(c(x0)) → Ac(Right2(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
Right5(c(x0)) → Ac(Right5(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))
P(c(x0)) → P(x0)

Proof

1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Right2(x1)] = 0 · x1 + -∞
[A1(x1)] = 8 · x1 + -∞
[Right5(x1)] = 0 · x1 + -∞
[Begin(x1)] = 0 · x1 + -∞
[Wait(x1)] = 0 · x1 + -∞
[Ac(x1)] = 8 · x1 + -∞
[c(x1)] = 8 · x1 + -∞
[0(x1)] = 8 · x1 + -∞
[P(x1)] = 0 · x1 + -∞
[Right4(x1)] = 8 · x1 + -∞
[AP(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[1(x1)] = 8 · x1 + -∞
[End(x1)] = 8 · x1 + -∞
[A0(x1)] = 8 · x1 + -∞
[Right3(x1)] = 8 · x1 + -∞
[Right1(x1)] = 0 · x1 + -∞
the rules
Begin(P(x0)) → Wait(Right1(x0))
Begin(P(x0)) → Wait(Right2(x0))
Begin(c(x0)) → Wait(Right3(x0))
Begin(c(x0)) → Wait(Right4(x0))
Right1(0(End(x0))) → Left(1(P(End(x0))))
Right2(1(End(x0))) → Left(c(P(End(x0))))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right4(1(End(x0))) → Left(c(0(End(x0))))
Right5(P(End(x0))) → Left(P(End(x0)))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right5(0(x0)) → A0(Right5(x0))
Right1(P(x0)) → AP(Right1(x0))
Right2(P(x0)) → AP(Right2(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right5(P(x0)) → AP(Right5(x0))
Right1(1(x0)) → A1(Right1(x0))
Right2(1(x0)) → A1(Right2(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right5(1(x0)) → A1(Right5(x0))
Right1(c(x0)) → Ac(Right1(x0))
Right2(c(x0)) → Ac(Right2(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
Right5(c(x0)) → Ac(Right5(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))
remain.

1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Right2(x1)] = 0 · x1 + -∞
[A1(x1)] = 0 · x1 + -∞
[Right5(x1)] = 1 · x1 + -∞
[Begin(x1)] = 0 · x1 + -∞
[Wait(x1)] = 0 · x1 + -∞
[Ac(x1)] = 0 · x1 + -∞
[c(x1)] = 0 · x1 + -∞
[0(x1)] = 0 · x1 + -∞
[P(x1)] = 0 · x1 + -∞
[Right4(x1)] = 0 · x1 + -∞
[AP(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[1(x1)] = 0 · x1 + -∞
[End(x1)] = 0 · x1 + -∞
[A0(x1)] = 0 · x1 + -∞
[Right3(x1)] = 0 · x1 + -∞
[Right1(x1)] = 0 · x1 + -∞
the rules
Begin(P(x0)) → Wait(Right1(x0))
Begin(P(x0)) → Wait(Right2(x0))
Begin(c(x0)) → Wait(Right3(x0))
Begin(c(x0)) → Wait(Right4(x0))
Right1(0(End(x0))) → Left(1(P(End(x0))))
Right2(1(End(x0))) → Left(c(P(End(x0))))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right4(1(End(x0))) → Left(c(0(End(x0))))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right5(0(x0)) → A0(Right5(x0))
Right1(P(x0)) → AP(Right1(x0))
Right2(P(x0)) → AP(Right2(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right5(P(x0)) → AP(Right5(x0))
Right1(1(x0)) → A1(Right1(x0))
Right2(1(x0)) → A1(Right2(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right5(1(x0)) → A1(Right5(x0))
Right1(c(x0)) → Ac(Right1(x0))
Right2(c(x0)) → Ac(Right2(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
Right5(c(x0)) → Ac(Right5(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))
remain.

1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
P(Begin(x0)) → Right1(Wait(x0))
P(Begin(x0)) → Right2(Wait(x0))
c(Begin(x0)) → Right3(Wait(x0))
c(Begin(x0)) → Right4(Wait(x0))
End(0(Right1(x0))) → End(P(1(Left(x0))))
End(1(Right2(x0))) → End(P(c(Left(x0))))
End(0(Right3(x0))) → End(0(1(Left(x0))))
End(1(Right4(x0))) → End(0(c(Left(x0))))
0(Right1(x0)) → Right1(A0(x0))
0(Right2(x0)) → Right2(A0(x0))
0(Right3(x0)) → Right3(A0(x0))
0(Right4(x0)) → Right4(A0(x0))
0(Right5(x0)) → Right5(A0(x0))
P(Right1(x0)) → Right1(AP(x0))
P(Right2(x0)) → Right2(AP(x0))
P(Right3(x0)) → Right3(AP(x0))
P(Right4(x0)) → Right4(AP(x0))
P(Right5(x0)) → Right5(AP(x0))
1(Right1(x0)) → Right1(A1(x0))
1(Right2(x0)) → Right2(A1(x0))
1(Right3(x0)) → Right3(A1(x0))
1(Right4(x0)) → Right4(A1(x0))
1(Right5(x0)) → Right5(A1(x0))
c(Right1(x0)) → Right1(Ac(x0))
c(Right2(x0)) → Right2(Ac(x0))
c(Right3(x0)) → Right3(Ac(x0))
c(Right4(x0)) → Right4(Ac(x0))
c(Right5(x0)) → Right5(Ac(x0))
Left(A0(x0)) → 0(Left(x0))
Left(AP(x0)) → P(Left(x0))
Left(A1(x0)) → 1(Left(x0))
Left(Ac(x0)) → c(Left(x0))
Left(Wait(x0)) → Begin(x0)
P(0(x0)) → P(1(x0))
P(1(x0)) → P(c(x0))
c(0(x0)) → 0(1(x0))
c(1(x0)) → 0(c(x0))

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[Right2(x1)] = 4 · x1 + 0
[A1(x1)] = 4 · x1 + 0
[Right5(x1)] = 1 · x1 + 3
[Begin(x1)] = 1 · x1 + 0
[Wait(x1)] = 1 · x1 + 0
[Ac(x1)] = 4 · x1 + 0
[c(x1)] = 4 · x1 + 0
[0(x1)] = 4 · x1 + 0
[P(x1)] = 4 · x1 + 0
[Right4(x1)] = 4 · x1 + 0
[AP(x1)] = 4 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[1(x1)] = 4 · x1 + 0
[End(x1)] = 1 · x1 + 0
[A0(x1)] = 4 · x1 + 0
[Right3(x1)] = 4 · x1 + 0
[Right1(x1)] = 4 · x1 + 0
the rules
P(Begin(x0)) → Right1(Wait(x0))
P(Begin(x0)) → Right2(Wait(x0))
c(Begin(x0)) → Right3(Wait(x0))
c(Begin(x0)) → Right4(Wait(x0))
End(0(Right1(x0))) → End(P(1(Left(x0))))
End(1(Right2(x0))) → End(P(c(Left(x0))))
End(0(Right3(x0))) → End(0(1(Left(x0))))
End(1(Right4(x0))) → End(0(c(Left(x0))))
0(Right1(x0)) → Right1(A0(x0))
0(Right2(x0)) → Right2(A0(x0))
0(Right3(x0)) → Right3(A0(x0))
0(Right4(x0)) → Right4(A0(x0))
P(Right1(x0)) → Right1(AP(x0))
P(Right2(x0)) → Right2(AP(x0))
P(Right3(x0)) → Right3(AP(x0))
P(Right4(x0)) → Right4(AP(x0))
1(Right1(x0)) → Right1(A1(x0))
1(Right2(x0)) → Right2(A1(x0))
1(Right3(x0)) → Right3(A1(x0))
1(Right4(x0)) → Right4(A1(x0))
c(Right1(x0)) → Right1(Ac(x0))
c(Right2(x0)) → Right2(Ac(x0))
c(Right3(x0)) → Right3(Ac(x0))
c(Right4(x0)) → Right4(Ac(x0))
Left(A0(x0)) → 0(Left(x0))
Left(AP(x0)) → P(Left(x0))
Left(A1(x0)) → 1(Left(x0))
Left(Ac(x0)) → c(Left(x0))
Left(Wait(x0)) → Begin(x0)
P(0(x0)) → P(1(x0))
P(1(x0)) → P(c(x0))
c(0(x0)) → 0(1(x0))
c(1(x0)) → 0(c(x0))
remain.

1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
Begin(P(x0)) → Wait(Right1(x0))
Begin(P(x0)) → Wait(Right2(x0))
Begin(c(x0)) → Wait(Right3(x0))
Begin(c(x0)) → Wait(Right4(x0))
Right1(0(End(x0))) → Left(1(P(End(x0))))
Right2(1(End(x0))) → Left(c(P(End(x0))))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right4(1(End(x0))) → Left(c(0(End(x0))))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right1(P(x0)) → AP(Right1(x0))
Right2(P(x0)) → AP(Right2(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right1(1(x0)) → A1(Right1(x0))
Right2(1(x0)) → A1(Right2(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right1(c(x0)) → Ac(Right1(x0))
Right2(c(x0)) → Ac(Right2(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))

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
[Right2(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[A1(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[Begin(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Wait(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Ac(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[c(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[0(x1)] =
1 0 0
1 1 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[P(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[Right4(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[AP(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[Left(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[1(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[End(x1)] =
1 0 1
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[A0(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[Right3(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right1(x1)] =
1 0 0
0 0 1
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
the rules
Begin(c(x0)) → Wait(Right3(x0))
Begin(c(x0)) → Wait(Right4(x0))
Right1(0(End(x0))) → Left(1(P(End(x0))))
Right2(1(End(x0))) → Left(c(P(End(x0))))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right4(1(End(x0))) → Left(c(0(End(x0))))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right1(P(x0)) → AP(Right1(x0))
Right2(P(x0)) → AP(Right2(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right1(1(x0)) → A1(Right1(x0))
Right2(1(x0)) → A1(Right2(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right1(c(x0)) → Ac(Right1(x0))
Right2(c(x0)) → Ac(Right2(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))
remain.

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Right2(x1)] = 4 · x1 + -∞
[A1(x1)] = 0 · x1 + -∞
[Begin(x1)] = 6 · x1 + -∞
[Wait(x1)] = 4 · x1 + -∞
[Ac(x1)] = 0 · x1 + -∞
[c(x1)] = 0 · x1 + -∞
[0(x1)] = 0 · x1 + -∞
[P(x1)] = 0 · x1 + -∞
[Right4(x1)] = 2 · x1 + -∞
[AP(x1)] = 0 · x1 + -∞
[Left(x1)] = 2 · x1 + -∞
[1(x1)] = 0 · x1 + -∞
[End(x1)] = 0 · x1 + -∞
[A0(x1)] = 0 · x1 + -∞
[Right3(x1)] = 2 · x1 + -∞
[Right1(x1)] = 2 · x1 + -∞
the rules
Begin(c(x0)) → Wait(Right3(x0))
Begin(c(x0)) → Wait(Right4(x0))
Right1(0(End(x0))) → Left(1(P(End(x0))))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right4(1(End(x0))) → Left(c(0(End(x0))))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right1(P(x0)) → AP(Right1(x0))
Right2(P(x0)) → AP(Right2(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right1(1(x0)) → A1(Right1(x0))
Right2(1(x0)) → A1(Right2(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right1(c(x0)) → Ac(Right1(x0))
Right2(c(x0)) → Ac(Right2(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))
remain.

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[Right2(x1)] = 4 · x1 + -∞
[A1(x1)] = 0 · x1 + -∞
[Begin(x1)] = 8 · x1 + -∞
[Wait(x1)] = 8 · x1 + -∞
[Ac(x1)] = 0 · x1 + -∞
[c(x1)] = 0 · x1 + -∞
[0(x1)] = 0 · x1 + -∞
[P(x1)] = 0 · x1 + -∞
[Right4(x1)] = 0 · x1 + -∞
[AP(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[1(x1)] = 0 · x1 + -∞
[End(x1)] = 1 · x1 + -∞
[A0(x1)] = 0 · x1 + -∞
[Right3(x1)] = 0 · x1 + -∞
[Right1(x1)] = 1 · x1 + -∞
the rules
Begin(c(x0)) → Wait(Right3(x0))
Begin(c(x0)) → Wait(Right4(x0))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right4(1(End(x0))) → Left(c(0(End(x0))))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right1(P(x0)) → AP(Right1(x0))
Right2(P(x0)) → AP(Right2(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right1(1(x0)) → A1(Right1(x0))
Right2(1(x0)) → A1(Right2(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right1(c(x0)) → Ac(Right1(x0))
Right2(c(x0)) → Ac(Right2(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(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
c(Begin(x0)) → Right3(Wait(x0))
c(Begin(x0)) → Right4(Wait(x0))
End(0(Right3(x0))) → End(0(1(Left(x0))))
End(1(Right4(x0))) → End(0(c(Left(x0))))
0(Right1(x0)) → Right1(A0(x0))
0(Right2(x0)) → Right2(A0(x0))
0(Right3(x0)) → Right3(A0(x0))
0(Right4(x0)) → Right4(A0(x0))
P(Right1(x0)) → Right1(AP(x0))
P(Right2(x0)) → Right2(AP(x0))
P(Right3(x0)) → Right3(AP(x0))
P(Right4(x0)) → Right4(AP(x0))
1(Right1(x0)) → Right1(A1(x0))
1(Right2(x0)) → Right2(A1(x0))
1(Right3(x0)) → Right3(A1(x0))
1(Right4(x0)) → Right4(A1(x0))
c(Right1(x0)) → Right1(Ac(x0))
c(Right2(x0)) → Right2(Ac(x0))
c(Right3(x0)) → Right3(Ac(x0))
c(Right4(x0)) → Right4(Ac(x0))
Left(A0(x0)) → 0(Left(x0))
Left(AP(x0)) → P(Left(x0))
Left(A1(x0)) → 1(Left(x0))
Left(Ac(x0)) → c(Left(x0))
Left(Wait(x0)) → Begin(x0)
P(0(x0)) → P(1(x0))
P(1(x0)) → P(c(x0))
c(0(x0)) → 0(1(x0))
c(1(x0)) → 0(c(x0))

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[Right2(x1)] = 8 · x1 + 4
[A1(x1)] = 1 · x1 + 0
[Begin(x1)] = 4 · x1 + 0
[Wait(x1)] = 1 · x1 + 0
[Ac(x1)] = 1 · x1 + 0
[c(x1)] = 1 · x1 + 0
[0(x1)] = 1 · x1 + 0
[P(x1)] = 2 · x1 + 0
[Right4(x1)] = 4 · x1 + 0
[AP(x1)] = 2 · x1 + 0
[Left(x1)] = 4 · x1 + 0
[1(x1)] = 1 · x1 + 0
[End(x1)] = 4 · x1 + 8
[A0(x1)] = 1 · x1 + 0
[Right3(x1)] = 4 · x1 + 0
[Right1(x1)] = 8 · x1 + 2
the rules
c(Begin(x0)) → Right3(Wait(x0))
c(Begin(x0)) → Right4(Wait(x0))
End(0(Right3(x0))) → End(0(1(Left(x0))))
End(1(Right4(x0))) → End(0(c(Left(x0))))
0(Right1(x0)) → Right1(A0(x0))
0(Right2(x0)) → Right2(A0(x0))
0(Right3(x0)) → Right3(A0(x0))
0(Right4(x0)) → Right4(A0(x0))
P(Right3(x0)) → Right3(AP(x0))
P(Right4(x0)) → Right4(AP(x0))
1(Right1(x0)) → Right1(A1(x0))
1(Right2(x0)) → Right2(A1(x0))
1(Right3(x0)) → Right3(A1(x0))
1(Right4(x0)) → Right4(A1(x0))
c(Right1(x0)) → Right1(Ac(x0))
c(Right2(x0)) → Right2(Ac(x0))
c(Right3(x0)) → Right3(Ac(x0))
c(Right4(x0)) → Right4(Ac(x0))
Left(A0(x0)) → 0(Left(x0))
Left(AP(x0)) → P(Left(x0))
Left(A1(x0)) → 1(Left(x0))
Left(Ac(x0)) → c(Left(x0))
Left(Wait(x0)) → Begin(x0)
P(0(x0)) → P(1(x0))
P(1(x0)) → P(c(x0))
c(0(x0)) → 0(1(x0))
c(1(x0)) → 0(c(x0))
remain.

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[Right2(x1)] = 8 · x1 + 1
[A1(x1)] = 2 · x1 + 0
[Begin(x1)] = 8 · x1 + 0
[Wait(x1)] = 8 · x1 + 0
[Ac(x1)] = 2 · x1 + 0
[c(x1)] = 2 · x1 + 0
[0(x1)] = 2 · x1 + 0
[P(x1)] = 1 · x1 + 0
[Right4(x1)] = 2 · x1 + 0
[AP(x1)] = 1 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[1(x1)] = 2 · x1 + 0
[End(x1)] = 4 · x1 + 4
[A0(x1)] = 2 · x1 + 0
[Right3(x1)] = 2 · x1 + 0
[Right1(x1)] = 8 · x1 + 2
the rules
c(Begin(x0)) → Right3(Wait(x0))
c(Begin(x0)) → Right4(Wait(x0))
End(0(Right3(x0))) → End(0(1(Left(x0))))
End(1(Right4(x0))) → End(0(c(Left(x0))))
0(Right3(x0)) → Right3(A0(x0))
0(Right4(x0)) → Right4(A0(x0))
P(Right3(x0)) → Right3(AP(x0))
P(Right4(x0)) → Right4(AP(x0))
1(Right3(x0)) → Right3(A1(x0))
1(Right4(x0)) → Right4(A1(x0))
c(Right3(x0)) → Right3(Ac(x0))
c(Right4(x0)) → Right4(Ac(x0))
Left(A0(x0)) → 0(Left(x0))
Left(AP(x0)) → P(Left(x0))
Left(A1(x0)) → 1(Left(x0))
Left(Ac(x0)) → c(Left(x0))
Left(Wait(x0)) → Begin(x0)
P(0(x0)) → P(1(x0))
P(1(x0)) → P(c(x0))
c(0(x0)) → 0(1(x0))
c(1(x0)) → 0(c(x0))
remain.

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(c(x0)) → Wait(Right3(x0))
Begin(c(x0)) → Wait(Right4(x0))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right4(1(End(x0))) → Left(c(0(End(x0))))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))

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
[A1(x1)] =
1 0 1
0 1 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[Begin(x1)] =
1 0 1
0 0 0
1 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[Wait(x1)] =
1 0 0
0 1 0
1 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[Ac(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[c(x1)] =
1 0 0
0 0 0
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[0(x1)] =
1 0 0
0 0 0
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[P(x1)] =
1 1 0
0 0 0
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[Right4(x1)] =
1 1 1
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[AP(x1)] =
1 1 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Left(x1)] =
1 0 1
0 1 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[1(x1)] =
1 0 0
0 1 0
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[End(x1)] =
1 1 1
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
1 0 0
[A0(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Right3(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
the rules
Begin(c(x0)) → Wait(Right3(x0))
Begin(c(x0)) → Wait(Right4(x0))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))
remain.

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
[A1(x1)] = 0 · x1 + -∞
[Begin(x1)] = 15 · x1 + -∞
[Wait(x1)] = 11 · x1 + -∞
[Ac(x1)] = 0 · x1 + -∞
[c(x1)] = 0 · x1 + -∞
[0(x1)] = 0 · x1 + -∞
[P(x1)] = 0 · x1 + -∞
[Right4(x1)] = 0 · x1 + -∞
[AP(x1)] = 0 · x1 + -∞
[Left(x1)] = 4 · x1 + -∞
[1(x1)] = 0 · x1 + -∞
[End(x1)] = 0 · x1 + -∞
[A0(x1)] = 0 · x1 + -∞
[Right3(x1)] = 4 · x1 + -∞
the rules
Begin(c(x0)) → Wait(Right3(x0))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right3(P(x0)) → AP(Right3(x0))
Right4(P(x0)) → AP(Right4(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))
remain.

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
c(Begin(x0)) → Right3(Wait(x0))
End(0(Right3(x0))) → End(0(1(Left(x0))))
0(Right3(x0)) → Right3(A0(x0))
0(Right4(x0)) → Right4(A0(x0))
P(Right3(x0)) → Right3(AP(x0))
P(Right4(x0)) → Right4(AP(x0))
1(Right3(x0)) → Right3(A1(x0))
1(Right4(x0)) → Right4(A1(x0))
c(Right3(x0)) → Right3(Ac(x0))
c(Right4(x0)) → Right4(Ac(x0))
Left(A0(x0)) → 0(Left(x0))
Left(AP(x0)) → P(Left(x0))
Left(A1(x0)) → 1(Left(x0))
Left(Ac(x0)) → c(Left(x0))
Left(Wait(x0)) → Begin(x0)
P(0(x0)) → P(1(x0))
P(1(x0)) → P(c(x0))
c(0(x0)) → 0(1(x0))
c(1(x0)) → 0(c(x0))

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
[A1(x1)] = 1 · x1 + 0
[Begin(x1)] = 1 · x1 + 0
[Wait(x1)] = 1 · x1 + 0
[Ac(x1)] = 1 · x1 + 0
[c(x1)] = 1 · x1 + 0
[0(x1)] = 1 · x1 + 0
[P(x1)] = 8 · x1 + 2
[Right4(x1)] = 2 · x1 + 2
[AP(x1)] = 8 · x1 + 2
[Left(x1)] = 1 · x1 + 0
[1(x1)] = 1 · x1 + 0
[End(x1)] = 2 · x1 + 0
[A0(x1)] = 1 · x1 + 0
[Right3(x1)] = 1 · x1 + 0
the rules
c(Begin(x0)) → Right3(Wait(x0))
End(0(Right3(x0))) → End(0(1(Left(x0))))
0(Right3(x0)) → Right3(A0(x0))
0(Right4(x0)) → Right4(A0(x0))
P(Right3(x0)) → Right3(AP(x0))
1(Right3(x0)) → Right3(A1(x0))
1(Right4(x0)) → Right4(A1(x0))
c(Right3(x0)) → Right3(Ac(x0))
c(Right4(x0)) → Right4(Ac(x0))
Left(A0(x0)) → 0(Left(x0))
Left(AP(x0)) → P(Left(x0))
Left(A1(x0)) → 1(Left(x0))
Left(Ac(x0)) → c(Left(x0))
Left(Wait(x0)) → Begin(x0)
P(0(x0)) → P(1(x0))
P(1(x0)) → P(c(x0))
c(0(x0)) → 0(1(x0))
c(1(x0)) → 0(c(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
[A1(x1)] = 4 · x1 + 0
[Begin(x1)] = 2 · x1 + 0
[Wait(x1)] = 2 · x1 + 0
[Ac(x1)] = 4 · x1 + 0
[c(x1)] = 4 · x1 + 0
[0(x1)] = 4 · x1 + 0
[P(x1)] = 1 · x1 + 0
[Right4(x1)] = 1 · x1 + 5
[AP(x1)] = 1 · x1 + 0
[Left(x1)] = 1 · x1 + 0
[1(x1)] = 4 · x1 + 0
[End(x1)] = 1 · x1 + 12
[A0(x1)] = 4 · x1 + 0
[Right3(x1)] = 4 · x1 + 0
the rules
c(Begin(x0)) → Right3(Wait(x0))
End(0(Right3(x0))) → End(0(1(Left(x0))))
0(Right3(x0)) → Right3(A0(x0))
P(Right3(x0)) → Right3(AP(x0))
1(Right3(x0)) → Right3(A1(x0))
c(Right3(x0)) → Right3(Ac(x0))
Left(A0(x0)) → 0(Left(x0))
Left(AP(x0)) → P(Left(x0))
Left(A1(x0)) → 1(Left(x0))
Left(Ac(x0)) → c(Left(x0))
Left(Wait(x0)) → Begin(x0)
P(0(x0)) → P(1(x0))
P(1(x0)) → P(c(x0))
c(0(x0)) → 0(1(x0))
c(1(x0)) → 0(c(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(c(x0)) → Wait(Right3(x0))
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right3(0(x0)) → A0(Right3(x0))
Right3(P(x0)) → AP(Right3(x0))
Right3(1(x0)) → A1(Right3(x0))
Right3(c(x0)) → Ac(Right3(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(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 (3 x 3)-matrices with strict dimension 1 over the naturals
[A1(x1)] =
1 0 0
0 1 0
1 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[Begin(x1)] =
1 1 0
0 0 1
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[Wait(x1)] =
1 0 1
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[Ac(x1)] =
1 0 0
0 1 0
1 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[c(x1)] =
1 0 0
1 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[0(x1)] =
1 0 0
1 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[P(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[AP(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
1 0 0
[Left(x1)] =
1 0 0
0 0 1
0 1 0
· x1 +
0 0 0
0 0 0
1 0 0
[1(x1)] =
1 0 0
1 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[End(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[A0(x1)] =
1 0 0
0 1 0
1 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[Right3(x1)] =
1 0 0
0 0 1
1 1 1
· x1 +
0 0 0
0 0 0
0 0 0
the rules
Right3(0(End(x0))) → Left(1(0(End(x0))))
Right3(0(x0)) → A0(Right3(x0))
Right3(P(x0)) → AP(Right3(x0))
Right3(1(x0)) → A1(Right3(x0))
Right3(c(x0)) → Ac(Right3(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))
remain.

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
[A1(x1)] = 0 · x1 + -∞
[Begin(x1)] = 0 · x1 + -∞
[Wait(x1)] = 0 · x1 + -∞
[Ac(x1)] = 0 · x1 + -∞
[c(x1)] = 0 · x1 + -∞
[0(x1)] = 0 · x1 + -∞
[P(x1)] = 0 · x1 + -∞
[AP(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[1(x1)] = 0 · x1 + -∞
[End(x1)] = 2 · x1 + -∞
[A0(x1)] = 0 · x1 + -∞
[Right3(x1)] = 10 · x1 + -∞
the rules
Right3(0(x0)) → A0(Right3(x0))
Right3(P(x0)) → AP(Right3(x0))
Right3(1(x0)) → A1(Right3(x0))
Right3(c(x0)) → Ac(Right3(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
Wait(Left(x0)) → Begin(x0)
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(x0))
remain.

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
[A1(x1)] = 0 · x1 + -∞
[Begin(x1)] = 0 · x1 + -∞
[Wait(x1)] = 8 · x1 + -∞
[Ac(x1)] = 0 · x1 + -∞
[c(x1)] = 0 · x1 + -∞
[0(x1)] = 0 · x1 + -∞
[P(x1)] = 0 · x1 + -∞
[AP(x1)] = 0 · x1 + -∞
[Left(x1)] = 0 · x1 + -∞
[1(x1)] = 0 · x1 + -∞
[A0(x1)] = 0 · x1 + -∞
[Right3(x1)] = 1 · x1 + -∞
the rules
Right3(0(x0)) → A0(Right3(x0))
Right3(P(x0)) → AP(Right3(x0))
Right3(1(x0)) → A1(Right3(x0))
Right3(c(x0)) → Ac(Right3(x0))
A0(Left(x0)) → Left(0(x0))
AP(Left(x0)) → Left(P(x0))
A1(Left(x0)) → Left(1(x0))
Ac(Left(x0)) → Left(c(x0))
0(P(x0)) → 1(P(x0))
1(P(x0)) → c(P(x0))
0(c(x0)) → 1(0(x0))
1(c(x0)) → c(0(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 Knuth Bendix order with w0 = 1 and the following precedence and weight function
prec(Ac) = 2 weight(Ac) = 1
prec(A1) = 2 weight(A1) = 1
prec(AP) = 2 weight(AP) = 1
prec(A0) = 2 weight(A0) = 1
prec(Left) = 0 weight(Left) = 1
prec(1) = 2 weight(1) = 1
prec(0) = 3 weight(0) = 1
prec(Right3) = 15 weight(Right3) = 0
prec(c) = 0 weight(c) = 1
prec(P) = 0 weight(P) = 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 R is empty

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