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