Consider the TRS R consisting of the rewrite rules

1: 0(#) -> #
2: # + x -> x
3: x + # -> x
4: 0(x) + 0(y) -> 0(x + y)
5: 0(x) + 1(y) -> 1(x + y)
6: 1(x) + 0(y) -> 1(x + y)
7: 1(x) + 1(y) -> 0((x + y) + 1(#))
8: (x + y) + z -> x + (y + z)
9: # - x -> #
10: x - # -> x
11: 0(x) - 0(y) -> 0(x - y)
12: 0(x) - 1(y) -> 1((x - y) - 1(#))
13: 1(x) - 0(y) -> 1(x - y)
14: 1(x) - 1(y) -> 0(x - y)
15: not(true) -> false
16: not(false) -> true
17: if(true,x,y) -> x
18: if(false,x,y) -> y
19: ge(0(x),0(y)) -> ge(x,y)
20: ge(0(x),1(y)) -> not(ge(y,x))
21: ge(1(x),0(y)) -> ge(x,y)
22: ge(1(x),1(y)) -> ge(x,y)
23: ge(x,#) -> true
24: ge(#,0(x)) -> ge(#,x)
25: ge(#,1(x)) -> false
26: log(x) -> log'(x) - 1(#)
27: log'(#) -> #
28: log'(1(x)) -> log'(x) + 1(#)
29: log'(0(x)) -> if(ge(x,1(#)),log'(x) + 1(#),#)

There are 30 dependency pairs:

30: 0(x) +# 0(y) -> 0#(x + y)
31: 0(x) +# 0(y) -> x +# y
32: 0(x) +# 1(y) -> x +# y
33: 1(x) +# 0(y) -> x +# y
34: 1(x) +# 1(y) -> 0#((x + y) + 1(#))
35: 1(x) +# 1(y) -> (x + y) +# 1(#)
36: 1(x) +# 1(y) -> x +# y
37: (x + y) +# z -> x +# (y + z)
38: (x + y) +# z -> y +# z
39: 0(x) -# 0(y) -> 0#(x - y)
40: 0(x) -# 0(y) -> x -# y
41: 0(x) -# 1(y) -> (x - y) -# 1(#)
42: 0(x) -# 1(y) -> x -# y
43: 1(x) -# 0(y) -> x -# y
44: 1(x) -# 1(y) -> 0#(x - y)
45: 1(x) -# 1(y) -> x -# y
46: GE(0(x),0(y)) -> GE(x,y)
47: GE(0(x),1(y)) -> NOT(ge(y,x))
48: GE(0(x),1(y)) -> GE(y,x)
49: GE(1(x),0(y)) -> GE(x,y)
50: GE(1(x),1(y)) -> GE(x,y)
51: GE(#,0(x)) -> GE(#,x)
52: LOG(x) -> log'(x) -# 1(#)
53: LOG(x) -> LOG'(x)
54: LOG'(1(x)) -> log'(x) +# 1(#)
55: LOG'(1(x)) -> LOG'(x)
56: LOG'(0(x)) -> IF(ge(x,1(#)),log'(x) + 1(#),#)
57: LOG'(0(x)) -> GE(x,1(#))
58: LOG'(0(x)) -> log'(x) +# 1(#)
59: LOG'(0(x)) -> LOG'(x)

The approximated dependency graph contains 5 SCCs:
{51},
{31-33,35-38},
{40-43,45},
{46,48-50}
and {55,59}.

- Consider the SCC {51}.
There are no usable rules.
By taking the polynomial interpretation
[#] = 1,
[0](x) = x + 1
and [GE](x,y) = x + y + 1,
rule 51
is strictly decreasing.

- Consider the SCC {31-33,35-38}.
The usable rules are {1-8}.
By taking the polynomial interpretation
[#] = 0,
[0](x) = x,
[1](x) = x + 1
and [+](x,y) = [+#](x,y) = x + y + 1,
the rules in {1,4-8,31,35,37}
are weakly decreasing and
the rules in {2,3,32,33,36,38}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {31,35,37}.
By taking the polynomial interpretation
[#] = 0,
[0](x) = [1](x) = x + 1,
[+](x,y) = x + y
and [+#](x,y) = x + y + 1,
the rules in {2,3,7,8,37}
are weakly decreasing and
the rules in {1,4-6,31,35}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {37}.
By taking the polynomial interpretation
[#] = 0,
[0](x) = x,
[+#](x,y) = [1](x) = x + 1
and [+](x,y) = x + y + 1,
the rules in {1,4-8}
are weakly decreasing and
the rules in {2,3,37}
are strictly decreasing.



- Consider the SCC {40-43,45}.
The usable rules are {1,9-14}.
By taking the polynomial interpretation
[#] = 0,
[0](x) = [1](x) = x + 1,
[-](x,y) = x + y
and [-#](x,y) = x + y + 1,
the rules in {9,10,12}
are weakly decreasing and
the rules in {1,11,13,14,40-43,45}
are strictly decreasing.

- Consider the SCC {46,48-50}.
There are no usable rules.
By taking the polynomial interpretation
[0](x) = [1](x) = x + 1
and [GE](x,y) = x + y + 1,
the rules in {46,48-50}
are strictly decreasing.

- Consider the SCC {55,59}.
There are no usable rules.
By taking the polynomial interpretation
[0](x) = [1](x) = [LOG'](x) = x + 1,
the rules in {55,59}
are strictly decreasing.

Hence the TRS is terminating.