YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(5(4(5(x0))))	→	Wait(Right1(x0))
Begin(4(5(x0)))	→	Wait(Right2(x0))
Begin(5(x0))	→	Wait(Right3(x0))
Begin(5(5(5(5(5(4(4(4(4(4(4(x0))))))))))))	→	Wait(Right4(x0))
Begin(5(5(5(5(4(4(4(4(4(4(x0)))))))))))	→	Wait(Right5(x0))
Begin(5(5(5(4(4(4(4(4(4(x0))))))))))	→	Wait(Right6(x0))
Begin(5(5(4(4(4(4(4(4(x0)))))))))	→	Wait(Right7(x0))
Begin(5(4(4(4(4(4(4(x0))))))))	→	Wait(Right8(x0))
Begin(4(4(4(4(4(4(x0)))))))	→	Wait(Right9(x0))
Begin(4(4(4(4(4(x0))))))	→	Wait(Right10(x0))
Begin(4(4(4(4(x0)))))	→	Wait(Right11(x0))
Begin(4(4(4(x0))))	→	Wait(Right12(x0))
Begin(4(4(x0)))	→	Wait(Right13(x0))
Begin(4(x0))	→	Wait(Right14(x0))
Right1(4(End(x0)))	→	Left(4(4(5(5(End(x0))))))
Right2(4(5(End(x0))))	→	Left(4(4(5(5(End(x0))))))
Right3(4(5(4(End(x0)))))	→	Left(4(4(5(5(End(x0))))))
Right4(5(End(x0)))	→	Left(2(End(x0)))
Right5(5(5(End(x0))))	→	Left(2(End(x0)))
Right6(5(5(5(End(x0)))))	→	Left(2(End(x0)))
Right7(5(5(5(5(End(x0))))))	→	Left(2(End(x0)))
Right8(5(5(5(5(5(End(x0)))))))	→	Left(2(End(x0)))
Right9(5(5(5(5(5(5(End(x0))))))))	→	Left(2(End(x0)))
Right10(5(5(5(5(5(5(4(End(x0)))))))))	→	Left(2(End(x0)))
Right11(5(5(5(5(5(5(4(4(End(x0))))))))))	→	Left(2(End(x0)))
Right12(5(5(5(5(5(5(4(4(4(End(x0)))))))))))	→	Left(2(End(x0)))
Right13(5(5(5(5(5(5(4(4(4(4(End(x0))))))))))))	→	Left(2(End(x0)))
Right14(5(5(5(5(5(5(4(4(4(4(4(End(x0)))))))))))))	→	Left(2(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))
Right6(0(x0))	→	A0(Right6(x0))
Right7(0(x0))	→	A0(Right7(x0))
Right8(0(x0))	→	A0(Right8(x0))
Right9(0(x0))	→	A0(Right9(x0))
Right10(0(x0))	→	A0(Right10(x0))
Right11(0(x0))	→	A0(Right11(x0))
Right12(0(x0))	→	A0(Right12(x0))
Right13(0(x0))	→	A0(Right13(x0))
Right14(0(x0))	→	A0(Right14(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))
Right6(1(x0))	→	A1(Right6(x0))
Right7(1(x0))	→	A1(Right7(x0))
Right8(1(x0))	→	A1(Right8(x0))
Right9(1(x0))	→	A1(Right9(x0))
Right10(1(x0))	→	A1(Right10(x0))
Right11(1(x0))	→	A1(Right11(x0))
Right12(1(x0))	→	A1(Right12(x0))
Right13(1(x0))	→	A1(Right13(x0))
Right14(1(x0))	→	A1(Right14(x0))
Right1(4(x0))	→	A4(Right1(x0))
Right2(4(x0))	→	A4(Right2(x0))
Right3(4(x0))	→	A4(Right3(x0))
Right4(4(x0))	→	A4(Right4(x0))
Right5(4(x0))	→	A4(Right5(x0))
Right6(4(x0))	→	A4(Right6(x0))
Right7(4(x0))	→	A4(Right7(x0))
Right8(4(x0))	→	A4(Right8(x0))
Right9(4(x0))	→	A4(Right9(x0))
Right10(4(x0))	→	A4(Right10(x0))
Right11(4(x0))	→	A4(Right11(x0))
Right12(4(x0))	→	A4(Right12(x0))
Right13(4(x0))	→	A4(Right13(x0))
Right14(4(x0))	→	A4(Right14(x0))
Right1(5(x0))	→	A5(Right1(x0))
Right2(5(x0))	→	A5(Right2(x0))
Right3(5(x0))	→	A5(Right3(x0))
Right4(5(x0))	→	A5(Right4(x0))
Right5(5(x0))	→	A5(Right5(x0))
Right6(5(x0))	→	A5(Right6(x0))
Right7(5(x0))	→	A5(Right7(x0))
Right8(5(x0))	→	A5(Right8(x0))
Right9(5(x0))	→	A5(Right9(x0))
Right10(5(x0))	→	A5(Right10(x0))
Right11(5(x0))	→	A5(Right11(x0))
Right12(5(x0))	→	A5(Right12(x0))
Right13(5(x0))	→	A5(Right13(x0))
Right14(5(x0))	→	A5(Right14(x0))
Right1(2(x0))	→	A2(Right1(x0))
Right2(2(x0))	→	A2(Right2(x0))
Right3(2(x0))	→	A2(Right3(x0))
Right4(2(x0))	→	A2(Right4(x0))
Right5(2(x0))	→	A2(Right5(x0))
Right6(2(x0))	→	A2(Right6(x0))
Right7(2(x0))	→	A2(Right7(x0))
Right8(2(x0))	→	A2(Right8(x0))
Right9(2(x0))	→	A2(Right9(x0))
Right10(2(x0))	→	A2(Right10(x0))
Right11(2(x0))	→	A2(Right11(x0))
Right12(2(x0))	→	A2(Right12(x0))
Right13(2(x0))	→	A2(Right13(x0))
Right14(2(x0))	→	A2(Right14(x0))
A0(Left(x0))	→	Left(0(x0))
A1(Left(x0))	→	Left(1(x0))
A4(Left(x0))	→	Left(4(x0))
A5(Left(x0))	→	Left(5(x0))
A2(Left(x0))	→	Left(2(x0))
Wait(Left(x0))	→	Begin(x0)
0(x0)	→	1(x0)
4(5(4(5(x0))))	→	4(4(5(5(x0))))
5(5(5(5(5(5(4(4(4(4(4(4(x0))))))))))))	→	2(x0)

Proof

1 String Reversal

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

5(4(5(Begin(x0))))	→	Right1(Wait(x0))
5(4(Begin(x0)))	→	Right2(Wait(x0))
5(Begin(x0))	→	Right3(Wait(x0))
4(4(4(4(4(4(5(5(5(5(5(Begin(x0))))))))))))	→	Right4(Wait(x0))
4(4(4(4(4(4(5(5(5(5(Begin(x0)))))))))))	→	Right5(Wait(x0))
4(4(4(4(4(4(5(5(5(Begin(x0))))))))))	→	Right6(Wait(x0))
4(4(4(4(4(4(5(5(Begin(x0)))))))))	→	Right7(Wait(x0))
4(4(4(4(4(4(5(Begin(x0))))))))	→	Right8(Wait(x0))
4(4(4(4(4(4(Begin(x0)))))))	→	Right9(Wait(x0))
4(4(4(4(4(Begin(x0))))))	→	Right10(Wait(x0))
4(4(4(4(Begin(x0)))))	→	Right11(Wait(x0))
4(4(4(Begin(x0))))	→	Right12(Wait(x0))
4(4(Begin(x0)))	→	Right13(Wait(x0))
4(Begin(x0))	→	Right14(Wait(x0))
End(4(Right1(x0)))	→	End(5(5(4(4(Left(x0))))))
End(5(4(Right2(x0))))	→	End(5(5(4(4(Left(x0))))))
End(4(5(4(Right3(x0)))))	→	End(5(5(4(4(Left(x0))))))
End(5(Right4(x0)))	→	End(2(Left(x0)))
End(5(5(Right5(x0))))	→	End(2(Left(x0)))
End(5(5(5(Right6(x0)))))	→	End(2(Left(x0)))
End(5(5(5(5(Right7(x0))))))	→	End(2(Left(x0)))
End(5(5(5(5(5(Right8(x0)))))))	→	End(2(Left(x0)))
End(5(5(5(5(5(5(Right9(x0))))))))	→	End(2(Left(x0)))
End(4(5(5(5(5(5(5(Right10(x0)))))))))	→	End(2(Left(x0)))
End(4(4(5(5(5(5(5(5(Right11(x0))))))))))	→	End(2(Left(x0)))
End(4(4(4(5(5(5(5(5(5(Right12(x0)))))))))))	→	End(2(Left(x0)))
End(4(4(4(4(5(5(5(5(5(5(Right13(x0))))))))))))	→	End(2(Left(x0)))
End(4(4(4(4(4(5(5(5(5(5(5(Right14(x0)))))))))))))	→	End(2(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))
0(Right6(x0))	→	Right6(A0(x0))
0(Right7(x0))	→	Right7(A0(x0))
0(Right8(x0))	→	Right8(A0(x0))
0(Right9(x0))	→	Right9(A0(x0))
0(Right10(x0))	→	Right10(A0(x0))
0(Right11(x0))	→	Right11(A0(x0))
0(Right12(x0))	→	Right12(A0(x0))
0(Right13(x0))	→	Right13(A0(x0))
0(Right14(x0))	→	Right14(A0(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))
1(Right6(x0))	→	Right6(A1(x0))
1(Right7(x0))	→	Right7(A1(x0))
1(Right8(x0))	→	Right8(A1(x0))
1(Right9(x0))	→	Right9(A1(x0))
1(Right10(x0))	→	Right10(A1(x0))
1(Right11(x0))	→	Right11(A1(x0))
1(Right12(x0))	→	Right12(A1(x0))
1(Right13(x0))	→	Right13(A1(x0))
1(Right14(x0))	→	Right14(A1(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right2(x0))	→	Right2(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
4(Right4(x0))	→	Right4(A4(x0))
4(Right5(x0))	→	Right5(A4(x0))
4(Right6(x0))	→	Right6(A4(x0))
4(Right7(x0))	→	Right7(A4(x0))
4(Right8(x0))	→	Right8(A4(x0))
4(Right9(x0))	→	Right9(A4(x0))
4(Right10(x0))	→	Right10(A4(x0))
4(Right11(x0))	→	Right11(A4(x0))
4(Right12(x0))	→	Right12(A4(x0))
4(Right13(x0))	→	Right13(A4(x0))
4(Right14(x0))	→	Right14(A4(x0))
5(Right1(x0))	→	Right1(A5(x0))
5(Right2(x0))	→	Right2(A5(x0))
5(Right3(x0))	→	Right3(A5(x0))
5(Right4(x0))	→	Right4(A5(x0))
5(Right5(x0))	→	Right5(A5(x0))
5(Right6(x0))	→	Right6(A5(x0))
5(Right7(x0))	→	Right7(A5(x0))
5(Right8(x0))	→	Right8(A5(x0))
5(Right9(x0))	→	Right9(A5(x0))
5(Right10(x0))	→	Right10(A5(x0))
5(Right11(x0))	→	Right11(A5(x0))
5(Right12(x0))	→	Right12(A5(x0))
5(Right13(x0))	→	Right13(A5(x0))
5(Right14(x0))	→	Right14(A5(x0))
2(Right1(x0))	→	Right1(A2(x0))
2(Right2(x0))	→	Right2(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
2(Right4(x0))	→	Right4(A2(x0))
2(Right5(x0))	→	Right5(A2(x0))
2(Right6(x0))	→	Right6(A2(x0))
2(Right7(x0))	→	Right7(A2(x0))
2(Right8(x0))	→	Right8(A2(x0))
2(Right9(x0))	→	Right9(A2(x0))
2(Right10(x0))	→	Right10(A2(x0))
2(Right11(x0))	→	Right11(A2(x0))
2(Right12(x0))	→	Right12(A2(x0))
2(Right13(x0))	→	Right13(A2(x0))
2(Right14(x0))	→	Right14(A2(x0))
Left(A0(x0))	→	0(Left(x0))
Left(A1(x0))	→	1(Left(x0))
Left(A4(x0))	→	4(Left(x0))
Left(A5(x0))	→	5(Left(x0))
Left(A2(x0))	→	2(Left(x0))
Left(Wait(x0))	→	Begin(x0)
0(x0)	→	1(x0)
5(4(5(4(x0))))	→	5(5(4(4(x0))))
4(4(4(4(4(4(5(5(5(5(5(5(x0))))))))))))	→	2(x0)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

End^#(4(Right1(x0)))	→	Left^#(x0)
End^#(4(Right1(x0)))	→	4^#(Left(x0))
End^#(4(Right1(x0)))	→	4^#(4(Left(x0)))
End^#(4(Right1(x0)))	→	5^#(4(4(Left(x0))))
End^#(4(Right1(x0)))	→	5^#(5(4(4(Left(x0)))))
End^#(4(Right1(x0)))	→	End^#(5(5(4(4(Left(x0))))))
End^#(5(4(Right2(x0))))	→	Left^#(x0)
End^#(5(4(Right2(x0))))	→	4^#(Left(x0))
End^#(5(4(Right2(x0))))	→	4^#(4(Left(x0)))
End^#(5(4(Right2(x0))))	→	5^#(4(4(Left(x0))))
End^#(5(4(Right2(x0))))	→	5^#(5(4(4(Left(x0)))))
End^#(5(4(Right2(x0))))	→	End^#(5(5(4(4(Left(x0))))))
End^#(4(5(4(Right3(x0)))))	→	Left^#(x0)
End^#(4(5(4(Right3(x0)))))	→	4^#(Left(x0))
End^#(4(5(4(Right3(x0)))))	→	4^#(4(Left(x0)))
End^#(4(5(4(Right3(x0)))))	→	5^#(4(4(Left(x0))))
End^#(4(5(4(Right3(x0)))))	→	5^#(5(4(4(Left(x0)))))
End^#(4(5(4(Right3(x0)))))	→	End^#(5(5(4(4(Left(x0))))))
End^#(5(Right4(x0)))	→	Left^#(x0)
End^#(5(Right4(x0)))	→	2^#(Left(x0))
End^#(5(Right4(x0)))	→	End^#(2(Left(x0)))
End^#(5(5(Right5(x0))))	→	Left^#(x0)
End^#(5(5(Right5(x0))))	→	2^#(Left(x0))
End^#(5(5(Right5(x0))))	→	End^#(2(Left(x0)))
End^#(5(5(5(Right6(x0)))))	→	Left^#(x0)
End^#(5(5(5(Right6(x0)))))	→	2^#(Left(x0))
End^#(5(5(5(Right6(x0)))))	→	End^#(2(Left(x0)))
End^#(5(5(5(5(Right7(x0))))))	→	Left^#(x0)
End^#(5(5(5(5(Right7(x0))))))	→	2^#(Left(x0))
End^#(5(5(5(5(Right7(x0))))))	→	End^#(2(Left(x0)))
End^#(5(5(5(5(5(Right8(x0)))))))	→	Left^#(x0)
End^#(5(5(5(5(5(Right8(x0)))))))	→	2^#(Left(x0))
End^#(5(5(5(5(5(Right8(x0)))))))	→	End^#(2(Left(x0)))
End^#(5(5(5(5(5(5(Right9(x0))))))))	→	Left^#(x0)
End^#(5(5(5(5(5(5(Right9(x0))))))))	→	2^#(Left(x0))
End^#(5(5(5(5(5(5(Right9(x0))))))))	→	End^#(2(Left(x0)))
End^#(4(5(5(5(5(5(5(Right10(x0)))))))))	→	Left^#(x0)
End^#(4(5(5(5(5(5(5(Right10(x0)))))))))	→	2^#(Left(x0))
End^#(4(5(5(5(5(5(5(Right10(x0)))))))))	→	End^#(2(Left(x0)))
End^#(4(4(5(5(5(5(5(5(Right11(x0))))))))))	→	Left^#(x0)
End^#(4(4(5(5(5(5(5(5(Right11(x0))))))))))	→	2^#(Left(x0))
End^#(4(4(5(5(5(5(5(5(Right11(x0))))))))))	→	End^#(2(Left(x0)))
End^#(4(4(4(5(5(5(5(5(5(Right12(x0)))))))))))	→	Left^#(x0)
End^#(4(4(4(5(5(5(5(5(5(Right12(x0)))))))))))	→	2^#(Left(x0))
End^#(4(4(4(5(5(5(5(5(5(Right12(x0)))))))))))	→	End^#(2(Left(x0)))
End^#(4(4(4(4(5(5(5(5(5(5(Right13(x0))))))))))))	→	Left^#(x0)
End^#(4(4(4(4(5(5(5(5(5(5(Right13(x0))))))))))))	→	2^#(Left(x0))
End^#(4(4(4(4(5(5(5(5(5(5(Right13(x0))))))))))))	→	End^#(2(Left(x0)))
End^#(4(4(4(4(4(5(5(5(5(5(5(Right14(x0)))))))))))))	→	Left^#(x0)
End^#(4(4(4(4(4(5(5(5(5(5(5(Right14(x0)))))))))))))	→	2^#(Left(x0))
End^#(4(4(4(4(4(5(5(5(5(5(5(Right14(x0)))))))))))))	→	End^#(2(Left(x0)))
Left^#(A0(x0))	→	Left^#(x0)
Left^#(A0(x0))	→	0^#(Left(x0))
Left^#(A1(x0))	→	Left^#(x0)
Left^#(A1(x0))	→	1^#(Left(x0))
Left^#(A4(x0))	→	Left^#(x0)
Left^#(A4(x0))	→	4^#(Left(x0))
Left^#(A5(x0))	→	Left^#(x0)
Left^#(A5(x0))	→	5^#(Left(x0))
Left^#(A2(x0))	→	Left^#(x0)
Left^#(A2(x0))	→	2^#(Left(x0))
0^#(x0)	→	1^#(x0)
5^#(4(5(4(x0))))	→	4^#(4(x0))
5^#(4(5(4(x0))))	→	5^#(4(4(x0)))
5^#(4(5(4(x0))))	→	5^#(5(4(4(x0))))
4^#(4(4(4(4(4(5(5(5(5(5(5(x0))))))))))))	→	2^#(x0)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pairs

End^#(4(Right1(x0)))	→	End^#(5(5(4(4(Left(x0))))))
End^#(5(4(Right2(x0))))	→	End^#(5(5(4(4(Left(x0))))))
End^#(4(5(4(Right3(x0)))))	→	End^#(5(5(4(4(Left(x0))))))
End^#(5(Right4(x0)))	→	End^#(2(Left(x0)))
End^#(5(5(Right5(x0))))	→	End^#(2(Left(x0)))
End^#(5(5(5(Right6(x0)))))	→	End^#(2(Left(x0)))
End^#(5(5(5(5(Right7(x0))))))	→	End^#(2(Left(x0)))
End^#(5(5(5(5(5(Right8(x0)))))))	→	End^#(2(Left(x0)))
End^#(5(5(5(5(5(5(Right9(x0))))))))	→	End^#(2(Left(x0)))
End^#(4(5(5(5(5(5(5(Right10(x0)))))))))	→	End^#(2(Left(x0)))
End^#(4(4(5(5(5(5(5(5(Right11(x0))))))))))	→	End^#(2(Left(x0)))
End^#(4(4(4(5(5(5(5(5(5(Right12(x0)))))))))))	→	End^#(2(Left(x0)))
End^#(4(4(4(4(5(5(5(5(5(5(Right13(x0))))))))))))	→	End^#(2(Left(x0)))
End^#(4(4(4(4(4(5(5(5(5(5(5(Right14(x0)))))))))))))	→	End^#(2(Left(x0)))

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight function

prec(End^#)	=	16	weight(End^#)	=	1
prec(A2)	=	0	weight(A2)	=	1
prec(A5)	=	0	weight(A5)	=	1
prec(A4)	=	16	weight(A4)	=	1
prec(A1)	=	0	weight(A1)	=	1
prec(1)	=	0	weight(1)	=	1
prec(A0)	=	0	weight(A0)	=	0
prec(0)	=	0	weight(0)	=	1
prec(2)	=	1	weight(2)	=	1
prec(Left)	=	16	weight(Left)	=	0
prec(Right14)	=	0	weight(Right14)	=	0
prec(Right13)	=	0	weight(Right13)	=	0
prec(Right12)	=	0	weight(Right12)	=	0
prec(Right11)	=	0	weight(Right11)	=	1
prec(Right10)	=	0	weight(Right10)	=	1
prec(Right9)	=	0	weight(Right9)	=	0
prec(Right8)	=	0	weight(Right8)	=	0
prec(Right7)	=	0	weight(Right7)	=	1
prec(Right6)	=	0	weight(Right6)	=	0
prec(Right5)	=	0	weight(Right5)	=	0
prec(Right4)	=	0	weight(Right4)	=	0
prec(Right3)	=	0	weight(Right3)	=	0
prec(Right2)	=	0	weight(Right2)	=	1
prec(Wait)	=	0	weight(Wait)	=	1
prec(Right1)	=	0	weight(Right1)	=	0
prec(Begin)	=	0	weight(Begin)	=	0
prec(4)	=	0	weight(4)	=	1
prec(5)	=	2	weight(5)	=	1

in combination with the following argument filter

π(End^#) = 1

π(A2) = []

π(A5) = []

π(A4) = []

π(A1) = []

π(1) = 1

π(A0) = 1

π(0) = 1

π(2) = []

π(Left) = 1

π(Right14) = 1

π(Right13) = 1

π(Right12) = 1

π(Right11) = []

π(Right10) = []

π(Right9) = 1

π(Right8) = 1

π(Right7) = []

π(Right6) = 1

π(Right5) = 1

π(Right4) = 1

π(Right3) = 1

π(Right2) = 1

π(Wait) = []

π(Right1) = 1

π(Begin) = 1

π(4) = [1]

π(5) = []

together with the usable rules

2(Right1(x0))	→	Right1(A2(x0))
2(Right2(x0))	→	Right2(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
2(Right4(x0))	→	Right4(A2(x0))
2(Right5(x0))	→	Right5(A2(x0))
2(Right6(x0))	→	Right6(A2(x0))
2(Right7(x0))	→	Right7(A2(x0))
2(Right8(x0))	→	Right8(A2(x0))
2(Right9(x0))	→	Right9(A2(x0))
2(Right10(x0))	→	Right10(A2(x0))
2(Right11(x0))	→	Right11(A2(x0))
2(Right12(x0))	→	Right12(A2(x0))
2(Right13(x0))	→	Right13(A2(x0))
2(Right14(x0))	→	Right14(A2(x0))
5(4(5(Begin(x0))))	→	Right1(Wait(x0))
5(4(Begin(x0)))	→	Right2(Wait(x0))
5(Begin(x0))	→	Right3(Wait(x0))
5(Right1(x0))	→	Right1(A5(x0))
5(Right2(x0))	→	Right2(A5(x0))
5(Right3(x0))	→	Right3(A5(x0))
5(Right4(x0))	→	Right4(A5(x0))
5(Right5(x0))	→	Right5(A5(x0))
5(Right6(x0))	→	Right6(A5(x0))
5(Right7(x0))	→	Right7(A5(x0))
5(Right8(x0))	→	Right8(A5(x0))
5(Right9(x0))	→	Right9(A5(x0))
5(Right10(x0))	→	Right10(A5(x0))
5(Right11(x0))	→	Right11(A5(x0))
5(Right12(x0))	→	Right12(A5(x0))
5(Right13(x0))	→	Right13(A5(x0))
5(Right14(x0))	→	Right14(A5(x0))
5(4(5(4(x0))))	→	5(5(4(4(x0))))

(w.r.t. the implicit argument filter of the reduction pair), the pair

End^#(5(4(Right2(x0))))

→

End^#(5(5(4(4(Left(x0))))))

remains.

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pairs

Left^#(A2(x0))	→	Left^#(x0)
Left^#(A0(x0))	→	Left^#(x0)
Left^#(A1(x0))	→	Left^#(x0)
Left^#(A4(x0))	→	Left^#(x0)
Left^#(A5(x0))	→	Left^#(x0)

1.1.1.2 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1 over the arctic semiring over the integers

[A5(x₁)]

1	0	0	0
1	0	0	0
0	0	0	0
1	0	0	0

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

[A2(x₁)]

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

[A0(x₁)]

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

[A4(x₁)]

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

[Left^#(x₁)]

0	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞

· x₁ +

-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞

[A1(x₁)]

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

Left^#(A2(x0))	→	Left^#(x0)
Left^#(A0(x0))	→	Left^#(x0)
Left^#(A1(x0))	→	Left^#(x0)
Left^#(A4(x0))	→	Left^#(x0)

remain.

1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pairs

5^#(4(5(4(x0))))	→	5^#(4(4(x0)))
5^#(4(5(4(x0))))	→	5^#(5(4(4(x0))))

1.1.1.3 Reduction Pair Processor with Usable Rules

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight function

prec(5^#)	=	0	weight(5^#)	=	1
prec(A2)	=	0	weight(A2)	=	1
prec(A5)	=	0	weight(A5)	=	1
prec(A4)	=	8	weight(A4)	=	0
prec(2)	=	5	weight(2)	=	1
prec(Right14)	=	0	weight(Right14)	=	1
prec(Right13)	=	0	weight(Right13)	=	1
prec(Right12)	=	0	weight(Right12)	=	1
prec(Right11)	=	0	weight(Right11)	=	1
prec(Right10)	=	0	weight(Right10)	=	1
prec(Right9)	=	0	weight(Right9)	=	1
prec(Right8)	=	0	weight(Right8)	=	1
prec(Right7)	=	0	weight(Right7)	=	1
prec(Right6)	=	0	weight(Right6)	=	1
prec(Right5)	=	0	weight(Right5)	=	1
prec(Right4)	=	0	weight(Right4)	=	1
prec(Right3)	=	0	weight(Right3)	=	1
prec(Right2)	=	0	weight(Right2)	=	1
prec(Wait)	=	0	weight(Wait)	=	1
prec(Right1)	=	0	weight(Right1)	=	1
prec(Begin)	=	0	weight(Begin)	=	1
prec(4)	=	5	weight(4)	=	1
prec(5)	=	1	weight(5)	=	1

together with the usable rules

4(4(4(4(4(4(5(5(5(5(5(Begin(x0))))))))))))	→	Right4(Wait(x0))
4(4(4(4(4(4(5(5(5(5(Begin(x0)))))))))))	→	Right5(Wait(x0))
4(4(4(4(4(4(5(5(5(Begin(x0))))))))))	→	Right6(Wait(x0))
4(4(4(4(4(4(5(5(Begin(x0)))))))))	→	Right7(Wait(x0))
4(4(4(4(4(4(5(Begin(x0))))))))	→	Right8(Wait(x0))
4(4(4(4(4(4(Begin(x0)))))))	→	Right9(Wait(x0))
4(4(4(4(4(Begin(x0))))))	→	Right10(Wait(x0))
4(4(4(4(Begin(x0)))))	→	Right11(Wait(x0))
4(4(4(Begin(x0))))	→	Right12(Wait(x0))
4(4(Begin(x0)))	→	Right13(Wait(x0))
4(Begin(x0))	→	Right14(Wait(x0))
4(Right1(x0))	→	Right1(A4(x0))
4(Right2(x0))	→	Right2(A4(x0))
4(Right3(x0))	→	Right3(A4(x0))
4(Right4(x0))	→	Right4(A4(x0))
4(Right5(x0))	→	Right5(A4(x0))
4(Right6(x0))	→	Right6(A4(x0))
4(Right7(x0))	→	Right7(A4(x0))
4(Right8(x0))	→	Right8(A4(x0))
4(Right9(x0))	→	Right9(A4(x0))
4(Right10(x0))	→	Right10(A4(x0))
4(Right11(x0))	→	Right11(A4(x0))
4(Right12(x0))	→	Right12(A4(x0))
4(Right13(x0))	→	Right13(A4(x0))
4(Right14(x0))	→	Right14(A4(x0))
4(4(4(4(4(4(5(5(5(5(5(5(x0))))))))))))	→	2(x0)
2(Right1(x0))	→	Right1(A2(x0))
2(Right2(x0))	→	Right2(A2(x0))
2(Right3(x0))	→	Right3(A2(x0))
2(Right4(x0))	→	Right4(A2(x0))
2(Right5(x0))	→	Right5(A2(x0))
2(Right6(x0))	→	Right6(A2(x0))
2(Right7(x0))	→	Right7(A2(x0))
2(Right8(x0))	→	Right8(A2(x0))
2(Right9(x0))	→	Right9(A2(x0))
2(Right10(x0))	→	Right10(A2(x0))
2(Right11(x0))	→	Right11(A2(x0))
2(Right12(x0))	→	Right12(A2(x0))
2(Right13(x0))	→	Right13(A2(x0))
2(Right14(x0))	→	Right14(A2(x0))
5(4(5(Begin(x0))))	→	Right1(Wait(x0))
5(4(Begin(x0)))	→	Right2(Wait(x0))
5(Begin(x0))	→	Right3(Wait(x0))
5(Right1(x0))	→	Right1(A5(x0))
5(Right2(x0))	→	Right2(A5(x0))
5(Right3(x0))	→	Right3(A5(x0))
5(Right4(x0))	→	Right4(A5(x0))
5(Right5(x0))	→	Right5(A5(x0))
5(Right6(x0))	→	Right6(A5(x0))
5(Right7(x0))	→	Right7(A5(x0))
5(Right8(x0))	→	Right8(A5(x0))
5(Right9(x0))	→	Right9(A5(x0))
5(Right10(x0))	→	Right10(A5(x0))
5(Right11(x0))	→	Right11(A5(x0))
5(Right12(x0))	→	Right12(A5(x0))
5(Right13(x0))	→	Right13(A5(x0))
5(Right14(x0))	→	Right14(A5(x0))
5(4(5(4(x0))))	→	5(5(4(4(x0))))

(w.r.t. the implicit argument filter of the reduction pair), all pairs could be removed.

1.1.1.3.1 P is empty

There are no pairs anymore.

π(End^#)	=	1
π(A2)	=	[]
π(A5)	=	[]
π(A4)	=	[]
π(A1)	=	[]
π(1)	=	1
π(A0)	=	1
π(0)	=	1
π(2)	=	[]
π(Left)	=	1
π(Right14)	=	1
π(Right13)	=	1
π(Right12)	=	1
π(Right11)	=	[]
π(Right10)	=	[]
π(Right9)	=	1
π(Right8)	=	1
π(Right7)	=	[]
π(Right6)	=	1
π(Right5)	=	1
π(Right4)	=	1
π(Right3)	=	1
π(Right2)	=	1
π(Wait)	=	[]
π(Right1)	=	1
π(Begin)	=	1
π(4)	=	[1]
π(5)	=	[]