YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

1(q0(1(x0)))	→	0(1(q1(x0)))
1(q0(0(x0)))	→	0(0(q1(x0)))
1(q1(1(x0)))	→	1(1(q1(x0)))
1(q1(0(x0)))	→	1(0(q1(x0)))
0(q1(x0))	→	q2(1(x0))
1(q2(x0))	→	q2(1(x0))
0(q2(x0))	→	0(q0(x0))

Proof

1 Rule Removal

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

prec(q2)	=	1		weight(q2)	=	1
prec(0)	=	2		weight(0)	=	1
prec(q1)	=	7		weight(q1)	=	1
prec(q0)	=	0		weight(q0)	=	1
prec(1)	=	4		weight(1)	=	1

all rules could be removed.

1.1 R is empty

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