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