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