YES

Problem:
 minus(0()) -> 0()
 +(x,0()) -> x
 +(0(),y) -> y
 +(minus(1()),1()) -> 0()
 minus(minus(x)) -> x
 +(x,minus(y)) -> minus(+(minus(x),y))
 +(x,+(y,z)) -> +(+(x,y),z)
 +(minus(+(x,1())),1()) -> minus(x)

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [1] = 4,
   
   [+](x0, x1) = x0 + x1 + 3,
   
   [minus](x0) = x0,
   
   [0] = 4
  orientation:
   minus(0()) = 4 >= 4 = 0()
   
   +(x,0()) = x + 7 >= x = x
   
   +(0(),y) = y + 7 >= y = y
   
   +(minus(1()),1()) = 11 >= 4 = 0()
   
   minus(minus(x)) = x >= x = x
   
   +(x,minus(y)) = x + y + 3 >= x + y + 3 = minus(+(minus(x),y))
   
   +(x,+(y,z)) = x + y + z + 6 >= x + y + z + 6 = +(+(x,y),z)
   
   +(minus(+(x,1())),1()) = x + 14 >= x = minus(x)
  problem:
   minus(0()) -> 0()
   minus(minus(x)) -> x
   +(x,minus(y)) -> minus(+(minus(x),y))
   +(x,+(y,z)) -> +(+(x,y),z)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [+](x0, x1) = x0 + 2x1 + 4,
    
    [minus](x0) = x0 + 1,
    
    [0] = 5
   orientation:
    minus(0()) = 6 >= 5 = 0()
    
    minus(minus(x)) = x + 2 >= x = x
    
    +(x,minus(y)) = x + 2y + 6 >= x + 2y + 6 = minus(+(minus(x),y))
    
    +(x,+(y,z)) = x + 2y + 4z + 12 >= x + 2y + 2z + 8 = +(+(x,y),z)
   problem:
    +(x,minus(y)) -> minus(+(minus(x),y))
   Matrix Interpretation Processor: dim=3
    
    interpretation:
                   [1 0 1]     [1 1 0]  
     [+](x0, x1) = [0 0 0]x0 + [0 1 0]x1
                   [0 0 0]     [0 0 0]  ,
     
                   [1 0 1]     [0]
     [minus](x0) = [0 1 0]x0 + [1]
                   [0 0 0]     [0]
    orientation:
                     [1 0 1]    [1 1 1]    [1]    [1 0 1]    [1 1 0]    [0]                       
     +(x,minus(y)) = [0 0 0]x + [0 1 0]y + [1] >= [0 0 0]x + [0 1 0]y + [1] = minus(+(minus(x),y))
                     [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]                       
    problem:
     
    Qed