YES

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

Proof:
 WPO Processor:
  algebra: MSum
  weight function:
   w0 = 0
   w(lambda) = 4
   w(id) = w(p) = w(t) = w(1) = w(a) = 0
  status function:
   st(id) = []
   st(p) = [0, 1]
   st(t) = st(1) = []
   st(a) = [0, 1]
   st(lambda) = [0]
  subterm penalty function:
   sp(p, 1) = sp(p, 0) = sp(a, 1) = sp(a, 0) = sp(lambda, 0) = 0
  subterm coefficient function:
   sc(p, 1) = sc(p, 0) = sc(a, 1) = sc(a, 0) = sc(lambda, 0) = 1
  weight status function:
   ws(t) = ws(a) = ws(lambda) = pol
   ws(id) = ws(p) = ws(1) = max
  precedence:
   a > id ~ p ~ t ~ 1 ~ lambda
  problem:
   
  Qed