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