YES(?,O(n^1))

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

Proof:
 Complexity Transformation Processor:
  strict:
   +(0(),y) -> y
   +(s(x),0()) -> s(x)
   +(s(x),s(y)) -> s(+(s(x),+(y,0())))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [s](x0) = x0,
     
     [+](x0, x1) = x0 + x1,
     
     [0] = 1
    orientation:
     +(0(),y) = y + 1 >= y = y
     
     +(s(x),0()) = x + 1 >= x = s(x)
     
     +(s(x),s(y)) = x + y >= x + y + 1 = s(+(s(x),+(y,0())))
    problem:
     strict:
      +(s(x),s(y)) -> s(+(s(x),+(y,0())))
     weak:
      +(0(),y) -> y
      +(s(x),0()) -> s(x)
    Bounds Processor:
     bound: 2
     enrichment: match
     automaton:
      final states: {3}
      transitions:
       s1(7) -> 3*
       s1(2) -> 17,7,5,6
       s1(1) -> 17,7,5,6
       +1(1,4) -> 5*
       +1(6,5) -> 7*
       +1(2,4) -> 5*
       01() -> 4*
       s2(2) -> 19,18
       s2(19) -> 19,7
       s2(1) -> 19,18
       +0(1,2) -> 3*
       +0(2,1) -> 3*
       +0(1,1) -> 3*
       +0(2,2) -> 3*
       +2(2,16) -> 17*
       +2(18,17) -> 19*
       +2(1,16) -> 17*
       s0(2) -> 1*
       s0(1) -> 1*
       02() -> 16*
       00() -> 2*
       1 -> 3*
       2 -> 3*
       4 -> 5*
       16 -> 17*
     problem:
      strict:
       
      weak:
       +(s(x),s(y)) -> s(+(s(x),+(y,0())))
       +(0(),y) -> y
       +(s(x),0()) -> s(x)
     Qed