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