YES Time: 0.000359 TRS: {f(s X, Y) -> h s f(h Y, X)} DP: DP: {f#(s X, Y) -> f#(h Y, X)} TRS: {f(s X, Y) -> h s f(h Y, X)} EDG: {} SCCS (0): Qed