YES 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: 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))} 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, 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)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, z)) (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y)) (*#(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, y), *#(x, oplus(y, z)) -> *#(x, y)) (*#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z)) (*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z)) (*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(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))} SCCS: 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: 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, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} EDG: {(*#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)) (*#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(x, oplus(y, z)) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, z)) (*#(x, oplus(y, z)) -> *#(x, z), *#(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, z)) (*#(+(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, z)) (*#(+(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, z))} SCCS: Scc: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} SCC: Strict: { *#(x, *(y, z)) -> *#(otimes(x, y), z), *#(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, 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, *(y, z)) -> *#(otimes(x, y), z)) (*#(+(x, y), z) -> *#(y, z), *#(x, *(y, z)) -> *#(otimes(x, y), z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z)) (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, *(y, z)) -> *#(otimes(x, y), z))} SCCS: Scc: {*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} Scc: {*#(x, *(y, z)) -> *#(otimes(x, y), z)} SCC: 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: Scc: {*#(+(x, y), z) -> *#(y, z)} SCC: 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 SCC: Strict: {*#(x, *(y, z)) -> *#(otimes(x, 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: {} Qed