YES(?,O(n^1))

Problem:
 app(id(),x) -> x
 app(plus(),0()) -> id()
 app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {5}
   transitions:
    id1() -> 5*
    app0(3,1) -> 5*
    app0(3,3) -> 5*
    app0(4,2) -> 5*
    app0(4,4) -> 5*
    app0(1,2) -> 5*
    app0(1,4) -> 5*
    app0(2,1) -> 5*
    app0(2,3) -> 5*
    app0(3,2) -> 5*
    app0(3,4) -> 5*
    app0(4,1) -> 5*
    app0(4,3) -> 5*
    app0(1,1) -> 5*
    app0(1,3) -> 5*
    app0(2,2) -> 5*
    app0(2,4) -> 5*
    id0() -> 1*
    plus0() -> 2*
    00() -> 3*
    s0() -> 4*
    1 -> 5*
    2 -> 5*
    3 -> 5*
    4 -> 5*
  problem:
   
  Qed