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