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