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))) Usable Rule Processor: DPs: f#(s(X),Y) -> f#(h(Y),X) TRS: ADG Processor: DPs: f#(s(X),Y) -> f#(h(Y),X) TRS: graph: Qed