YES Problem: a(b(x)) -> b(b(a(x))) Proof: DP Processor: DPs: a#(b(x)) -> a#(x) TRS: a(b(x)) -> b(b(a(x))) Subterm Criterion Processor: simple projection: pi(a#) = 0 problem: DPs: TRS: a(b(x)) -> b(b(a(x))) Qed