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