YES(?,O(n^1))

Problem:
 p(m,n,s(r)) -> p(m,r,n)
 p(m,s(n),0()) -> p(0(),n,m)
 p(m,0(),0()) -> m

Proof:
 Complexity Transformation Processor:
  strict:
   p(m,n,s(r)) -> p(m,r,n)
   p(m,s(n),0()) -> p(0(),n,m)
   p(m,0(),0()) -> m
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [0] = 0,
     
     [p](x0, x1, x2) = x0 + x1 + x2 + 1,
     
     [s](x0) = x0
    orientation:
     p(m,n,s(r)) = m + n + r + 1 >= m + n + r + 1 = p(m,r,n)
     
     p(m,s(n),0()) = m + n + 1 >= m + n + 1 = p(0(),n,m)
     
     p(m,0(),0()) = m + 1 >= m = m
    problem:
     strict:
      p(m,n,s(r)) -> p(m,r,n)
      p(m,s(n),0()) -> p(0(),n,m)
     weak:
      p(m,0(),0()) -> m
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [0] = 0,
       
       [p](x0, x1, x2) = x0 + x1 + x2,
       
       [s](x0) = x0 + 1
      orientation:
       p(m,n,s(r)) = m + n + r + 1 >= m + n + r = p(m,r,n)
       
       p(m,s(n),0()) = m + n + 1 >= m + n = p(0(),n,m)
       
       p(m,0(),0()) = m >= m = m
      problem:
       strict:
        
       weak:
        p(m,n,s(r)) -> p(m,r,n)
        p(m,s(n),0()) -> p(0(),n,m)
        p(m,0(),0()) -> m
      Qed