YES Problem: f(s(X),Y) -> h(s(f(h(Y),X))) Proof: DP Processor: DPs: f#(s(X),Y) -> f#(h(Y),X) TRS: f(s(X),Y) -> h(s(f(h(Y),X))) EDG Processor: DPs: f#(s(X),Y) -> f#(h(Y),X) TRS: f(s(X),Y) -> h(s(f(h(Y),X))) graph: Qed