YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(1(x0))	→	Wait(Right1(x0))
Begin(4(x0))	→	Wait(Right2(x0))
Begin(4(x0))	→	Wait(Right3(x0))
Right1(2(End(x0)))	→	Left(4(1(End(x0))))
Right2(3(End(x0)))	→	Left(4(2(End(x0))))
Right3(2(End(x0)))	→	Left(3(2(End(x0))))
Right1(2(x0))	→	A2(Right1(x0))
Right2(2(x0))	→	A2(Right2(x0))
Right3(2(x0))	→	A2(Right3(x0))
Right1(1(x0))	→	A1(Right1(x0))
Right2(1(x0))	→	A1(Right2(x0))
Right3(1(x0))	→	A1(Right3(x0))
Right1(4(x0))	→	A4(Right1(x0))
Right2(4(x0))	→	A4(Right2(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right1(3(x0))	→	A3(Right1(x0))
Right2(3(x0))	→	A3(Right2(x0))
Right3(3(x0))	→	A3(Right3(x0))
A2(Left(x0))	→	Left(2(x0))
A1(Left(x0))	→	Left(1(x0))
A4(Left(x0))	→	Left(4(x0))
A3(Left(x0))	→	Left(3(x0))
Wait(Left(x0))	→	Begin(x0)
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(x0))

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

1(Begin(x0))	→	Right1(Wait(x0))
4(Begin(x0))	→	Right2(Wait(x0))
4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right1(x0)))	→	End(1(4(Left(x0))))
End(3(Right2(x0)))	→	End(2(4(Left(x0))))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right1(x0))	→	Right1(A2(x0))
2(Right2(x0))	→	Right2(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
1(Right1(x0))	→	Right1(A1(x0))
1(Right2(x0))	→	Right2(A1(x0))
1(Right3(x0))	→	Right3(A1(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right2(x0))	→	Right2(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right1(x0))	→	Right1(A3(x0))
3(Right2(x0))	→	Right2(A3(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[4(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[2(x₁)]

1	0	0
1	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Begin(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Wait(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[Right2(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[3(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[1(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[End(x₁)]

1	1	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[A3(x₁)]

1	0	0
0	0	0
1	0	1

· x₁ +

0	0	0
0	0	0
1	0	0

[A1(x₁)]

1	0	0
0	0	0
1	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[A2(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Left(x₁)]

1	0	0
1	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[A4(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right3(x₁)]

1	1	0
0	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right1(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

the rules

1(Begin(x0))	→	Right1(Wait(x0))
4(Begin(x0))	→	Right2(Wait(x0))
4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right1(x0)))	→	End(1(4(Left(x0))))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right1(x0))	→	Right1(A2(x0))
2(Right2(x0))	→	Right2(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
1(Right1(x0))	→	Right1(A1(x0))
1(Right2(x0))	→	Right2(A1(x0))
1(Right3(x0))	→	Right3(A1(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right2(x0))	→	Right2(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right1(x0))	→	Right1(A3(x0))
3(Right2(x0))	→	Right2(A3(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

remain.

1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[4(x₁)]	=	1 · x₁ + -∞
[2(x₁)]	=	1 · x₁ + -∞
[Begin(x₁)]	=	1 · x₁ + -∞
[Wait(x₁)]	=	0 · x₁ + -∞
[Right2(x₁)]	=	0 · x₁ + -∞
[3(x₁)]	=	1 · x₁ + -∞
[1(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	0 · x₁ + -∞
[A3(x₁)]	=	1 · x₁ + -∞
[A1(x₁)]	=	0 · x₁ + -∞
[A2(x₁)]	=	1 · x₁ + -∞
[Left(x₁)]	=	1 · x₁ + -∞
[A4(x₁)]	=	1 · x₁ + -∞
[Right3(x₁)]	=	2 · x₁ + -∞
[Right1(x₁)]	=	1 · x₁ + -∞

the rules

1(Begin(x0))	→	Right1(Wait(x0))
4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right1(x0)))	→	End(1(4(Left(x0))))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right1(x0))	→	Right1(A2(x0))
2(Right2(x0))	→	Right2(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
1(Right1(x0))	→	Right1(A1(x0))
1(Right2(x0))	→	Right2(A1(x0))
1(Right3(x0))	→	Right3(A1(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right2(x0))	→	Right2(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right1(x0))	→	Right1(A3(x0))
3(Right2(x0))	→	Right2(A3(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

remain.

1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

Begin(1(x0))	→	Wait(Right1(x0))
Begin(4(x0))	→	Wait(Right3(x0))
Right1(2(End(x0)))	→	Left(4(1(End(x0))))
Right3(2(End(x0)))	→	Left(3(2(End(x0))))
Right1(2(x0))	→	A2(Right1(x0))
Right2(2(x0))	→	A2(Right2(x0))
Right3(2(x0))	→	A2(Right3(x0))
Right1(1(x0))	→	A1(Right1(x0))
Right2(1(x0))	→	A1(Right2(x0))
Right3(1(x0))	→	A1(Right3(x0))
Right1(4(x0))	→	A4(Right1(x0))
Right2(4(x0))	→	A4(Right2(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right1(3(x0))	→	A3(Right1(x0))
Right2(3(x0))	→	A3(Right2(x0))
Right3(3(x0))	→	A3(Right3(x0))
A2(Left(x0))	→	Left(2(x0))
A1(Left(x0))	→	Left(1(x0))
A4(Left(x0))	→	Left(4(x0))
A3(Left(x0))	→	Left(3(x0))
Wait(Left(x0))	→	Begin(x0)
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(x0))

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[4(x₁)]	=	1 · x₁ + 1
[2(x₁)]	=	1 · x₁ + 1
[Begin(x₁)]	=	4 · x₁ + 12
[Wait(x₁)]	=	2 · x₁ + 0
[Right2(x₁)]	=	4 · x₁ + 8
[3(x₁)]	=	1 · x₁ + 1
[1(x₁)]	=	1 · x₁ + 0
[End(x₁)]	=	4 · x₁ + 6
[A3(x₁)]	=	1 · x₁ + 2
[A1(x₁)]	=	1 · x₁ + 0
[A2(x₁)]	=	1 · x₁ + 2
[Left(x₁)]	=	2 · x₁ + 6
[A4(x₁)]	=	1 · x₁ + 2
[Right3(x₁)]	=	2 · x₁ + 8
[Right1(x₁)]	=	2 · x₁ + 6

the rules

Begin(1(x0))	→	Wait(Right1(x0))
Begin(4(x0))	→	Wait(Right3(x0))
Right1(2(End(x0)))	→	Left(4(1(End(x0))))
Right3(2(End(x0)))	→	Left(3(2(End(x0))))
Right1(2(x0))	→	A2(Right1(x0))
Right3(2(x0))	→	A2(Right3(x0))
Right1(1(x0))	→	A1(Right1(x0))
Right2(1(x0))	→	A1(Right2(x0))
Right3(1(x0))	→	A1(Right3(x0))
Right1(4(x0))	→	A4(Right1(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right1(3(x0))	→	A3(Right1(x0))
Right3(3(x0))	→	A3(Right3(x0))
A2(Left(x0))	→	Left(2(x0))
A1(Left(x0))	→	Left(1(x0))
A4(Left(x0))	→	Left(4(x0))
A3(Left(x0))	→	Left(3(x0))
Wait(Left(x0))	→	Begin(x0)
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(x0))

remain.

1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

1(Begin(x0))	→	Right1(Wait(x0))
4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right1(x0)))	→	End(1(4(Left(x0))))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right1(x0))	→	Right1(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
1(Right1(x0))	→	Right1(A1(x0))
1(Right2(x0))	→	Right2(A1(x0))
1(Right3(x0))	→	Right3(A1(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right1(x0))	→	Right1(A3(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[4(x₁)]	=	1 · x₁ + 0
[2(x₁)]	=	1 · x₁ + 0
[Begin(x₁)]	=	4 · x₁ + 0
[Wait(x₁)]	=	1 · x₁ + 0
[Right2(x₁)]	=	10 · x₁ + 8
[3(x₁)]	=	1 · x₁ + 0
[1(x₁)]	=	2 · x₁ + 0
[End(x₁)]	=	1 · x₁ + 0
[A3(x₁)]	=	1 · x₁ + 0
[A1(x₁)]	=	2 · x₁ + 0
[A2(x₁)]	=	1 · x₁ + 0
[Left(x₁)]	=	4 · x₁ + 0
[A4(x₁)]	=	1 · x₁ + 0
[Right3(x₁)]	=	4 · x₁ + 0
[Right1(x₁)]	=	8 · x₁ + 0

the rules

1(Begin(x0))	→	Right1(Wait(x0))
4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right1(x0)))	→	End(1(4(Left(x0))))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right1(x0))	→	Right1(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
1(Right1(x0))	→	Right1(A1(x0))
1(Right3(x0))	→	Right3(A1(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right1(x0))	→	Right1(A3(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

remain.

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

[4(x₁)]

1	0	0
0	0	1
1	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[2(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Begin(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Wait(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[3(x₁)]

1	0	0
1	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[1(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[End(x₁)]

1	0	1
0	0	0
1	0	1

· x₁ +

1	0	0
0	0	0
1	0	0

[A3(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[A1(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[A2(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Left(x₁)]

1	0	0
1	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[A4(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right3(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right1(x₁)]

1	0	0
0	0	0
0	1	0

· x₁ +

1	0	0
0	0	0
0	0	0

the rules

1(Begin(x0))	→	Right1(Wait(x0))
4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right1(x0))	→	Right1(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
1(Right1(x0))	→	Right1(A1(x0))
1(Right3(x0))	→	Right3(A1(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right1(x0))	→	Right1(A3(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

remain.

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[4(x₁)]	=	0 · x₁ + -∞
[2(x₁)]	=	0 · x₁ + -∞
[Begin(x₁)]	=	3 · x₁ + -∞
[Wait(x₁)]	=	3 · x₁ + -∞
[3(x₁)]	=	0 · x₁ + -∞
[1(x₁)]	=	1 · x₁ + -∞
[End(x₁)]	=	0 · x₁ + -∞
[A3(x₁)]	=	0 · x₁ + -∞
[A1(x₁)]	=	1 · x₁ + -∞
[A2(x₁)]	=	0 · x₁ + -∞
[Left(x₁)]	=	0 · x₁ + -∞
[A4(x₁)]	=	0 · x₁ + -∞
[Right3(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	0 · x₁ + -∞

the rules

4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right1(x0))	→	Right1(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
1(Right1(x0))	→	Right1(A1(x0))
1(Right3(x0))	→	Right3(A1(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right1(x0))	→	Right1(A3(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

remain.

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(4(x0))	→	Wait(Right3(x0))
Right3(2(End(x0)))	→	Left(3(2(End(x0))))
Right1(2(x0))	→	A2(Right1(x0))
Right3(2(x0))	→	A2(Right3(x0))
Right1(1(x0))	→	A1(Right1(x0))
Right3(1(x0))	→	A1(Right3(x0))
Right1(4(x0))	→	A4(Right1(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right1(3(x0))	→	A3(Right1(x0))
Right3(3(x0))	→	A3(Right3(x0))
A2(Left(x0))	→	Left(2(x0))
A1(Left(x0))	→	Left(1(x0))
A4(Left(x0))	→	Left(4(x0))
A3(Left(x0))	→	Left(3(x0))
Wait(Left(x0))	→	Begin(x0)
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(x0))

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[4(x₁)]	=	1 · x₁ + 0
[2(x₁)]	=	1 · x₁ + 0
[Begin(x₁)]	=	1 · x₁ + 13
[Wait(x₁)]	=	1 · x₁ + 10
[3(x₁)]	=	1 · x₁ + 0
[1(x₁)]	=	1 · x₁ + 2
[End(x₁)]	=	1 · x₁ + 2
[A3(x₁)]	=	1 · x₁ + 0
[A1(x₁)]	=	1 · x₁ + 2
[A2(x₁)]	=	1 · x₁ + 0
[Left(x₁)]	=	1 · x₁ + 3
[A4(x₁)]	=	1 · x₁ + 0
[Right3(x₁)]	=	1 · x₁ + 3
[Right1(x₁)]	=	13 · x₁ + 0

the rules

Begin(4(x0))	→	Wait(Right3(x0))
Right3(2(End(x0)))	→	Left(3(2(End(x0))))
Right1(2(x0))	→	A2(Right1(x0))
Right3(2(x0))	→	A2(Right3(x0))
Right3(1(x0))	→	A1(Right3(x0))
Right1(4(x0))	→	A4(Right1(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right1(3(x0))	→	A3(Right1(x0))
Right3(3(x0))	→	A3(Right3(x0))
A2(Left(x0))	→	Left(2(x0))
A1(Left(x0))	→	Left(1(x0))
A4(Left(x0))	→	Left(4(x0))
A3(Left(x0))	→	Left(3(x0))
Wait(Left(x0))	→	Begin(x0)
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(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

4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right1(x0))	→	Right1(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
1(Right3(x0))	→	Right3(A1(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right1(x0))	→	Right1(A3(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[4(x₁)]	=	4 · x₁ + 0
[2(x₁)]	=	4 · x₁ + 0
[Begin(x₁)]	=	1 · x₁ + 0
[Wait(x₁)]	=	1 · x₁ + 0
[3(x₁)]	=	4 · x₁ + 0
[1(x₁)]	=	1 · x₁ + 0
[End(x₁)]	=	1 · x₁ + 9
[A3(x₁)]	=	4 · x₁ + 0
[A1(x₁)]	=	1 · x₁ + 0
[A2(x₁)]	=	4 · x₁ + 0
[Left(x₁)]	=	1 · x₁ + 0
[A4(x₁)]	=	4 · x₁ + 0
[Right3(x₁)]	=	4 · x₁ + 0
[Right1(x₁)]	=	1 · x₁ + 4

the rules

4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right3(x0))	→	Right3(A2(x0))
1(Right3(x0))	→	Right3(A1(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(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

Begin(4(x0))	→	Wait(Right3(x0))
Right3(2(End(x0)))	→	Left(3(2(End(x0))))
Right3(2(x0))	→	A2(Right3(x0))
Right3(1(x0))	→	A1(Right3(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right3(3(x0))	→	A3(Right3(x0))
A2(Left(x0))	→	Left(2(x0))
A1(Left(x0))	→	Left(1(x0))
A4(Left(x0))	→	Left(4(x0))
A3(Left(x0))	→	Left(3(x0))
Wait(Left(x0))	→	Begin(x0)
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(x0))

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

[4(x₁)]	=	4 · x₁ + 0
[2(x₁)]	=	4 · x₁ + 0
[Begin(x₁)]	=	4 · x₁ + 2
[Wait(x₁)]	=	4 · x₁ + 2
[3(x₁)]	=	4 · x₁ + 0
[1(x₁)]	=	1 · x₁ + 6
[End(x₁)]	=	1 · x₁ + 0
[A3(x₁)]	=	4 · x₁ + 0
[A1(x₁)]	=	1 · x₁ + 8
[A2(x₁)]	=	4 · x₁ + 0
[Left(x₁)]	=	1 · x₁ + 0
[A4(x₁)]	=	4 · x₁ + 0
[Right3(x₁)]	=	4 · x₁ + 0

the rules

Begin(4(x0))	→	Wait(Right3(x0))
Right3(2(End(x0)))	→	Left(3(2(End(x0))))
Right3(2(x0))	→	A2(Right3(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right3(3(x0))	→	A3(Right3(x0))
A2(Left(x0))	→	Left(2(x0))
A4(Left(x0))	→	Left(4(x0))
A3(Left(x0))	→	Left(3(x0))
Wait(Left(x0))	→	Begin(x0)
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(x0))

remain.

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

4(Begin(x0))	→	Right3(Wait(x0))
End(2(Right3(x0)))	→	End(2(3(Left(x0))))
2(Right3(x0))	→	Right3(A2(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

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

[4(x₁)]

1	0	0
1	0	1
1	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[2(x₁)]

1	0	0
0	1	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Begin(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[Wait(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[3(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[1(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[End(x₁)]

1	0	1
0	0	0
1	1	1

· x₁ +

1	0	0
1	0	0
0	0	0

[A3(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[A2(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Left(x₁)]

1	0	0
0	1	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[A4(x₁)]

1	0	0
1	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right3(x₁)]

1	0	0
0	1	0
0	1	0

· x₁ +

0	0	0
1	0	0
1	0	0

the rules

4(Begin(x0))	→	Right3(Wait(x0))
2(Right3(x0))	→	Right3(A2(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
Left(Wait(x0))	→	Begin(x0)
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

remain.

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

[4(x₁)]	=	0 · x₁ + -∞
[2(x₁)]	=	0 · x₁ + -∞
[Begin(x₁)]	=	6 · x₁ + -∞
[Wait(x₁)]	=	6 · x₁ + -∞
[3(x₁)]	=	0 · x₁ + -∞
[1(x₁)]	=	1 · x₁ + -∞
[A3(x₁)]	=	0 · x₁ + -∞
[A2(x₁)]	=	0 · x₁ + -∞
[Left(x₁)]	=	1 · x₁ + -∞
[A4(x₁)]	=	0 · x₁ + -∞
[Right3(x₁)]	=	0 · x₁ + -∞

the rules

4(Begin(x0))	→	Right3(Wait(x0))
2(Right3(x0))	→	Right3(A2(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(x0))

remain.

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

[4(x₁)]	=	0 · x₁ + -∞
[2(x₁)]	=	0 · x₁ + -∞
[Begin(x₁)]	=	3 · x₁ + -∞
[Wait(x₁)]	=	0 · x₁ + -∞
[3(x₁)]	=	0 · x₁ + -∞
[1(x₁)]	=	0 · x₁ + -∞
[A3(x₁)]	=	0 · x₁ + -∞
[A2(x₁)]	=	0 · x₁ + -∞
[Left(x₁)]	=	8 · x₁ + -∞
[A4(x₁)]	=	0 · x₁ + -∞
[Right3(x₁)]	=	1 · x₁ + -∞

the rules

2(Right3(x0))	→	Right3(A2(x0))
4(Right3(x0))	→	Right3(A4(x0))
3(Right3(x0))	→	Right3(A3(x0))
Left(A2(x0))	→	2(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A3(x0))	→	3(Left(x0))
1(2(x0))	→	1(4(x0))
4(3(x0))	→	2(4(x0))
4(2(x0))	→	2(3(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

Right3(2(x0))	→	A2(Right3(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right3(3(x0))	→	A3(Right3(x0))
A2(Left(x0))	→	Left(2(x0))
A4(Left(x0))	→	Left(4(x0))
A3(Left(x0))	→	Left(3(x0))
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(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

[4(x₁)]	=	2 · x₁ + 0
[2(x₁)]	=	2 · x₁ + 0
[3(x₁)]	=	2 · x₁ + 0
[1(x₁)]	=	1 · x₁ + 0
[A3(x₁)]	=	2 · x₁ + 0
[A2(x₁)]	=	2 · x₁ + 0
[Left(x₁)]	=	1 · x₁ + 8
[A4(x₁)]	=	2 · x₁ + 0
[Right3(x₁)]	=	8 · x₁ + 0

the rules

Right3(2(x0))	→	A2(Right3(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right3(3(x0))	→	A3(Right3(x0))
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(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 (2 x 2)-matrices with strict dimension 1 over the arctic semiring over the integers

[4(x₁)]

2	1
3	0

· x₁ +

-∞	-∞
-∞	-∞

[2(x₁)]

2	-∞
3	-∞

· x₁ +

-∞	-∞
-∞	-∞

[3(x₁)]

0	1
3	0

· x₁ +

-∞	-∞
-∞	-∞

[1(x₁)]

0	-∞
1	-∞

· x₁ +

-∞	-∞
-∞	-∞

[A3(x₁)]

0	1
0	-∞

· x₁ +

-∞	-∞
-∞	-∞

[A2(x₁)]

2	-∞
-∞	-∞

· x₁ +

-∞	-∞
-∞	-∞

[A4(x₁)]

1	1
-∞	-∞

· x₁ +

-∞	-∞
-∞	-∞

[Right3(x₁)]

2	-∞
1	0

· x₁ +

-∞	-∞
-∞	-∞

the rules

Right3(2(x0))	→	A2(Right3(x0))
Right3(3(x0))	→	A3(Right3(x0))
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(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 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[4(x₁)]	=	1 · x₁ + -∞
[2(x₁)]	=	1 · x₁ + -∞
[3(x₁)]	=	1 · x₁ + -∞
[1(x₁)]	=	0 · x₁ + -∞
[A3(x₁)]	=	1 · x₁ + -∞
[A2(x₁)]	=	0 · x₁ + -∞
[Right3(x₁)]	=	0 · x₁ + -∞

the rules

Right3(3(x0))	→	A3(Right3(x0))
2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(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 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[4(x₁)]	=	1 · x₁ + -∞
[2(x₁)]	=	1 · x₁ + -∞
[3(x₁)]	=	1 · x₁ + -∞
[1(x₁)]	=	0 · x₁ + -∞
[A3(x₁)]	=	0 · x₁ + -∞
[Right3(x₁)]	=	0 · x₁ + -∞

the rules

2(1(x0))	→	4(1(x0))
3(4(x0))	→	4(2(x0))
2(4(x0))	→	3(2(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 Knuth Bendix order with w0 = 1 and the following precedence and weight function

prec(3)	=	1	weight(3)	=	1
prec(2)	=	3	weight(2)	=	1
prec(4)	=	0	weight(4)	=	1
prec(1)	=	0	weight(1)	=	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 R is empty

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