YES(?,O(n^2))

Problem:
 add(0(),x) -> x
 add(s(x),y) -> s(add(x,y))

Proof:
 Complexity Transformation Processor:
  strict:
   add(0(),x) -> x
   add(s(x),y) -> s(add(x,y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [s](x0) = x0,
     
     [add](x0, x1) = x0 + x1,
     
     [0] = 1
    orientation:
     add(0(),x) = x + 1 >= x = x
     
     add(s(x),y) = x + y >= x + y = s(add(x,y))
    problem:
     strict:
      add(s(x),y) -> s(add(x,y))
     weak:
      add(0(),x) -> x
    Matrix Interpretation Processor:
     dimension: 2
     max_matrix:
      [1 1]
      [0 1]
      interpretation:
                      [0]
       [s](x0) = x0 + [1],
       
                       [1 1]       
       [add](x0, x1) = [0 1]x0 + x1,
       
             [0]
       [0] = [0]
      orientation:
                     [1 1]        [1]    [1 1]        [0]              
       add(s(x),y) = [0 1]x + y + [1] >= [0 1]x + y + [1] = s(add(x,y))
       
                              
       add(0(),x) = x >= x = x
      problem:
       strict:
        
       weak:
        add(s(x),y) -> s(add(x,y))
        add(0(),x) -> x
      Qed