YES TRS: {f(s(x), y, y) -> f(y, x, s(x))} DP: Strict: {f#(s(x), y, y) -> f#(y, x, s(x))} Weak: {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: {f(s(x), y, y) -> f(y, x, s(x))} POLY: Argument Filtering: pi(s) = [0], pi(f#) = [0,1], pi(f) = [] Usable Rules: {} Interpretation: [f#](x0, x1) = x0 + x1, [s](x0) = x0 + 1 Strict: {} Weak: {f(s(x), y, y) -> f(y, x, s(x))} Qed