YES TRS: {f(c(s(x), y)) -> f(c(x, s(y))), g(c(x, s(y))) -> g(c(s(x), y))} DP: Strict: {f#(c(s(x), y)) -> f#(c(x, s(y))), g#(c(x, s(y))) -> g#(c(s(x), y))} Weak: {f(c(s(x), y)) -> f(c(x, s(y))), g(c(x, s(y))) -> g(c(s(x), y))} EDG: {(g#(c(x, s(y))) -> g#(c(s(x), y)), g#(c(x, s(y))) -> g#(c(s(x), y))) (f#(c(s(x), y)) -> f#(c(x, s(y))), f#(c(s(x), y)) -> f#(c(x, s(y))))} SCCS: Scc: {g#(c(x, s(y))) -> g#(c(s(x), y))} Scc: {f#(c(s(x), y)) -> f#(c(x, s(y)))} SCC: Strict: {g#(c(x, s(y))) -> g#(c(s(x), y))} Weak: {f(c(s(x), y)) -> f(c(x, s(y))), g(c(x, s(y))) -> g(c(s(x), y))} POLY: Argument Filtering: pi(g#) = 0, pi(g) = [], pi(s) = [0], pi(c) = 1, pi(f) = [] Usable Rules: {} Interpretation: [s](x0) = x0 + 1 Strict: {} Weak: {f(c(s(x), y)) -> f(c(x, s(y))), g(c(x, s(y))) -> g(c(s(x), y))} Qed SCC: Strict: {f#(c(s(x), y)) -> f#(c(x, s(y)))} Weak: {f(c(s(x), y)) -> f(c(x, s(y))), g(c(x, s(y))) -> g(c(s(x), y))} POLY: Argument Filtering: pi(g) = [], pi(s) = [0], pi(c) = 0, pi(f#) = 0, pi(f) = [] Usable Rules: {} Interpretation: [s](x0) = x0 + 1 Strict: {} Weak: {f(c(s(x), y)) -> f(c(x, s(y))), g(c(x, s(y))) -> g(c(s(x), y))} Qed