YES Problem: f(x,y,w,w,a()) -> g1(x,x,y,w) f(x,y,w,a(),a()) -> g1(y,x,x,w) f(x,y,a(),a(),w) -> g2(x,y,y,w) f(x,y,a(),w,w) -> g2(y,y,x,w) g1(x,x,y,a()) -> h(x,y) g1(y,x,x,a()) -> h(x,y) g2(x,y,y,a()) -> h(x,y) g2(y,y,x,a()) -> h(x,y) h(x,x) -> x Proof: Matrix Interpretation Processor: dim=1 interpretation: [h](x0, x1) = x0 + x1 + 6, [g2](x0, x1, x2, x3) = x0 + 2x1 + x2 + 2x3, [g1](x0, x1, x2, x3) = 2x0 + x1 + 2x2 + 2x3, [f](x0, x1, x2, x3, x4) = 3x0 + 4x1 + 2x2 + x3 + 2x4 + 7, [a] = 3 orientation: f(x,y,w,w,a()) = 3w + 3x + 4y + 13 >= 2w + 3x + 2y = g1(x,x,y,w) f(x,y,w,a(),a()) = 2w + 3x + 4y + 16 >= 2w + 3x + 2y = g1(y,x,x,w) f(x,y,a(),a(),w) = 2w + 3x + 4y + 16 >= 2w + x + 3y = g2(x,y,y,w) f(x,y,a(),w,w) = 3w + 3x + 4y + 13 >= 2w + x + 3y = g2(y,y,x,w) g1(x,x,y,a()) = 3x + 2y + 6 >= x + y + 6 = h(x,y) g1(y,x,x,a()) = 3x + 2y + 6 >= x + y + 6 = h(x,y) g2(x,y,y,a()) = x + 3y + 6 >= x + y + 6 = h(x,y) g2(y,y,x,a()) = x + 3y + 6 >= x + y + 6 = h(x,y) h(x,x) = 2x + 6 >= x = x problem: g1(x,x,y,a()) -> h(x,y) g1(y,x,x,a()) -> h(x,y) g2(x,y,y,a()) -> h(x,y) g2(y,y,x,a()) -> h(x,y) Matrix Interpretation Processor: dim=1 interpretation: [h](x0, x1) = 2x0 + x1 + 2, [g2](x0, x1, x2, x3) = 4x0 + 5x1 + 2x2 + 4x3 + 3, [g1](x0, x1, x2, x3) = 2x0 + x1 + x2 + x3, [a] = 2 orientation: g1(x,x,y,a()) = 3x + y + 2 >= 2x + y + 2 = h(x,y) g1(y,x,x,a()) = 2x + 2y + 2 >= 2x + y + 2 = h(x,y) g2(x,y,y,a()) = 4x + 7y + 11 >= 2x + y + 2 = h(x,y) g2(y,y,x,a()) = 2x + 9y + 11 >= 2x + y + 2 = h(x,y) problem: g1(x,x,y,a()) -> h(x,y) g1(y,x,x,a()) -> h(x,y) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1 0 0] [h](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [1 0 0] [1 0 0] [1 0 0] [1 0 1] [1] [g1](x0, x1, x2, x3) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0], [0] [a] = [0] [1] orientation: [2 0 0] [1 0 0] [2] [1 0 0] [1 0 0] g1(x,x,y,a()) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y = h(x,y) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [2 0 0] [1 0 0] [2] [1 0 0] [1 0 0] g1(y,x,x,a()) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y = h(x,y) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] problem: Qed