Consider the TRS R consisting of the rewrite rules

1: g(A) -> A
2: g(B) -> A
3: g(B) -> B
4: g(C) -> A
5: g(C) -> B
6: g(C) -> C
7: foldf(x,nil) -> x
8: foldf(x,cons(y,z)) -> f(foldf(x,z),y)
9: f(t,x) -> f'(t,g(x))
10: f'(triple(a,b,c),C) -> triple(a,b,cons(C,c))
11: f'(triple(a,b,c),B) -> f(triple(a,b,c),A)
12: f'(triple(a,b,c),A) -> f''(foldf(triple(cons(A,a),nil,c),b))
13: f''(triple(a,b,c)) -> foldf(triple(a,b,nil),c)

There are 8 dependency pairs:

14: FOLDF(x,cons(y,z)) -> F(foldf(x,z),y)
15: FOLDF(x,cons(y,z)) -> FOLDF(x,z)
16: F(t,x) -> F'(t,g(x))
17: F(t,x) -> G(x)
18: F'(triple(a,b,c),B) -> F(triple(a,b,c),A)
19: F'(triple(a,b,c),A) -> F''(foldf(triple(cons(A,a),nil,c),b))
20: F'(triple(a,b,c),A) -> FOLDF(triple(cons(A,a),nil,c),b)
21: F''(triple(a,b,c)) -> FOLDF(triple(a,b,nil),c)

The approximated dependency graph contains one SCC:
{14-16,18-21}.

- Consider the SCC {14-16,18-21}.
By taking the polynomial interpretation
[C] = [nil] = 0,
[A] = [B] = 1,
[f](x,y) = [F](x,y) = [f'](x,y) = [F'](x,y) = [f''](x) = [F''](x) = [g](x) = x + 1,
[foldf](x,y) = x + y,
[cons](x,y) = [FOLDF](x,y) = x + y + 1
and [triple](x,y,z) = y + z + 1,
the rules in {4,5,7-12,16,18-21}
are weakly decreasing and
the rules in {1-3,6,13-15}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {16,18}.
The usable rules are {1-6}.
By taking the polynomial interpretation
[A] = 0,
[B] = [C] = 1,
[g](x) = x,
[F](x,y) = [F'](x,y) = x + y + 1
and [triple](x,y,z) = x + y + z + 1,
the rules in {1,3,5,6,16}
are weakly decreasing and
the rules in {2,4,18}
are strictly decreasing.


Hence the TRS is terminating.