YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(2(3(4(x0)))))	→	0(2(3(1(4(x0)))))
0(5(1(2(3(4(x0))))))	→	0(1(2(5(3(4(x0))))))
0(5(1(2(3(4(x0))))))	→	0(5(2(1(3(4(x0))))))
0(5(1(2(3(4(x0))))))	→	5(0(2(3(1(4(x0))))))
0(5(2(3(1(4(x0))))))	→	0(1(5(2(3(4(x0))))))

Proof

1 Rule Removal

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

prec(5)	=	2		weight(5)	=	1
prec(0)	=	3		weight(0)	=	0
prec(1)	=	1		weight(1)	=	1
prec(2)	=	0		weight(2)	=	1
prec(3)	=	0		weight(3)	=	1
prec(4)	=	0		weight(4)	=	1

all rules could be removed.

1.1 R is empty

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