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

There are 12 dependency pairs:

12: O(x) +# O(y) -> O#(x + y)
13: O(x) +# O(y) -> x +# y
14: O(x) +# I(y) -> x +# y
15: I(x) +# O(y) -> x +# y
16: I(x) +# I(y) -> O#((x + y) + I(0))
17: I(x) +# I(y) -> (x + y) +# I(0)
18: I(x) +# I(y) -> x +# y
19: O(x) *# y -> O#(x * y)
20: O(x) *# y -> x *# y
21: I(x) *# y -> O(x * y) +# y
22: I(x) *# y -> O#(x * y)
23: I(x) *# y -> x *# y

The approximated dependency graph contains 2 SCCs:
{13-15,17,18}
and {20,23}.

- Consider the SCC {13-15,17,18}.
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,13,17}
are weakly decreasing and
the rules in {2,3,14,15,18}
are strictly decreasing.
There are 2 new SCCs.

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

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


- Consider the SCC {20,23}.
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 {20,23}
are strictly decreasing.

Hence the TRS is terminating.