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:
 RT 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:
   
  Bounds Processor:
   bound: 0
   enrichment: match-rt
   automaton:
    final states: {4,5}
    transitions:
     p0(4,5,5) -> 4*
     p0(5,4,5) -> 4*
     p0(4,4,4) -> 4*
     p0(5,5,4) -> 4*
     p0(4,4,5) -> 4*
     p0(5,5,5) -> 4*
     p0(4,5,4) -> 4*
     p0(5,4,4) -> 4*
     s0(5) -> 5*
     s0(4) -> 5*
     00() -> 4*
     5 -> 4*
   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
    interpretation:
     [0] = 1,
     
     [p](x0, x1, x2) = x0 + x1 + x2 + 7,
     
     [s](x0) = x0 + 1
    orientation:
     p(m,n,s(r)) = m + n + r + 8 >= m + n + r + 7 = p(m,r,n)
     
     p(m,s(n),0()) = m + n + 9 >= m + n + 8 = p(0(),n,m)
     
     p(m,0(),0()) = m + 9 >= 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