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