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,x,y) -> x
5: if(false,x,y) -> y
6: g(s(x),s(y)) -> if(f(x),s(x),s(y))
7: g(x,c(y)) -> g(x,g(s(c(y)),y))

There are 5 dependency pairs:

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

The approximated dependency graph contains 2 SCCs:
{8}
and {11,12}.

- 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 {11,12}.
By taking the polynomial interpretation
[0] = [1] = [f](x) = [false] = [s](x) = [true] = 1,
[c](x) = x + 1,
[g](x,y) = [G](x,y) = y + 1
and [if](x,y,z) = y + z,
the rules in {1-7,11}
are weakly decreasing and
rule 12
is strictly decreasing.
There is one new SCC.

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


Hence the TRS is terminating.