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: foldB(t,0) -> t
8: foldB(t,s(n)) -> f(foldB(t,n),B)
9: foldC(t,0) -> t
10: foldC(t,s(n)) -> f(foldC(t,n),C)
11: f(t,x) -> f'(t,g(x))
12: f'(triple(a,b,c),C) -> triple(a,b,s(c))
13: f'(triple(a,b,c),B) -> f(triple(a,b,c),A)
14: f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b))
15: f''(triple(a,b,c)) -> foldC(triple(a,b,0),c)
16: fold(t,x,0) -> t
17: fold(t,x,s(n)) -> f(fold(t,x,n),x)

There are 12 dependency pairs:

18: FOLDB(t,s(n)) -> F(foldB(t,n),B)
19: FOLDB(t,s(n)) -> FOLDB(t,n)
20: FOLDC(t,s(n)) -> F(foldC(t,n),C)
21: FOLDC(t,s(n)) -> FOLDC(t,n)
22: F(t,x) -> F'(t,g(x))
23: F(t,x) -> G(x)
24: F'(triple(a,b,c),B) -> F(triple(a,b,c),A)
25: F'(triple(a,b,c),A) -> F''(foldB(triple(s(a),0,c),b))
26: F'(triple(a,b,c),A) -> FOLDB(triple(s(a),0,c),b)
27: F''(triple(a,b,c)) -> FOLDC(triple(a,b,0),c)
28: FOLD(t,x,s(n)) -> F(fold(t,x,n),x)
29: FOLD(t,x,s(n)) -> FOLD(t,x,n)

The approximated dependency graph contains 2 SCCs:
{18-22,24-27}
and {29}.

- Consider the SCC {18-22,24-27}.
The usable rules are {1-15}.
By taking the polynomial interpretation
[0] = 0,
[A] = [B] = [C] = [g](x) = 1,
[f''](x) = [F''](x) = x,
[f](x,y) = [F](x,y) = [s](x) = x + 1,
[f'](x,y) = [F'](x,y) = [foldB](x,y) = [FOLDB](x,y) = [foldC](x,y) = [FOLDC](x,y) = x + y
and [triple](x,y,z) = x + y + z + 1,
the rules in {1-15,18,20,22,24-27}
are weakly decreasing and
the rules in {19,21}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {18,20,22,24-27}.
By taking the polynomial interpretation
[0] = 0,
[A] = [B] = [C] = [g](x) = 1,
[f](x,y) = [F](x,y) = [f''](x) = [F''](x) = [s](x) = x + 1,
[f'](x,y) = [F'](x,y) = [foldB](x,y) = x + y,
[FOLDB](x,y) = [foldC](x,y) = [FOLDC](x,y) = x + y + 1
and [triple](x,y,z) = y + z + 1,
the rules in {1-8,10-15,20,22,24-27}
are weakly decreasing and
the rules in {9,18}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {20,22,24,25,27}.
By taking the polynomial interpretation
[0] = 0,
[A] = [B] = [C] = 1,
[f](x,y) = [F](x,y) = [f'](x,y) = [F'](x,y) = [f''](x) = [F''](x) = [g](x) = [s](x) = x + 1,
[foldB](x,y) = [foldC](x,y) = x + y,
[FOLDC](x,y) = x + y + 1
and [triple](x,y,z) = y + z + 1,
the rules in {7-14,22,24,25,27}
are weakly decreasing and
the rules in {1-6,15,20}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {22,24}.
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,22}
are weakly decreasing and
the rules in {2,4,24}
are strictly decreasing.




- Consider the SCC {29}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [FOLD](x,y,z) = x + y + z + 1,
rule 29
is strictly decreasing.

Hence the TRS is terminating.