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