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: {5,6}
   transitions:
    minus1(7,5) -> 5*
    p1(5) -> 7*
    01() -> 5*
    02() -> 7*
    p0(5) -> 5*
    p0(6) -> 5*
    00() -> 5*
    s0(5) -> 6*
    s0(6) -> 6*
    minus0(5,5) -> 5*
    minus0(6,6) -> 5*
    minus0(5,6) -> 5*
    minus0(6,5) -> 5*
    5 -> 7*
    6 -> 5*
    7 -> 5*
  problem:
   
  Qed