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