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