YES TRS: {f(x, g(x)) -> x, f(x, h(y)) -> f(h(x), y)} RUF: Strict: {f(x, h(y)) -> f(h(x), y)} Weak: {} DP: Strict: {f#(x, h(y)) -> f#(h(x), y)} Weak: {f(x, h(y)) -> f(h(x), y)} EDG: {(f#(x, h(y)) -> f#(h(x), y), f#(x, h(y)) -> f#(h(x), y))} SCCS: Scc: {f#(x, h(y)) -> f#(h(x), y)} SCC: Strict: {f#(x, h(y)) -> f#(h(x), y)} Weak: {f(x, h(y)) -> f(h(x), y)} SPSC: Simple Projection: pi(f#) = 1 Strict: {} Qed