MAYBE Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

s(b(x0)) → b(s(s(s(x0))))
s(b(s(x0))) → b(t(x0))
t(b(x0)) → b(s(x0))
t(b(s(x0))) → u(t(b(x0)))
b(u(x0)) → b(s(x0))
t(s(x0)) → t(t(x0))
t(u(x0)) → u(t(x0))
s(u(x0)) → s(s(x0))

Proof

1 Termination Assumption

We assume termination of the following TRS
s(b(x0)) → b(s(s(s(x0))))
s(b(s(x0))) → b(t(x0))
t(b(x0)) → b(s(x0))
t(b(s(x0))) → u(t(b(x0)))
b(u(x0)) → b(s(x0))
t(s(x0)) → t(t(x0))
t(u(x0)) → u(t(x0))
s(u(x0)) → s(s(x0))