YES
TRS:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
DP:
Strict:
{+#(O(x), O(y)) -> O#(+(x, y)),
+#(O(x), O(y)) -> +#(x, y),
+#(O(x), I(y)) -> +#(x, y),
+#(I(x), O(y)) -> +#(x, y),
+#(I(x), I(y)) -> O#(+(+(x, y), I(0()))),
+#(I(x), I(y)) -> +#(x, y),
+#(I(x), I(y)) -> +#(+(x, y), I(0())),
*#(O(x), y) -> O#(*(x, y)),
*#(O(x), y) -> *#(x, y),
*#(I(x), y) -> O#(*(x, y)),
*#(I(x), y) -> +#(O(*(x, y)), y),
*#(I(x), y) -> *#(x, y),
-#(O(x), O(y)) -> O#(-(x, y)),
-#(O(x), O(y)) -> -#(x, y),
-#(O(x), I(y)) -> -#(x, y),
-#(O(x), I(y)) -> -#(-(x, y), I(1())),
-#(I(x), O(y)) -> -#(x, y),
-#(I(x), I(y)) -> O#(-(x, y)),
-#(I(x), I(y)) -> -#(x, y)}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
EDG:
{(+#(O(x), I(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0())))
(+#(O(x), I(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(x, y))
(+#(O(x), I(y)) -> +#(x, y), +#(I(x), I(y)) -> O#(+(+(x, y), I(0()))))
(+#(O(x), I(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y))
(+#(O(x), I(y)) -> +#(x, y), +#(O(x), I(y)) -> +#(x, y))
(+#(O(x), I(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y))
(+#(O(x), I(y)) -> +#(x, y), +#(O(x), O(y)) -> O#(+(x, y)))
(+#(I(x), I(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0())))
(+#(I(x), I(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(x, y))
(+#(I(x), I(y)) -> +#(x, y), +#(I(x), I(y)) -> O#(+(+(x, y), I(0()))))
(+#(I(x), I(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y))
(+#(I(x), I(y)) -> +#(x, y), +#(O(x), I(y)) -> +#(x, y))
(+#(I(x), I(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y))
(+#(I(x), I(y)) -> +#(x, y), +#(O(x), O(y)) -> O#(+(x, y)))
(*#(I(x), y) -> *#(x, y), *#(I(x), y) -> *#(x, y))
(*#(I(x), y) -> *#(x, y), *#(I(x), y) -> +#(O(*(x, y)), y))
(*#(I(x), y) -> *#(x, y), *#(I(x), y) -> O#(*(x, y)))
(*#(I(x), y) -> *#(x, y), *#(O(x), y) -> *#(x, y))
(*#(I(x), y) -> *#(x, y), *#(O(x), y) -> O#(*(x, y)))
(-#(O(x), I(y)) -> -#(x, y), -#(I(x), I(y)) -> -#(x, y))
(-#(O(x), I(y)) -> -#(x, y), -#(I(x), I(y)) -> O#(-(x, y)))
(-#(O(x), I(y)) -> -#(x, y), -#(I(x), O(y)) -> -#(x, y))
(-#(O(x), I(y)) -> -#(x, y), -#(O(x), I(y)) -> -#(-(x, y), I(1())))
(-#(O(x), I(y)) -> -#(x, y), -#(O(x), I(y)) -> -#(x, y))
(-#(O(x), I(y)) -> -#(x, y), -#(O(x), O(y)) -> -#(x, y))
(-#(O(x), I(y)) -> -#(x, y), -#(O(x), O(y)) -> O#(-(x, y)))
(-#(I(x), I(y)) -> -#(x, y), -#(I(x), I(y)) -> -#(x, y))
(-#(I(x), I(y)) -> -#(x, y), -#(I(x), I(y)) -> O#(-(x, y)))
(-#(I(x), I(y)) -> -#(x, y), -#(I(x), O(y)) -> -#(x, y))
(-#(I(x), I(y)) -> -#(x, y), -#(O(x), I(y)) -> -#(-(x, y), I(1())))
(-#(I(x), I(y)) -> -#(x, y), -#(O(x), I(y)) -> -#(x, y))
(-#(I(x), I(y)) -> -#(x, y), -#(O(x), O(y)) -> -#(x, y))
(-#(I(x), I(y)) -> -#(x, y), -#(O(x), O(y)) -> O#(-(x, y)))
(*#(I(x), y) -> +#(O(*(x, y)), y), +#(I(x), I(y)) -> +#(+(x, y), I(0())))
(*#(I(x), y) -> +#(O(*(x, y)), y), +#(I(x), I(y)) -> +#(x, y))
(*#(I(x), y) -> +#(O(*(x, y)), y), +#(I(x), I(y)) -> O#(+(+(x, y), I(0()))))
(*#(I(x), y) -> +#(O(*(x, y)), y), +#(I(x), O(y)) -> +#(x, y))
(*#(I(x), y) -> +#(O(*(x, y)), y), +#(O(x), I(y)) -> +#(x, y))
(*#(I(x), y) -> +#(O(*(x, y)), y), +#(O(x), O(y)) -> +#(x, y))
(*#(I(x), y) -> +#(O(*(x, y)), y), +#(O(x), O(y)) -> O#(+(x, y)))
(+#(I(x), I(y)) -> +#(+(x, y), I(0())), +#(I(x), I(y)) -> +#(+(x, y), I(0())))
(+#(I(x), I(y)) -> +#(+(x, y), I(0())), +#(I(x), I(y)) -> +#(x, y))
(+#(I(x), I(y)) -> +#(+(x, y), I(0())), +#(I(x), I(y)) -> O#(+(+(x, y), I(0()))))
(+#(I(x), I(y)) -> +#(+(x, y), I(0())), +#(O(x), I(y)) -> +#(x, y))
(-#(O(x), I(y)) -> -#(-(x, y), I(1())), -#(O(x), I(y)) -> -#(x, y))
(-#(O(x), I(y)) -> -#(-(x, y), I(1())), -#(O(x), I(y)) -> -#(-(x, y), I(1())))
(-#(O(x), I(y)) -> -#(-(x, y), I(1())), -#(I(x), I(y)) -> O#(-(x, y)))
(-#(O(x), I(y)) -> -#(-(x, y), I(1())), -#(I(x), I(y)) -> -#(x, y))
(-#(I(x), O(y)) -> -#(x, y), -#(O(x), O(y)) -> O#(-(x, y)))
(-#(I(x), O(y)) -> -#(x, y), -#(O(x), O(y)) -> -#(x, y))
(-#(I(x), O(y)) -> -#(x, y), -#(O(x), I(y)) -> -#(x, y))
(-#(I(x), O(y)) -> -#(x, y), -#(O(x), I(y)) -> -#(-(x, y), I(1())))
(-#(I(x), O(y)) -> -#(x, y), -#(I(x), O(y)) -> -#(x, y))
(-#(I(x), O(y)) -> -#(x, y), -#(I(x), I(y)) -> O#(-(x, y)))
(-#(I(x), O(y)) -> -#(x, y), -#(I(x), I(y)) -> -#(x, y))
(-#(O(x), O(y)) -> -#(x, y), -#(O(x), O(y)) -> O#(-(x, y)))
(-#(O(x), O(y)) -> -#(x, y), -#(O(x), O(y)) -> -#(x, y))
(-#(O(x), O(y)) -> -#(x, y), -#(O(x), I(y)) -> -#(x, y))
(-#(O(x), O(y)) -> -#(x, y), -#(O(x), I(y)) -> -#(-(x, y), I(1())))
(-#(O(x), O(y)) -> -#(x, y), -#(I(x), O(y)) -> -#(x, y))
(-#(O(x), O(y)) -> -#(x, y), -#(I(x), I(y)) -> O#(-(x, y)))
(-#(O(x), O(y)) -> -#(x, y), -#(I(x), I(y)) -> -#(x, y))
(*#(O(x), y) -> *#(x, y), *#(O(x), y) -> O#(*(x, y)))
(*#(O(x), y) -> *#(x, y), *#(O(x), y) -> *#(x, y))
(*#(O(x), y) -> *#(x, y), *#(I(x), y) -> O#(*(x, y)))
(*#(O(x), y) -> *#(x, y), *#(I(x), y) -> +#(O(*(x, y)), y))
(*#(O(x), y) -> *#(x, y), *#(I(x), y) -> *#(x, y))
(+#(I(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> O#(+(x, y)))
(+#(I(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y))
(+#(I(x), O(y)) -> +#(x, y), +#(O(x), I(y)) -> +#(x, y))
(+#(I(x), O(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y))
(+#(I(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> O#(+(+(x, y), I(0()))))
(+#(I(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(x, y))
(+#(I(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0())))
(+#(O(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> O#(+(x, y)))
(+#(O(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y))
(+#(O(x), O(y)) -> +#(x, y), +#(O(x), I(y)) -> +#(x, y))
(+#(O(x), O(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y))
(+#(O(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> O#(+(+(x, y), I(0()))))
(+#(O(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(x, y))
(+#(O(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0())))}
SCCS:
Scc:
{-#(O(x), O(y)) -> -#(x, y),
-#(O(x), I(y)) -> -#(x, y),
-#(O(x), I(y)) -> -#(-(x, y), I(1())),
-#(I(x), O(y)) -> -#(x, y),
-#(I(x), I(y)) -> -#(x, y)}
Scc:
{*#(O(x), y) -> *#(x, y),
*#(I(x), y) -> *#(x, y)}
Scc:
{+#(O(x), O(y)) -> +#(x, y),
+#(O(x), I(y)) -> +#(x, y),
+#(I(x), O(y)) -> +#(x, y),
+#(I(x), I(y)) -> +#(x, y),
+#(I(x), I(y)) -> +#(+(x, y), I(0()))}
SCC:
Strict:
{-#(O(x), O(y)) -> -#(x, y),
-#(O(x), I(y)) -> -#(x, y),
-#(O(x), I(y)) -> -#(-(x, y), I(1())),
-#(I(x), O(y)) -> -#(x, y),
-#(I(x), I(y)) -> -#(x, y)}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
POLY:
Argument Filtering:
pi(1) = [], pi(-#) = [0], pi(-) = 0, pi(*) = [], pi(I) = [0], pi(+) = [], pi(O) = [0], pi(0) = []
Usable Rules:
{}
Interpretation:
[-#](x0) = x0 + 1,
[I](x0) = x0 + 1,
[O](x0) = x0 + 1
Strict:
{}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
Qed
SCC:
Strict:
{*#(O(x), y) -> *#(x, y),
*#(I(x), y) -> *#(x, y)}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
SPSC:
Simple Projection:
pi(*#) = 0
Strict:
{*#(O(x), y) -> *#(x, y)}
EDG:
{(*#(O(x), y) -> *#(x, y), *#(O(x), y) -> *#(x, y))}
SCCS:
Scc:
{*#(O(x), y) -> *#(x, y)}
SCC:
Strict:
{*#(O(x), y) -> *#(x, y)}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
SPSC:
Simple Projection:
pi(*#) = 0
Strict:
{}
Qed
SCC:
Strict:
{+#(O(x), O(y)) -> +#(x, y),
+#(O(x), I(y)) -> +#(x, y),
+#(I(x), O(y)) -> +#(x, y),
+#(I(x), I(y)) -> +#(x, y),
+#(I(x), I(y)) -> +#(+(x, y), I(0()))}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
POLY:
Argument Filtering:
pi(1) = [], pi(-) = [], pi(*) = [], pi(I) = [0], pi(+#) = 1, pi(+) = [], pi(O) = 0, pi(0) = []
Usable Rules:
{}
Interpretation:
[I](x0) = x0 + 1,
[0] = 0
Strict:
{+#(O(x), O(y)) -> +#(x, y),
+#(I(x), O(y)) -> +#(x, y),
+#(I(x), I(y)) -> +#(+(x, y), I(0()))}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
EDG:
{(+#(I(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0())))
(+#(I(x), O(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y))
(+#(I(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y))
(+#(I(x), I(y)) -> +#(+(x, y), I(0())), +#(I(x), I(y)) -> +#(+(x, y), I(0())))
(+#(O(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y))
(+#(O(x), O(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y))
(+#(O(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0())))}
SCCS:
Scc:
{+#(I(x), I(y)) -> +#(+(x, y), I(0()))}
Scc:
{+#(O(x), O(y)) -> +#(x, y),
+#(I(x), O(y)) -> +#(x, y)}
SCC:
Strict:
{+#(I(x), I(y)) -> +#(+(x, y), I(0()))}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
POLY:
Argument Filtering:
pi(1) = [], pi(-) = [], pi(*) = [], pi(I) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(O) = 0, pi(0) = []
Usable Rules:
{}
Interpretation:
[+#](x0, x1) = x0 + x1,
[+](x0, x1) = x0 + x1,
[I](x0) = x0 + 1,
[0] = 0
Strict:
{}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
Qed
SCC:
Strict:
{+#(O(x), O(y)) -> +#(x, y),
+#(I(x), O(y)) -> +#(x, y)}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
SPSC:
Simple Projection:
pi(+#) = 0
Strict:
{+#(O(x), O(y)) -> +#(x, y)}
EDG:
{(+#(O(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y))}
SCCS:
Scc:
{+#(O(x), O(y)) -> +#(x, y)}
SCC:
Strict:
{+#(O(x), O(y)) -> +#(x, y)}
Weak:
{ O(0()) -> 0(),
+(x, 0()) -> x,
+(0(), x) -> x,
+(O(x), O(y)) -> O(+(x, y)),
+(O(x), I(y)) -> I(+(x, y)),
+(I(x), O(y)) -> I(+(x, y)),
+(I(x), I(y)) -> O(+(+(x, y), I(0()))),
*(x, 0()) -> 0(),
*(0(), x) -> 0(),
*(O(x), y) -> O(*(x, y)),
*(I(x), y) -> +(O(*(x, y)), y),
-(x, 0()) -> x,
-(0(), x) -> 0(),
-(O(x), O(y)) -> O(-(x, y)),
-(O(x), I(y)) -> I(-(-(x, y), I(1()))),
-(I(x), O(y)) -> I(-(x, y)),
-(I(x), I(y)) -> O(-(x, y))}
SPSC:
Simple Projection:
pi(+#) = 0
Strict:
{}
Qed