YES(?,O(n^2))

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

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                      [1 6]     [3]
   [+](x0, x1) = x0 + [0 1]x1 + [4],
   
             [1 4]     [10]
   [i](x0) = [0 1]x0 + [0 ],
   
         [4]
   [0] = [4]
  orientation:
            [30]    [4]      
   i(0()) = [4 ] >= [4] = 0()
   
              [1 6]    [7]         
   +(0(),y) = [0 1]y + [8] >= y = y
   
                  [31]         
   +(x,0()) = x + [8 ] >= x = x
   
             [1 8]    [20]         
   i(i(x)) = [0 1]x + [0 ] >= x = x
   
               [2  10]    [13]    [4]      
   +(i(x),x) = [0  2 ]x + [4 ] >= [4] = 0()
   
               [2  10]    [13]    [4]      
   +(x,i(x)) = [0  2 ]x + [4 ] >= [4] = 0()
   
               [1 4]    [1  10]    [29]    [1 4]    [1  10]    [23]               
   i(+(x,y)) = [0 1]x + [0  1 ]y + [4 ] >= [0 1]x + [0  1 ]y + [4 ] = +(i(x),i(y))
   
                     [1 6]    [1  12]    [30]        [1 6]    [1 6]    [6]              
   +(x,+(y,z)) = x + [0 1]y + [0  1 ]z + [8 ] >= x + [0 1]y + [0 1]z + [8] = +(+(x,y),z)
   
                        [2  16]    [16]         
   +(+(x,i(y)),y) = x + [0  2 ]y + [8 ] >= x = x
   
                        [2  16]    [16]         
   +(+(x,y),i(y)) = x + [0  2 ]y + [8 ] >= x = x
  problem:
   
  Qed