YES

TRS:

  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

linear polynomial interpretations on N:

  a_A(x1,x2) = x1 + x2
  a#_A(x1,x2) = x1 + x2
  lambda_A(x1) = x1 + 1
  lambda#_A(x1) = x1 + 1
  1_A = 0
  1#_A = 0
  t_A = 0
  t#_A = 0

precedence:

  a > lambda = t > 1