YES TRS: { *(x, x) -> x, *(x, *(y, z)) -> *(*(x, y), z)} DP: Strict: {*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z)} Weak: { *(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: Scc: {*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z)} SCC: 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: Scc: {*#(x, *(y, z)) -> *#(*(x, y), z)} SCC: Strict: {*#(x, *(y, z)) -> *#(*(x, y), z)} Weak: { *(x, x) -> x, *(x, *(y, z)) -> *(*(x, y), z)} SPSC: Simple Projection: pi(*#) = 1 Strict: {} Qed