YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

R(E(x0))	→	L(E(x0))
a(L(x0))	→	L(Aa(x0))
b(L(x0))	→	L(Ab(x0))
R(Aa(x0))	→	a(R(x0))
R(Ab(x0))	→	b(R(x0))
a(b(L(x0)))	→	b(a(R(x0)))

Proof

1 Rule Removal

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

prec(Ab)	=	0		weight(Ab)	=	1
prec(b)	=	1		weight(b)	=	1
prec(Aa)	=	0		weight(Aa)	=	1
prec(a)	=	5		weight(a)	=	1
prec(L)	=	0		weight(L)	=	1
prec(R)	=	7		weight(R)	=	1
prec(E)	=	0		weight(E)	=	1

all rules could be removed.

1.1 R is empty

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