YES(?,O(n^1))

Problem:
 p(0()) -> 0()
 p(s(x)) -> x
 minus(x,0()) -> x
 minus(x,s(y)) -> minus(p(x),y)

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    minus1(6,2) -> 4*
    minus1(6,1) -> 4*
    p1(2) -> 6*
    p1(6) -> 6*
    p1(1) -> 6*
    01() -> 6,3
    02() -> 6,4
    p0(2) -> 3*
    p0(1) -> 3*
    00() -> 1*
    s0(2) -> 2*
    s0(1) -> 2*
    minus0(1,2) -> 4*
    minus0(2,1) -> 4*
    minus0(1,1) -> 4*
    minus0(2,2) -> 4*
    1 -> 6,4,3
    2 -> 6,4,3
    6 -> 4*
  problem:
   
  Qed