MAYBE Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

R(b(x0))	→	b(R(x0))
R(c(x0))	→	L(c(x0))
b(L(x0))	→	L(b(x0))
a(L(x0))	→	a(b(R(x0)))

Proof

1 Termination Assumption

We assume termination of the following TRS

R(b(x0))	→	b(R(x0))
R(c(x0))	→	L(c(x0))
b(L(x0))	→	L(b(x0))
a(L(x0))	→	a(b(R(x0)))