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:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,5}
   transitions:
    p1(4,5,5) -> 4*
    p1(5,4,5) -> 4*
    p1(4,4,4) -> 4*
    p1(5,5,4) -> 4*
    p1(4,4,5) -> 4*
    p1(5,5,5) -> 4*
    p1(4,5,4) -> 4*
    p1(5,4,4) -> 4*
    01() -> 4*
    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:
   
  Qed