YES Problem: g(x,a(),b()) -> g(b(),b(),a()) Proof: DP Processor: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: g(x,a(),b()) -> g(b(),b(),a()) Usable Rule Processor: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: CDG Processor: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: graph: Qed