Consider the TRS R consisting of the rewrite rules

1: if(true,x,y) -> x
2: if(false,x,y) -> y
3: if(x,y,y) -> y
4: if(if(x,y,z),u,v) -> if(x,if(y,u,v),if(z,u,v))

There are 3 dependency pairs:

5: IF(if(x,y,z),u,v) -> IF(x,if(y,u,v),if(z,u,v))
6: IF(if(x,y,z),u,v) -> IF(y,u,v)
7: IF(if(x,y,z),u,v) -> IF(z,u,v)

The approximated dependency graph contains one SCC:
{5-7}.

- Consider the SCC {5-7}.
By taking the polynomial interpretation
[u] = [v] = 0,
[false] = [true] = 1
and [if](x,y,z) = [IF](x,y,z) = 2x + y + z + 1,
the rules in {4,5}
are weakly decreasing and
the rules in {1-3,6,7}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {5}.
By taking the polynomial interpretation
[u] = [v] = 0,
[false] = [true] = 1,
[IF](x,y,z) = 2x + y + 1
and [if](x,y,z) = 2x + y + z + 1,
rule 4
is weakly decreasing and
the rules in {1-3,5}
are strictly decreasing.


Hence the TRS is terminating.