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