YES(?,O(n^1))

Problem:
 a(lambda(x),y) -> lambda(a(x,1()))
 a(lambda(x),y) -> lambda(a(x,a(y,t())))
 a(a(x,y),z) -> a(x,a(y,z))
 lambda(x) -> x
 a(x,y) -> x
 a(x,y) -> y

Proof:
 Bounds Processor:
  bound: 0
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    a0(1,2) -> 3*
    a0(2,1) -> 3*
    a0(1,1) -> 3*
    a0(2,2) -> 3*
    lambda0(2) -> 4*
    lambda0(1) -> 4*
    10() -> 1*
    t0() -> 2*
    1 -> 3,4
    2 -> 3,4
  problem:
   
  Qed