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 - # -> x
10: # - 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(false) -> true
16: not(true) -> false
17: and(x,true) -> x
18: and(x,false) -> false
19: if(true,x,y) -> x
20: if(false,x,y) -> y
21: ge(0(x),0(y)) -> ge(x,y)
22: ge(0(x),1(y)) -> not(ge(y,x))
23: ge(1(x),0(y)) -> ge(x,y)
24: ge(1(x),1(y)) -> ge(x,y)
25: ge(x,#) -> true
26: ge(#,1(x)) -> false
27: ge(#,0(x)) -> ge(#,x)
28: val(l(x)) -> x
29: val(n(x,y,z)) -> x
30: min(l(x)) -> x
31: min(n(x,y,z)) -> min(y)
32: max(l(x)) -> x
33: max(n(x,y,z)) -> max(z)
34: bs(l(x)) -> true
35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
36: size(l(x)) -> 1(#)
37: size(n(x,y,z)) -> (size(x) + size(y)) + 1(#)
38: wb(l(x)) -> true
39: wb(n(x,y,z)) -> and(if(ge(size(y),size(z)),ge(1(#),size(y) - size(z)),ge(1(#),size(z) - size(y))),and(wb(y),wb(z)))

There are 49 dependency pairs:

40: 0(x) +# 0(y) -> 0#(x + y)
41: 0(x) +# 0(y) -> x +# y
42: 0(x) +# 1(y) -> x +# y
43: 1(x) +# 0(y) -> x +# y
44: 1(x) +# 1(y) -> 0#((x + y) + 1(#))
45: 1(x) +# 1(y) -> (x + y) +# 1(#)
46: 1(x) +# 1(y) -> x +# y
47: x +# (y + z) -> (x + y) +# z
48: x +# (y + z) -> x +# y
49: 0(x) -# 0(y) -> 0#(x - y)
50: 0(x) -# 0(y) -> x -# y
51: 0(x) -# 1(y) -> (x - y) -# 1(#)
52: 0(x) -# 1(y) -> x -# y
53: 1(x) -# 0(y) -> x -# y
54: 1(x) -# 1(y) -> 0#(x - y)
55: 1(x) -# 1(y) -> x -# y
56: GE(0(x),0(y)) -> GE(x,y)
57: GE(0(x),1(y)) -> NOT(ge(y,x))
58: GE(0(x),1(y)) -> GE(y,x)
59: GE(1(x),0(y)) -> GE(x,y)
60: GE(1(x),1(y)) -> GE(x,y)
61: GE(#,0(x)) -> GE(#,x)
62: MIN(n(x,y,z)) -> MIN(y)
63: MAX(n(x,y,z)) -> MAX(z)
64: BS(n(x,y,z)) -> AND(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
65: BS(n(x,y,z)) -> AND(ge(x,max(y)),ge(min(z),x))
66: BS(n(x,y,z)) -> GE(x,max(y))
67: BS(n(x,y,z)) -> MAX(y)
68: BS(n(x,y,z)) -> GE(min(z),x)
69: BS(n(x,y,z)) -> MIN(z)
70: BS(n(x,y,z)) -> AND(bs(y),bs(z))
71: BS(n(x,y,z)) -> BS(y)
72: BS(n(x,y,z)) -> BS(z)
73: SIZE(n(x,y,z)) -> (size(x) + size(y)) +# 1(#)
74: SIZE(n(x,y,z)) -> size(x) +# size(y)
75: SIZE(n(x,y,z)) -> SIZE(x)
76: SIZE(n(x,y,z)) -> SIZE(y)
77: WB(n(x,y,z)) -> AND(if(ge(size(y),size(z)),ge(1(#),size(y) - size(z)),ge(1(#),size(z) - size(y))),and(wb(y),wb(z)))
78: WB(n(x,y,z)) -> IF(ge(size(y),size(z)),ge(1(#),size(y) - size(z)),ge(1(#),size(z) - size(y)))
79: WB(n(x,y,z)) -> GE(size(y),size(z))
80: WB(n(x,y,z)) -> GE(1(#),size(y) - size(z))
81: WB(n(x,y,z)) -> size(y) -# size(z)
82: WB(n(x,y,z)) -> GE(1(#),size(z) - size(y))
83: WB(n(x,y,z)) -> size(z) -# size(y)
84: WB(n(x,y,z)) -> SIZE(z)
85: WB(n(x,y,z)) -> SIZE(y)
86: WB(n(x,y,z)) -> AND(wb(y),wb(z))
87: WB(n(x,y,z)) -> WB(y)
88: WB(n(x,y,z)) -> WB(z)

The approximated dependency graph contains 9 SCCs:
{61},
{63},
{62},
{41-43,45-48},
{75,76},
{50-53,55},
{56,58-60},
{71,72}
and {87,88}.

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

- Consider the SCC {63}.
There are no usable rules.
By taking the polynomial interpretation
[MAX](x) = x + 1
and [n](x,y,z) = x + y + z + 1,
rule 63
is strictly decreasing.

- Consider the SCC {62}.
There are no usable rules.
By taking the polynomial interpretation
[MIN](x) = x + 1
and [n](x,y,z) = x + y + z + 1,
rule 62
is strictly decreasing.

- Consider the SCC {41-43,45-48}.
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,41,45,47}
are weakly decreasing and
the rules in {2,3,42,43,46,48}
are strictly decreasing.
There are 2 new SCCs.

- Consider the SCC {45}.
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}
are weakly decreasing and
the rules in {1,4-6,45}
are strictly decreasing.

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

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



- Consider the SCC {75,76}.
There are no usable rules.
By taking the polynomial interpretation
[SIZE](x) = x + 1
and [n](x,y,z) = x + y + z + 1,
the rules in {75,76}
are strictly decreasing.

- Consider the SCC {50-53,55}.
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,50-53,55}
are strictly decreasing.

- Consider the SCC {56,58-60}.
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 {56,58-60}
are strictly decreasing.

- Consider the SCC {71,72}.
There are no usable rules.
By taking the polynomial interpretation
[BS](x) = x + 1
and [n](x,y,z) = x + y + z + 1,
the rules in {71,72}
are strictly decreasing.

- Consider the SCC {87,88}.
There are no usable rules.
By taking the polynomial interpretation
[WB](x) = x + 1
and [n](x,y,z) = x + y + z + 1,
the rules in {87,88}
are strictly decreasing.

Hence the TRS is terminating.