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