YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(a(x0)) → b(c(x0))
b(b(x0)) → c(d(x0))
b(x0) → a(x0)
c(c(x0)) → d(f(x0))
d(d(x0)) → f(f(f(x0)))
d(x0) → b(x0)
f(f(x0)) → g(a(x0))
g(g(x0)) → a(x0)

Proof

1 Bounds

The given TRS is match-bounded by 3. This is shown by the following automaton.