YES Problem: a(a(x)) -> a(b(a(x))) Proof: DP Processor: DPs: a#(a(x)) -> a#(b(a(x))) TRS: a(a(x)) -> a(b(a(x))) EDG Processor: DPs: a#(a(x)) -> a#(b(a(x))) TRS: a(a(x)) -> a(b(a(x))) graph: Qed