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