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