YES Time: 0.000972 TRS: { *(x, x) -> x, *(x, *(y, z)) -> *(*(x, y), z)} DP: DP: {*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z)} TRS: { *(x, x) -> x, *(x, *(y, z)) -> *(*(x, y), z)} EDG: {(*#(x, *(y, z)) -> *#(*(x, y), z), *#(x, *(y, z)) -> *#(*(x, y), z)) (*#(x, *(y, z)) -> *#(*(x, y), z), *#(x, *(y, z)) -> *#(x, y)) (*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(x, y)) (*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z))} SCCS (1): Scc: {*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z)} SCC (2): Strict: {*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z)} Weak: { *(x, x) -> x, *(x, *(y, z)) -> *(*(x, y), z)} SPSC: Simple Projection: pi(*#) = 1 Strict: {*#(x, *(y, z)) -> *#(*(x, y), z)} EDG: {(*#(x, *(y, z)) -> *#(*(x, y), z), *#(x, *(y, z)) -> *#(*(x, y), z))} SCCS (1): Scc: {*#(x, *(y, z)) -> *#(*(x, y), z)} SCC (1): Strict: {*#(x, *(y, z)) -> *#(*(x, y), z)} Weak: { *(x, x) -> x, *(x, *(y, z)) -> *(*(x, y), z)} SPSC: Simple Projection: pi(*#) = 1 Strict: {} Qed