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)

There are 10 dependency pairs:

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

The approximated dependency graph contains one SCC:
{16-20,22-25}.

- Consider the SCC {16-20,22-25}.
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-16,18,20,22-25}
are weakly decreasing and
the rules in {17,19}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {16,18,20,22-25}.
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,18,20,22-25}
are weakly decreasing and
the rules in {9,16}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {18,20,22,23,25}.
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,20,22,23,25}
are weakly decreasing and
the rules in {1-6,15,18}
are strictly decreasing.
There is one new SCC.

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




Hence the TRS is terminating.