YES Time: 0.020503 TRS: { *(x, *(y, z)) -> *(otimes(x, y), z), *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)), *(1(), y) -> y, *(+(x, y), z) -> oplus(*(x, z), *(y, z))} DP: DP: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} TRS: { *(x, *(y, z)) -> *(otimes(x, y), z), *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)), *(1(), y) -> y, *(+(x, y), z) -> oplus(*(x, z), *(y, z))} UR: {} EDG: {(*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(y, z)) (*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z)) (*#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z)) (*#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, y)) (*#(x, oplus(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(otimes(x, y), z)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, z)) (*#(+(x, y), z) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, y)) (*#(+(x, y), z) -> *#(x, z), *#(x, *(y, z)) -> *#(otimes(x, y), z)) (*#(+(x, y), z) -> *#(y, z), *#(x, *(y, z)) -> *#(otimes(x, y), z)) (*#(+(x, y), z) -> *#(y, z), *#(x, oplus(y, z)) -> *#(x, y)) (*#(+(x, y), z) -> *#(y, z), *#(x, oplus(y, z)) -> *#(x, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z)) (*#(x, oplus(y, z)) -> *#(x, z), *#(x, *(y, z)) -> *#(otimes(x, y), z)) (*#(x, oplus(y, z)) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, y)) (*#(x, oplus(y, z)) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, z)) (*#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)) (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, *(y, z)) -> *#(otimes(x, y), z)) (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y)) (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, z))} STATUS: arrows: 0.080000 SCCS (1): Scc: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} SCC (5): Strict: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} Weak: { *(x, *(y, z)) -> *(otimes(x, y), z), *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)), *(1(), y) -> y, *(+(x, y), z) -> oplus(*(x, z), *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [*](x0, x1) = x0 + 1, [otimes](x0, x1) = 0, [oplus](x0, x1) = 1, [+](x0, x1) = x0 + x1 + 1, [1] = 0, [*#](x0, x1) = x0 Strict: *#(+(x, y), z) -> *#(y, z) 1 + 1x + 1y + 0z >= 0 + 1y + 0z *#(+(x, y), z) -> *#(x, z) 1 + 1x + 1y + 0z >= 0 + 1x + 0z *#(x, oplus(y, z)) -> *#(x, z) 0 + 1x + 0y + 0z >= 0 + 1x + 0z *#(x, oplus(y, z)) -> *#(x, y) 0 + 1x + 0y + 0z >= 0 + 1x + 0y *#(x, *(y, z)) -> *#(otimes(x, y), z) 0 + 1x + 0y + 0z >= 0 + 0x + 0y + 0z Weak: *(+(x, y), z) -> oplus(*(x, z), *(y, z)) 1 + 0x + 0y + 1z >= 1 + 0x + 0y + 0z *(1(), y) -> y 1 + 1y >= 1y *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)) 2 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z *(x, *(y, z)) -> *(otimes(x, y), z) 2 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z SCCS (1): Scc: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z)} SCC (3): Strict: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z)} Weak: { *(x, *(y, z)) -> *(otimes(x, y), z), *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)), *(1(), y) -> y, *(+(x, y), z) -> oplus(*(x, z), *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [*](x0, x1) = x0 + 1, [otimes](x0, x1) = 0, [oplus](x0, x1) = x0 + x1, [+](x0, x1) = 0, [1] = 0, [*#](x0, x1) = x0 + x1 Strict: *#(x, oplus(y, z)) -> *#(x, z) 0 + 1x + 1y + 1z >= 0 + 1x + 1z *#(x, oplus(y, z)) -> *#(x, y) 0 + 1x + 1y + 1z >= 0 + 1x + 1y *#(x, *(y, z)) -> *#(otimes(x, y), z) 1 + 1x + 0y + 1z >= 0 + 0x + 0y + 1z Weak: *(+(x, y), z) -> oplus(*(x, z), *(y, z)) 1 + 0x + 0y + 1z >= 2 + 0x + 0y + 2z *(1(), y) -> y 1 + 1y >= 1y *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)) 1 + 0x + 1y + 1z >= 2 + 0x + 1y + 1z *(x, *(y, z)) -> *(otimes(x, y), z) 2 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z SCCS (1): Scc: {*#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z)} SCC (2): Strict: {*#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z)} Weak: { *(x, *(y, z)) -> *(otimes(x, y), z), *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)), *(1(), y) -> y, *(+(x, y), z) -> oplus(*(x, z), *(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [*](x0, x1) = 0, [otimes](x0, x1) = 0, [oplus](x0, x1) = x0 + x1 + 1, [+](x0, x1) = 0, [1] = 0, [*#](x0, x1) = x0 Strict: *#(x, oplus(y, z)) -> *#(x, z) 1 + 0x + 1y + 1z >= 0 + 0x + 1z *#(x, oplus(y, z)) -> *#(x, y) 1 + 0x + 1y + 1z >= 0 + 0x + 1y Weak: *(+(x, y), z) -> oplus(*(x, z), *(y, z)) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z *(1(), y) -> y 0 + 0y >= 1y *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z *(x, *(y, z)) -> *(otimes(x, y), z) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z Qed