YES Time: 0.003055 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))} 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))} 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))} SPSC: Simple Projection: pi(*#) = 1 Strict: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} 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, y)) (*#(x, oplus(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(otimes(x, y), z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(y, z), *#(x, oplus(y, z)) -> *#(x, y)) (*#(+(x, y), z) -> *#(y, z), *#(x, *(y, z)) -> *#(otimes(x, y), z)) (*#(+(x, y), z) -> *#(x, z), *#(x, *(y, z)) -> *#(otimes(x, y), z)) (*#(+(x, y), z) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, y)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, 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))} SCCS (1): Scc: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} SCC (4): Strict: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y), *#(+(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))} SPSC: Simple Projection: pi(*#) = 1 Strict: {*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} EDG: {(*#(+(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, y)) (*#(+(x, y), z) -> *#(y, z), *#(x, oplus(y, z)) -> *#(x, y)) (*#(+(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, y), *#(x, oplus(y, z)) -> *#(x, y)) (*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z)) (*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(y, z))} SCCS (1): Scc: {*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} SCC (3): Strict: {*#(x, oplus(y, z)) -> *#(x, y), *#(+(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))} SPSC: Simple Projection: pi(*#) = 1 Strict: {*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} EDG: {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z))} SCCS (1): Scc: {*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} SCC (2): Strict: {*#(+(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))} SPSC: Simple Projection: pi(*#) = 0 Strict: {*#(+(x, y), z) -> *#(y, z)} EDG: {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))} SCCS (1): Scc: {*#(+(x, y), z) -> *#(y, z)} SCC (1): Strict: {*#(+(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))} SPSC: Simple Projection: pi(*#) = 0 Strict: {} Qed