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