YES Problem: f(a(),f(b(),f(a(),x))) -> f(a(),f(b(),f(b(),f(a(),x)))) f(b(),f(b(),f(b(),x))) -> f(b(),f(b(),x)) Proof: DP Processor: DPs: f#(a(),f(b(),f(a(),x))) -> f#(b(),f(b(),f(a(),x))) f#(a(),f(b(),f(a(),x))) -> f#(a(),f(b(),f(b(),f(a(),x)))) TRS: f(a(),f(b(),f(a(),x))) -> f(a(),f(b(),f(b(),f(a(),x)))) f(b(),f(b(),f(b(),x))) -> f(b(),f(b(),x)) Matrix Interpretation Processor: dim=2 usable rules: f(a(),f(b(),f(a(),x))) -> f(a(),f(b(),f(b(),f(a(),x)))) f(b(),f(b(),f(b(),x))) -> f(b(),f(b(),x)) interpretation: [f#](x0, x1) = [0 2]x0 + [2 0]x1, [0 0] [0 1] [f](x0, x1) = [1 0]x0 + [0 0]x1, [0] [b] = [0], [1] [a] = [2] orientation: f#(a(),f(b(),f(a(),x))) = [6] >= [2] = f#(b(),f(b(),f(a(),x))) f#(a(),f(b(),f(a(),x))) = [6] >= [4] = f#(a(),f(b(),f(b(),f(a(),x)))) [0] [0] f(a(),f(b(),f(a(),x))) = [1] >= [1] = f(a(),f(b(),f(b(),f(a(),x)))) [0] [0] f(b(),f(b(),f(b(),x))) = [0] >= [0] = f(b(),f(b(),x)) problem: DPs: TRS: f(a(),f(b(),f(a(),x))) -> f(a(),f(b(),f(b(),f(a(),x)))) f(b(),f(b(),f(b(),x))) -> f(b(),f(b(),x)) Qed