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