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