Consider the TRS R consisting of the rewrite rules

1: c(c(c(a(x,y)))) -> b(c(c(c(c(y)))),x)
2: c(c(b(c(y),0))) -> a(0,c(c(a(y,0))))
3: c(c(a(a(y,0),x))) -> c(y)

There are 7 dependency pairs:

4: C(c(c(a(x,y)))) -> C(c(c(c(y))))
5: C(c(c(a(x,y)))) -> C(c(c(y)))
6: C(c(c(a(x,y)))) -> C(c(y))
7: C(c(c(a(x,y)))) -> C(y)
8: C(c(b(c(y),0))) -> C(c(a(y,0)))
9: C(c(b(c(y),0))) -> C(a(y,0))
10: C(c(a(a(y,0),x))) -> C(y)

The approximated dependency graph contains one SCC:
{4-8,10}.

- Consider the SCC {4-8,10}.
By taking the polynomial interpretation
[0] = 0,
[c](x) = 2x,
[C](x) = x + 1,
[a](x,y) = x + 2y + 1
and [b](x,y) = x + 3y + 3,
the rules in {1-8,10}
are strictly decreasing.

Hence the TRS is terminating.