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()) EDG Processor: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: g(x,a(),b()) -> g(b(),b(),a()) graph: Qed