YES(?,O(n^1))

Problem:
 app(app(plus(),0()),y) -> y
 app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
 app(app(app(curry(),f),x),y) -> app(app(f,x),y)
 add() -> app(curry(),plus())

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {6,5}
   transitions:
    app1(8,7) -> 6*
    curry1() -> 8*
    plus1() -> 7*
    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*
    plus0() -> 1*
    00() -> 2*
    s0() -> 3*
    curry0() -> 4*
    add0() -> 6*
  problem:
   
  Qed