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