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