Consider the TRS R consisting of the rewrite rules

1: f(0) -> true
2: f(1) -> false
3: f(s(x)) -> f(x)
4: if(true,s(x),s(y)) -> s(x)
5: if(false,s(x),s(y)) -> s(y)
6: g(x,c(y)) -> c(g(x,y))
7: g(x,c(y)) -> g(x,if(f(x),c(g(s(x),y)),c(y)))

There are 6 dependency pairs:

8: F(s(x)) -> F(x)
9: G(x,c(y)) -> G(x,y)
10: G(x,c(y)) -> G(x,if(f(x),c(g(s(x),y)),c(y)))
11: G(x,c(y)) -> IF(f(x),c(g(s(x),y)),c(y))
12: G(x,c(y)) -> F(x)
13: G(x,c(y)) -> G(s(x),y)

The approximated dependency graph contains 2 SCCs:
{8}
and {9,10,13}.

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

- Consider the SCC {9,10,13}.
By taking the polynomial interpretation
[0] = [1] = [f](x) = [false] = [s](x) = [true] = 1,
[c](x) = x + 1,
[G](x,y) = x + y + 1
and [g](x,y) = [if](x,y,z) = y,
the rules in {1-7,10,13}
are weakly decreasing and
rule 9
is strictly decreasing.
There is one new SCC.

- Consider the SCC {10,13}.
By taking the polynomial interpretation
[0] = [1] = [f](x) = [false] = [s](x) = [true] = 1,
[c](x) = x + 1,
[g](x,y) = [if](x,y,z) = y
and [G](x,y) = y + 1,
the rules in {1-7,10}
are weakly decreasing and
rule 13
is strictly decreasing.
There is one new SCC.

- Consider the SCC {10}.
By taking the polynomial interpretation
[if](x,y,z) = [s](x) = 0,
[0] = [1] = [f](x) = [false] = [true] = 1,
[c](x) = x + 1
and [g](x,y) = [G](x,y) = x + y + 1,
the rules in {1-6}
are weakly decreasing and
the rules in {7,10}
are strictly decreasing.



Hence the TRS is terminating.