YES Time: 0.000764 TRS: {f(g(x, y), f(y, y)) -> f(g(y, x), y)} DP: DP: {f#(g(x, y), f(y, y)) -> f#(g(y, x), y)} TRS: {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 (1): Scc: {f#(g(x, y), f(y, y)) -> f#(g(y, x), y)} SCC (1): 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