YES Time: 0.131270 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: DP: {+#(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)} 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)} 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, 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())) (*#(I x, y) -> +#(O *(x, y), y), +#(O x, O y) -> O# +(x, y)) (*#(I x, y) -> +#(O *(x, y), y), +#(O 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), +#(I x, O 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, I y) -> +#(x, y)) (*#(I x, y) -> +#(O *(x, y), y), +#(I x, I y) -> +#(+(x, y), I 0()))} SCCS (3): 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 (5): 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = 0, [*](x0, x1) = 0, [-](x0, x1) = 0, [O](x0) = x0, [I](x0) = x0 + 1, [0] = 0, [1] = 0, [-#](x0, x1) = x0 Strict: -#(I x, I y) -> -#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y -#(I x, O y) -> -#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y -#(O x, I y) -> -#(-(x, y), I 1()) 1 + 0x + 1y >= 1 + 0x + 0y -#(O x, I y) -> -#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y -#(O x, O y) -> -#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y Weak: EDG: {(-#(I x, O y) -> -#(x, y), -#(I x, O y) -> -#(x, y)) (-#(I x, O y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1())) (-#(I x, O y) -> -#(x, y), -#(O x, O y) -> -#(x, y)) (-#(O x, I y) -> -#(-(x, y), I 1()), -#(O x, I y) -> -#(-(x, y), I 1())) (-#(O x, O y) -> -#(x, y), -#(O x, O 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))} SCCS (2): Scc: {-#(O x, I y) -> -#(-(x, y), I 1())} Scc: {-#(O x, O y) -> -#(x, y), -#(I x, O y) -> -#(x, y)} SCC (1): Strict: {-#(O x, I y) -> -#(-(x, y), I 1())} 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [*](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0, [O](x0) = x0 + 1, [I](x0) = x0 + 1, [0] = 1, [1] = 1, [-#](x0, x1) = x0 Strict: -#(O x, I y) -> -#(-(x, y), I 1()) 1 + 1x + 0y >= 0 + 1x + 0y Weak: Qed SCC (2): 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(-#) = 1 Strict: {-#(O x, O y) -> -#(x, y)} EDG: {(-#(O x, O y) -> -#(x, y), -#(O x, O y) -> -#(x, y))} SCCS (1): Scc: {-#(O x, O y) -> -#(x, y)} SCC (1): 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(-#) = 1 Strict: {} Qed SCC (2): 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: {*#(I x, y) -> *#(x, y)} EDG: {(*#(I x, y) -> *#(x, y), *#(I x, y) -> *#(x, y))} SCCS (1): Scc: {*#(I x, y) -> *#(x, y)} SCC (1): Strict: {*#(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: {} Qed SCC (5): 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1, [*](x0, x1) = 0, [-](x0, x1) = x0 + 1, [O](x0) = x0, [I](x0) = x0 + 1, [0] = 0, [1] = 1, [+#](x0, x1) = x0 + x1 Strict: +#(I x, I y) -> +#(+(x, y), I 0()) 2 + 1x + 1y >= 1 + 1x + 1y +#(I x, I y) -> +#(x, y) 2 + 1x + 1y >= 0 + 1x + 1y +#(I x, O y) -> +#(x, y) 1 + 1x + 1y >= 0 + 1x + 1y +#(O x, I y) -> +#(x, y) 1 + 1x + 1y >= 0 + 1x + 1y +#(O x, O y) -> +#(x, y) 0 + 1x + 1y >= 0 + 1x + 1y Weak: EDG: {(+#(O x, O y) -> +#(x, y), +#(O x, O y) -> +#(x, y))} SCCS (1): Scc: {+#(O x, O y) -> +#(x, y)} SCC (1): 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(+#) = 1 Strict: {} Qed