YES TRS: { p(s(x)) -> x, s(p(x)) -> x, +(p(x), y) -> p(+(x, y)), +(s(x), y) -> s(+(x, y)), +(0(), y) -> y, minus(p(x)) -> s(minus(x)), minus(s(x)) -> p(minus(x)), minus(0()) -> 0(), *(p(x), y) -> +(*(x, y), minus(y)), *(s(x), y) -> +(*(x, y), y), *(0(), y) -> 0()} DP: Strict: { +#(p(x), y) -> p#(+(x, y)), +#(p(x), y) -> +#(x, y), +#(s(x), y) -> s#(+(x, y)), +#(s(x), y) -> +#(x, y), minus#(p(x)) -> s#(minus(x)), minus#(p(x)) -> minus#(x), minus#(s(x)) -> p#(minus(x)), minus#(s(x)) -> minus#(x), *#(p(x), y) -> +#(*(x, y), minus(y)), *#(p(x), y) -> minus#(y), *#(p(x), y) -> *#(x, y), *#(s(x), y) -> +#(*(x, y), y), *#(s(x), y) -> *#(x, y)} Weak: { p(s(x)) -> x, s(p(x)) -> x, +(p(x), y) -> p(+(x, y)), +(s(x), y) -> s(+(x, y)), +(0(), y) -> y, minus(p(x)) -> s(minus(x)), minus(s(x)) -> p(minus(x)), minus(0()) -> 0(), *(p(x), y) -> +(*(x, y), minus(y)), *(s(x), y) -> +(*(x, y), y), *(0(), y) -> 0()} EDG: {(minus#(p(x)) -> minus#(x), minus#(s(x)) -> minus#(x)) (minus#(p(x)) -> minus#(x), minus#(s(x)) -> p#(minus(x))) (minus#(p(x)) -> minus#(x), minus#(p(x)) -> minus#(x)) (minus#(p(x)) -> minus#(x), minus#(p(x)) -> s#(minus(x))) (*#(p(x), y) -> minus#(y), minus#(s(x)) -> minus#(x)) (*#(p(x), y) -> minus#(y), minus#(s(x)) -> p#(minus(x))) (*#(p(x), y) -> minus#(y), minus#(p(x)) -> minus#(x)) (*#(p(x), y) -> minus#(y), minus#(p(x)) -> s#(minus(x))) (+#(p(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y)) (+#(p(x), y) -> +#(x, y), +#(s(x), y) -> s#(+(x, y))) (+#(p(x), y) -> +#(x, y), +#(p(x), y) -> +#(x, y)) (+#(p(x), y) -> +#(x, y), +#(p(x), y) -> p#(+(x, y))) (*#(p(x), y) -> *#(x, y), *#(s(x), y) -> *#(x, y)) (*#(p(x), y) -> *#(x, y), *#(s(x), y) -> +#(*(x, y), y)) (*#(p(x), y) -> *#(x, y), *#(p(x), y) -> *#(x, y)) (*#(p(x), y) -> *#(x, y), *#(p(x), y) -> minus#(y)) (*#(p(x), y) -> *#(x, y), *#(p(x), y) -> +#(*(x, y), minus(y))) (*#(s(x), y) -> *#(x, y), *#(p(x), y) -> +#(*(x, y), minus(y))) (*#(s(x), y) -> *#(x, y), *#(p(x), y) -> minus#(y)) (*#(s(x), y) -> *#(x, y), *#(p(x), y) -> *#(x, y)) (*#(s(x), y) -> *#(x, y), *#(s(x), y) -> +#(*(x, y), y)) (*#(s(x), y) -> *#(x, y), *#(s(x), y) -> *#(x, y)) (+#(s(x), y) -> +#(x, y), +#(p(x), y) -> p#(+(x, y))) (+#(s(x), y) -> +#(x, y), +#(p(x), y) -> +#(x, y)) (+#(s(x), y) -> +#(x, y), +#(s(x), y) -> s#(+(x, y))) (+#(s(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y)) (*#(p(x), y) -> +#(*(x, y), minus(y)), +#(p(x), y) -> p#(+(x, y))) (*#(p(x), y) -> +#(*(x, y), minus(y)), +#(p(x), y) -> +#(x, y)) (*#(p(x), y) -> +#(*(x, y), minus(y)), +#(s(x), y) -> s#(+(x, y))) (*#(p(x), y) -> +#(*(x, y), minus(y)), +#(s(x), y) -> +#(x, y)) (minus#(s(x)) -> minus#(x), minus#(p(x)) -> s#(minus(x))) (minus#(s(x)) -> minus#(x), minus#(p(x)) -> minus#(x)) (minus#(s(x)) -> minus#(x), minus#(s(x)) -> p#(minus(x))) (minus#(s(x)) -> minus#(x), minus#(s(x)) -> minus#(x)) (*#(s(x), y) -> +#(*(x, y), y), +#(p(x), y) -> p#(+(x, y))) (*#(s(x), y) -> +#(*(x, y), y), +#(p(x), y) -> +#(x, y)) (*#(s(x), y) -> +#(*(x, y), y), +#(s(x), y) -> s#(+(x, y))) (*#(s(x), y) -> +#(*(x, y), y), +#(s(x), y) -> +#(x, y))} SCCS: Scc: {*#(p(x), y) -> *#(x, y), *#(s(x), y) -> *#(x, y)} Scc: {minus#(p(x)) -> minus#(x), minus#(s(x)) -> minus#(x)} Scc: {+#(p(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y)} SCC: Strict: {*#(p(x), y) -> *#(x, y), *#(s(x), y) -> *#(x, y)} Weak: { p(s(x)) -> x, s(p(x)) -> x, +(p(x), y) -> p(+(x, y)), +(s(x), y) -> s(+(x, y)), +(0(), y) -> y, minus(p(x)) -> s(minus(x)), minus(s(x)) -> p(minus(x)), minus(0()) -> 0(), *(p(x), y) -> +(*(x, y), minus(y)), *(s(x), y) -> +(*(x, y), y), *(0(), y) -> 0()} SPSC: Simple Projection: pi(*#) = 0 Strict: {*#(p(x), y) -> *#(x, y)} EDG: {(*#(p(x), y) -> *#(x, y), *#(p(x), y) -> *#(x, y))} SCCS: Scc: {*#(p(x), y) -> *#(x, y)} SCC: Strict: {*#(p(x), y) -> *#(x, y)} Weak: { p(s(x)) -> x, s(p(x)) -> x, +(p(x), y) -> p(+(x, y)), +(s(x), y) -> s(+(x, y)), +(0(), y) -> y, minus(p(x)) -> s(minus(x)), minus(s(x)) -> p(minus(x)), minus(0()) -> 0(), *(p(x), y) -> +(*(x, y), minus(y)), *(s(x), y) -> +(*(x, y), y), *(0(), y) -> 0()} SPSC: Simple Projection: pi(*#) = 0 Strict: {} Qed SCC: Strict: {minus#(p(x)) -> minus#(x), minus#(s(x)) -> minus#(x)} Weak: { p(s(x)) -> x, s(p(x)) -> x, +(p(x), y) -> p(+(x, y)), +(s(x), y) -> s(+(x, y)), +(0(), y) -> y, minus(p(x)) -> s(minus(x)), minus(s(x)) -> p(minus(x)), minus(0()) -> 0(), *(p(x), y) -> +(*(x, y), minus(y)), *(s(x), y) -> +(*(x, y), y), *(0(), y) -> 0()} SPSC: Simple Projection: pi(minus#) = 0 Strict: {minus#(s(x)) -> minus#(x)} EDG: {(minus#(s(x)) -> minus#(x), minus#(s(x)) -> minus#(x))} SCCS: Scc: {minus#(s(x)) -> minus#(x)} SCC: Strict: {minus#(s(x)) -> minus#(x)} Weak: { p(s(x)) -> x, s(p(x)) -> x, +(p(x), y) -> p(+(x, y)), +(s(x), y) -> s(+(x, y)), +(0(), y) -> y, minus(p(x)) -> s(minus(x)), minus(s(x)) -> p(minus(x)), minus(0()) -> 0(), *(p(x), y) -> +(*(x, y), minus(y)), *(s(x), y) -> +(*(x, y), y), *(0(), y) -> 0()} SPSC: Simple Projection: pi(minus#) = 0 Strict: {} Qed SCC: Strict: {+#(p(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y)} Weak: { p(s(x)) -> x, s(p(x)) -> x, +(p(x), y) -> p(+(x, y)), +(s(x), y) -> s(+(x, y)), +(0(), y) -> y, minus(p(x)) -> s(minus(x)), minus(s(x)) -> p(minus(x)), minus(0()) -> 0(), *(p(x), y) -> +(*(x, y), minus(y)), *(s(x), y) -> +(*(x, y), y), *(0(), y) -> 0()} SPSC: Simple Projection: pi(+#) = 0 Strict: {+#(p(x), y) -> +#(x, y)} EDG: {(+#(p(x), y) -> +#(x, y), +#(p(x), y) -> +#(x, y))} SCCS: Scc: {+#(p(x), y) -> +#(x, y)} SCC: Strict: {+#(p(x), y) -> +#(x, y)} Weak: { p(s(x)) -> x, s(p(x)) -> x, +(p(x), y) -> p(+(x, y)), +(s(x), y) -> s(+(x, y)), +(0(), y) -> y, minus(p(x)) -> s(minus(x)), minus(s(x)) -> p(minus(x)), minus(0()) -> 0(), *(p(x), y) -> +(*(x, y), minus(y)), *(s(x), y) -> +(*(x, y), y), *(0(), y) -> 0()} SPSC: Simple Projection: pi(+#) = 0 Strict: {} Qed