YES(?,O(n^2))

Problem:
 not(true()) -> false()
 not(false()) -> true()
 odd(0()) -> false()
 odd(s(x)) -> not(odd(x))
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 +(s(x),y) -> s(+(x,y))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                 [1 1]     [1 1]     [4]
   [+](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
   
                  [0]
   [s](x0) = x0 + [1],
   
               [1 8]     [1]
   [odd](x0) = [0 0]x0 + [2],
   
         [0]
   [0] = [0],
   
             [0]
   [false] = [0],
   
               [1 0]     [7]
   [not](x0) = [0 0]x0 + [2],
   
            [0]
   [true] = [2]
  orientation:
                 [7]    [0]          
   not(true()) = [2] >= [0] = false()
   
                  [7]    [0]         
   not(false()) = [2] >= [2] = true()
   
              [1]    [0]          
   odd(0()) = [2] >= [0] = false()
   
               [1 8]    [9]    [1 8]    [8]              
   odd(s(x)) = [0 0]x + [2] >= [0 0]x + [2] = not(odd(x))
   
              [1 1]    [4]         
   +(x,0()) = [0 1]x + [0] >= x = x
   
               [1 1]    [1 1]    [5]    [1 1]    [1 1]    [4]            
   +(x,s(y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = s(+(x,y))
   
               [1 1]    [1 1]    [5]    [1 1]    [1 1]    [4]            
   +(s(x),y) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = s(+(x,y))
  problem:
   
  Qed