YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(a(a(a(b(b(x0))))))	→	Wait(Right1(x0))
Begin(a(a(b(b(x0)))))	→	Wait(Right2(x0))
Begin(a(b(b(x0))))	→	Wait(Right3(x0))
Begin(b(b(x0)))	→	Wait(Right4(x0))
Begin(b(x0))	→	Wait(Right5(x0))
Right1(b(End(x0)))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right3(b(a(a(End(x0)))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right4(b(a(a(a(End(x0))))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right5(b(a(a(a(b(End(x0)))))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

Proof

1 Rule Removal

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

[Wait(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right5(x₁)]

1	0	0
1	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Right1(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right2(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[Left(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[b(x₁)]

1	0	1
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right4(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Aa(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ab(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[End(x₁)]

1	0	1
0	1	1
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[Right3(x₁)]

1	0	0
1	0	0
0	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

the rules

Begin(a(a(a(b(b(x0))))))	→	Wait(Right1(x0))
Begin(a(a(b(b(x0)))))	→	Wait(Right2(x0))
Begin(a(b(b(x0))))	→	Wait(Right3(x0))
Begin(b(b(x0)))	→	Wait(Right4(x0))
Begin(b(x0))	→	Wait(Right5(x0))
Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right3(b(a(a(End(x0)))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right4(b(a(a(a(End(x0))))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

remain.

1.1 Rule Removal

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

[Wait(x₁)]	=	0 · x₁ + -∞
[Right5(x₁)]	=	5 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	8 · x₁ + -∞
[Right2(x₁)]	=	8 · x₁ + -∞
[Left(x₁)]	=	6 · x₁ + -∞
[b(x₁)]	=	1 · x₁ + -∞
[Right4(x₁)]	=	8 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	1 · x₁ + -∞
[End(x₁)]	=	6 · x₁ + -∞
[Right3(x₁)]	=	8 · x₁ + -∞
[Begin(x₁)]	=	6 · x₁ + -∞

the rules

Begin(a(a(a(b(b(x0))))))	→	Wait(Right1(x0))
Begin(a(a(b(b(x0)))))	→	Wait(Right2(x0))
Begin(a(b(b(x0))))	→	Wait(Right3(x0))
Begin(b(b(x0)))	→	Wait(Right4(x0))
Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right3(b(a(a(End(x0)))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right4(b(a(a(a(End(x0))))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

remain.

1.1.1 Rule Removal

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

[Wait(x₁)]	=	0 · x₁ + -∞
[Right5(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	0 · x₁ + -∞
[Right2(x₁)]	=	1 · x₁ + -∞
[Left(x₁)]	=	1 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[Right4(x₁)]	=	1 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	0 · x₁ + -∞
[Right3(x₁)]	=	1 · x₁ + -∞
[Begin(x₁)]	=	1 · x₁ + -∞

the rules

Begin(a(a(b(b(x0)))))	→	Wait(Right2(x0))
Begin(a(b(b(x0))))	→	Wait(Right3(x0))
Begin(b(b(x0)))	→	Wait(Right4(x0))
Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right3(b(a(a(End(x0)))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right4(b(a(a(a(End(x0))))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

remain.

1.1.1.1 String Reversal

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

b(b(a(a(Begin(x0)))))	→	Right2(Wait(x0))
b(b(a(Begin(x0))))	→	Right3(Wait(x0))
b(b(Begin(x0)))	→	Right4(Wait(x0))
End(a(b(Right2(x0))))	→	End(a(b(b(a(a(b(a(Left(x0)))))))))
End(a(a(b(Right3(x0)))))	→	End(a(b(b(a(a(b(a(Left(x0)))))))))
End(a(a(a(b(Right4(x0))))))	→	End(a(b(b(a(a(b(a(Left(x0)))))))))
b(Right1(x0))	→	Right1(Ab(x0))
b(Right2(x0))	→	Right2(Ab(x0))
b(Right3(x0))	→	Right3(Ab(x0))
b(Right4(x0))	→	Right4(Ab(x0))
b(Right5(x0))	→	Right5(Ab(x0))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
a(Right4(x0))	→	Right4(Aa(x0))
a(Right5(x0))	→	Right5(Aa(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Wait(x0))	→	Begin(x0)
b(b(a(a(a(b(x0))))))	→	a(b(b(a(a(b(a(x0)))))))

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[Wait(x₁)]	=	4 · x₁ + 0
[Right5(x₁)]	=	1 · x₁ + 0
[a(x₁)]	=	1 · x₁ + 0
[Right1(x₁)]	=	6 · x₁ + 8
[Right2(x₁)]	=	4 · x₁ + 0
[Left(x₁)]	=	1 · x₁ + 0
[b(x₁)]	=	2 · x₁ + 0
[Right4(x₁)]	=	4 · x₁ + 0
[Aa(x₁)]	=	1 · x₁ + 0
[Ab(x₁)]	=	2 · x₁ + 0
[End(x₁)]	=	2 · x₁ + 0
[Right3(x₁)]	=	4 · x₁ + 0
[Begin(x₁)]	=	4 · x₁ + 0

the rules

b(b(a(a(Begin(x0)))))	→	Right2(Wait(x0))
b(b(a(Begin(x0))))	→	Right3(Wait(x0))
b(b(Begin(x0)))	→	Right4(Wait(x0))
End(a(b(Right2(x0))))	→	End(a(b(b(a(a(b(a(Left(x0)))))))))
End(a(a(b(Right3(x0)))))	→	End(a(b(b(a(a(b(a(Left(x0)))))))))
End(a(a(a(b(Right4(x0))))))	→	End(a(b(b(a(a(b(a(Left(x0)))))))))
b(Right2(x0))	→	Right2(Ab(x0))
b(Right3(x0))	→	Right3(Ab(x0))
b(Right4(x0))	→	Right4(Ab(x0))
b(Right5(x0))	→	Right5(Ab(x0))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
a(Right4(x0))	→	Right4(Aa(x0))
a(Right5(x0))	→	Right5(Aa(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Wait(x0))	→	Begin(x0)
b(b(a(a(a(b(x0))))))	→	a(b(b(a(a(b(a(x0)))))))

remain.

1.1.1.1.1.1 String Reversal

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

Begin(a(a(b(b(x0)))))	→	Wait(Right2(x0))
Begin(a(b(b(x0))))	→	Wait(Right3(x0))
Begin(b(b(x0)))	→	Wait(Right4(x0))
Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right3(b(a(a(End(x0)))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right4(b(a(a(a(End(x0))))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[Wait(x₁)]	=	4 · x₁ + 0
[Right5(x₁)]	=	4 · x₁ + 2
[a(x₁)]	=	1 · x₁ + 0
[Right1(x₁)]	=	1 · x₁ + 0
[Right2(x₁)]	=	4 · x₁ + 3
[Left(x₁)]	=	1 · x₁ + 0
[b(x₁)]	=	2 · x₁ + 1
[Right4(x₁)]	=	4 · x₁ + 3
[Aa(x₁)]	=	1 · x₁ + 0
[Ab(x₁)]	=	2 · x₁ + 1
[End(x₁)]	=	1 · x₁ + 1
[Right3(x₁)]	=	4 · x₁ + 3
[Begin(x₁)]	=	4 · x₁ + 0

the rules

Begin(a(a(b(b(x0)))))	→	Wait(Right2(x0))
Begin(a(b(b(x0))))	→	Wait(Right3(x0))
Begin(b(b(x0)))	→	Wait(Right4(x0))
Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right3(b(a(a(End(x0)))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right4(b(a(a(a(End(x0))))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

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

[Wait(x₁)]

1	1	0
0	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right5(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
1	0	0

[a(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Right1(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[Right2(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

1	0	0
0	0	0
0	0	0

[Left(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[b(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
1	0	0

[Right4(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Aa(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ab(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
1	0	0
0	0	0

[End(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right3(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Begin(x₁)]

1	0	1
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

the rules

Begin(a(a(b(b(x0)))))	→	Wait(Right2(x0))
Right3(b(a(a(End(x0)))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right4(b(a(a(a(End(x0))))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

remain.

1.1.1.1.1.1.1.1.1 Rule Removal

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

[Wait(x₁)]	=	0 · x₁ + -∞
[Right5(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	12 · x₁ + -∞
[Right2(x₁)]	=	10 · x₁ + -∞
[Left(x₁)]	=	10 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[Right4(x₁)]	=	10 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	6 · x₁ + -∞
[Right3(x₁)]	=	14 · x₁ + -∞
[Begin(x₁)]	=	10 · x₁ + -∞

the rules

Begin(a(a(b(b(x0)))))	→	Wait(Right2(x0))
Right4(b(a(a(a(End(x0))))))	→	Left(a(b(a(a(b(b(a(End(x0)))))))))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

remain.

1.1.1.1.1.1.1.1.1.1 Rule Removal

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

[Wait(x₁)]	=	0 · x₁ + -∞
[Right5(x₁)]	=	4 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	7 · x₁ + -∞
[Right2(x₁)]	=	0 · x₁ + -∞
[Left(x₁)]	=	0 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[Right4(x₁)]	=	4 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	0 · x₁ + -∞
[Right3(x₁)]	=	0 · x₁ + -∞
[Begin(x₁)]	=	0 · x₁ + -∞

the rules

Begin(a(a(b(b(x0)))))	→	Wait(Right2(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

remain.

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

[Wait(x₁)]	=	0 · x₁ + -∞
[Right5(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	0 · x₁ + -∞
[Right2(x₁)]	=	0 · x₁ + -∞
[Left(x₁)]	=	11 · x₁ + -∞
[b(x₁)]	=	1 · x₁ + -∞
[Right4(x₁)]	=	11 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	1 · x₁ + -∞
[Right3(x₁)]	=	4 · x₁ + -∞
[Begin(x₁)]	=	8 · x₁ + -∞

the rules

Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
b(a(a(a(b(b(x0))))))	→	a(b(a(a(b(b(a(x0)))))))

remain.

1.1.1.1.1.1.1.1.1.1.1.1 Bounds

The given TRS is match-bounded by 0. This is shown by the following automaton.

final states:

{19, 17, 15, 13, 12, 11, 10, 8, 6, 4, 1}

transitions:

10 → 3

1 → 3

8 → 9

13 → 14

6 → 7

11 → 5

4 → 5

12 → 7

19 → 20

19 → 16

b₀(18) → 20

b₀(2) → 16

b₀(23) → 24

b₀(20) → 21

Left₀(16) → 15

Left₀(18) → 17

Right3₀(2) → 5

Aa₀(7) → 12

Aa₀(14) → 13

Aa₀(9) → 8

Aa₀(5) → 11

Aa₀(3) → 10

Right4₀(2) → 7

f13₀ → 2

Ab₀(7) → 6

Ab₀(3) → 1

Ab₀(5) → 4

Right2₀(2) → 3

a₀(2) → 18

a₀(21) → 22

a₀(24) → 19

a₀(22) → 23

Right5₀(2) → 14

Right1₀(2) → 9

10	→	3
1	→	3
8	→	9
13	→	14
6	→	7
11	→	5
4	→	5
12	→	7
19	→	20
19	→	16
b₀(18)	→	20
b₀(2)	→	16
b₀(23)	→	24
b₀(20)	→	21
Left₀(16)	→	15
Left₀(18)	→	17
Right3₀(2)	→	5
Aa₀(7)	→	12
Aa₀(14)	→	13
Aa₀(9)	→	8
Aa₀(5)	→	11
Aa₀(3)	→	10
Right4₀(2)	→	7
f13₀	→	2
Ab₀(7)	→	6
Ab₀(3)	→	1
Ab₀(5)	→	4
Right2₀(2)	→	3
a₀(2)	→	18
a₀(21)	→	22
a₀(24)	→	19
a₀(22)	→	23
Right5₀(2)	→	14
Right1₀(2)	→	9