YES Problem: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) -(0(),y) -> 0() -(x,0()) -> x -(s(x),s(y)) -> -(x,y) Proof: Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1 0 0] [0] [-](x0, x1) = [0 1 0]x0 + [0 0 0]x1 + [1] [1 0 1] [0 0 0] [0], [0] [s](x0) = x0 + [0] [1], [1 0 1] [1 1 1] [+](x0, x1) = [1 1 1]x0 + [1 1 1]x1 [1 0 1] [1 1 1] , [1] [0] = [0] [0] orientation: [1 1 1] [1] +(0(),y) = [1 1 1]y + [1] >= y = y [1 1 1] [1] [1 0 1] [1 1 1] [1] [1 0 1] [1 1 1] [0] +(s(x),y) = [1 1 1]x + [1 1 1]y + [1] >= [1 1 1]x + [1 1 1]y + [0] = s(+(x,y)) [1 0 1] [1 1 1] [1] [1 0 1] [1 1 1] [1] [1 0 0] [1] [1] -(0(),y) = [0 0 0]y + [1] >= [0] = 0() [0 0 0] [1] [0] [1 0 0] [1] -(x,0()) = [0 1 0]x + [1] >= x = x [1 0 1] [0] [1 0 0] [1 0 0] [0] [1 0 0] [1 0 0] [0] -(s(x),s(y)) = [0 1 0]x + [0 0 0]y + [1] >= [0 1 0]x + [0 0 0]y + [1] = -(x,y) [1 0 1] [0 0 0] [1] [1 0 1] [0 0 0] [0] problem: -(0(),y) -> 0() -(s(x),s(y)) -> -(x,y) Matrix Interpretation Processor: dim=3 interpretation: [1 0 1] [1 1 0] [-](x0, x1) = [1 0 0]x0 + [0 0 0]x1 [0 0 1] [0 0 0] , [0] [s](x0) = x0 + [1] [0], [0] [0] = [0] [1] orientation: [1 1 0] [1] [0] -(0(),y) = [0 0 0]y + [0] >= [0] = 0() [0 0 0] [1] [1] [1 0 1] [1 1 0] [1] [1 0 1] [1 1 0] -(s(x),s(y)) = [1 0 0]x + [0 0 0]y + [0] >= [1 0 0]x + [0 0 0]y = -(x,y) [0 0 1] [0 0 0] [0] [0 0 1] [0 0 0] problem: Qed