YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(0(((x0))))	→	((1(1(x0))))
1(1(((x0))))	→	0(0(#(#(x0))))
#(#(0(0(x0))))	→	0(0(#(#(x0))))
#(#(1(1(x0))))	→	1(1(#(#(x0))))
#(#($($(x0))))	→	(($($(x0))))
#(#(#(#(x0))))	→	#(#(x0))
#(#(((x0))))	→	((x0))

Proof

1 Rule Removal

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

prec($)	=	0		weight($)	=	1
prec(#)	=	6		weight(#)	=	1
prec(1)	=	4		weight(1)	=	1
prec(0)	=	1		weight(0)	=	1
prec(*)	=	0		weight(*)	=	1

all rules could be removed.

1.1 R is empty

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