Consider the TRS R consisting of the rewrite rules

1: O(0) -> 0
2: 0 + x -> x
3: x + 0 -> x
4: O(x) + O(y) -> O(x + y)
5: O(x) + I(y) -> I(x + y)
6: I(x) + O(y) -> I(x + y)
7: I(x) + I(y) -> O((x + y) + I(0))
8: 0 * x -> 0
9: x * 0 -> 0
10: O(x) * y -> O(x * y)
11: I(x) * y -> O(x * y) + y
12: x - 0 -> x
13: 0 - x -> 0
14: O(x) - O(y) -> O(x - y)
15: O(x) - I(y) -> I((x - y) - I(1))
16: I(x) - O(y) -> I(x - y)
17: I(x) - I(y) -> O(x - y)

There are 19 dependency pairs:

18: O(x) +# O(y) -> O#(x + y)
19: O(x) +# O(y) -> x +# y
20: O(x) +# I(y) -> x +# y
21: I(x) +# O(y) -> x +# y
22: I(x) +# I(y) -> O#((x + y) + I(0))
23: I(x) +# I(y) -> (x + y) +# I(0)
24: I(x) +# I(y) -> x +# y
25: O(x) *# y -> O#(x * y)
26: O(x) *# y -> x *# y
27: I(x) *# y -> O(x * y) +# y
28: I(x) *# y -> O#(x * y)
29: I(x) *# y -> x *# y
30: O(x) -# O(y) -> O#(x - y)
31: O(x) -# O(y) -> x -# y
32: O(x) -# I(y) -> (x - y) -# I(1)
33: O(x) -# I(y) -> x -# y
34: I(x) -# O(y) -> x -# y
35: I(x) -# I(y) -> O#(x - y)
36: I(x) -# I(y) -> x -# y

The approximated dependency graph contains 3 SCCs:
{19-21,23,24},
{26,29}
and {31-34,36}.

- Consider the SCC {19-21,23,24}.
The usable rules are {1-7}.
By taking the polynomial interpretation
[0] = 1,
[O](x) = x,
[I](x) = x + 1,
[+](x,y) = x + y
and [+#](x,y) = x + y + 1,
the rules in {1,4-7,19,23}
are weakly decreasing and
the rules in {2,3,20,21,24}
are strictly decreasing.
There are 2 new SCCs.

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

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


- Consider the SCC {26,29}.
There are no usable rules.
By taking the polynomial interpretation
[I](x) = [O](x) = x + 1
and [*#](x,y) = x + y + 1,
the rules in {26,29}
are strictly decreasing.

- Consider the SCC {31-34,36}.
The usable rules are {1,12-17}.
By taking the polynomial interpretation
[1] = 0,
[0] = 1,
[I](x) = [O](x) = x + 1,
[-](x,y) = x + y
and [-#](x,y) = x + y + 1,
the rules in {13,15}
are weakly decreasing and
the rules in {1,12,14,16,17,31-34,36}
are strictly decreasing.

Hence the TRS is terminating.