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