YES Problem: a(b(b(x1))) -> b(a(a(x1))) a(a(b(x1))) -> b(b(a(x1))) Proof: DP Processor: DPs: a#(b(b(x1))) -> a#(x1) a#(b(b(x1))) -> a#(a(x1)) a#(a(b(x1))) -> a#(x1) TRS: a(b(b(x1))) -> b(a(a(x1))) a(a(b(x1))) -> b(b(a(x1))) KBO Processor: weight function: w0 = 1 w(a#) = w(a) = w(b) = 1 precedence: a# > a > b problem: DPs: TRS: Qed