MAYBE

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:
 RT Transformation Processor:
  strict:
   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)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [1] = 0,
    
    [+](x0, x1) = x0 + x1 + 9,
    
    [minus](x0) = x0 + 23,
    
    [0] = 0
   orientation:
    minus(0()) = 23 >= 0 = 0()
    
    +(x,0()) = x + 9 >= x = x
    
    +(0(),y) = y + 9 >= y = y
    
    +(minus(1()),1()) = 32 >= 0 = 0()
    
    minus(minus(x)) = x + 46 >= x = x
    
    +(x,minus(y)) = x + y + 32 >= x + y + 55 = minus(+(minus(x),y))
    
    +(x,+(y,z)) = x + y + z + 18 >= x + y + z + 18 = +(+(x,y),z)
    
    +(minus(+(x,1())),1()) = x + 41 >= x + 23 = minus(x)
   problem:
    strict:
     +(x,minus(y)) -> minus(+(minus(x),y))
     +(x,+(y,z)) -> +(+(x,y),z)
    weak:
     minus(0()) -> 0()
     +(x,0()) -> x
     +(0(),y) -> y
     +(minus(1()),1()) -> 0()
     minus(minus(x)) -> x
     +(minus(+(x,1())),1()) -> minus(x)
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
           [0]
     [1] = [7],
     
                        [1 2]     [0]
     [+](x0, x1) = x0 + [0 1]x1 + [1],
     
                     
     [minus](x0) = x0,
     
           [0 ]
     [0] = [15]
    orientation:
                         [1 2]    [0]        [1 2]    [0]                       
     +(x,minus(y)) = x + [0 1]y + [1] >= x + [0 1]y + [1] = minus(+(minus(x),y))
     
                       [1 2]    [1 4]    [2]        [1 2]    [1 2]    [0]              
     +(x,+(y,z)) = x + [0 1]y + [0 1]z + [2] >= x + [0 1]y + [0 1]z + [2] = +(+(x,y),z)
     
                  [0 ]    [0 ]      
     minus(0()) = [15] >= [15] = 0()
     
                    [30]         
     +(x,0()) = x + [16] >= x = x
     
                [1 2]    [0 ]         
     +(0(),y) = [0 1]y + [16] >= y = y
     
                         [14]    [0 ]      
     +(minus(1()),1()) = [15] >= [15] = 0()
     
                                 
     minus(minus(x)) = x >= x = x
     
                                  [28]                
     +(minus(+(x,1())),1()) = x + [16] >= x = minus(x)
    problem:
     strict:
      +(x,minus(y)) -> minus(+(minus(x),y))
     weak:
      +(x,+(y,z)) -> +(+(x,y),z)
      minus(0()) -> 0()
      +(x,0()) -> x
      +(0(),y) -> y
      +(minus(1()),1()) -> 0()
      minus(minus(x)) -> x
      +(minus(+(x,1())),1()) -> minus(x)
    Open