YES
TRS:
 {      lambda(x) -> x,
          a(x, y) -> x,
          a(x, y) -> y,
  a(lambda(x), y) -> lambda(a(x, a(y, t()))),
  a(lambda(x), y) -> lambda(a(x, 1())),
    a(a(x, y), z) -> a(x, a(y, z))}
 DP:
  Strict:
   {a#(lambda(x), y) -> lambda#(a(x, a(y, t()))),
    a#(lambda(x), y) -> lambda#(a(x, 1())),
    a#(lambda(x), y) -> a#(x, a(y, t())),
    a#(lambda(x), y) -> a#(x, 1()),
    a#(lambda(x), y) -> a#(y, t()),
      a#(a(x, y), z) -> a#(x, a(y, z)),
      a#(a(x, y), z) -> a#(y, z)}
  Weak:
  {      lambda(x) -> x,
           a(x, y) -> x,
           a(x, y) -> y,
   a(lambda(x), y) -> lambda(a(x, a(y, t()))),
   a(lambda(x), y) -> lambda(a(x, 1())),
     a(a(x, y), z) -> a(x, a(y, z))}
  EDG:
   {(a#(lambda(x), y) -> a#(x, 1()), a#(a(x, y), z) -> a#(y, z))
    (a#(lambda(x), y) -> a#(x, 1()), a#(a(x, y), z) -> a#(x, a(y, z)))
    (a#(lambda(x), y) -> a#(x, 1()), a#(lambda(x), y) -> a#(y, t()))
    (a#(lambda(x), y) -> a#(x, 1()), a#(lambda(x), y) -> a#(x, 1()))
    (a#(lambda(x), y) -> a#(x, 1()), a#(lambda(x), y) -> a#(x, a(y, t())))
    (a#(lambda(x), y) -> a#(x, 1()), a#(lambda(x), y) -> lambda#(a(x, 1())))
    (a#(lambda(x), y) -> a#(x, 1()), a#(lambda(x), y) -> lambda#(a(x, a(y, t()))))
    (a#(lambda(x), y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(y, z))
    (a#(lambda(x), y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(x, a(y, z)))
    (a#(lambda(x), y) -> a#(x, a(y, t())), a#(lambda(x), y) -> a#(y, t()))
    (a#(lambda(x), y) -> a#(x, a(y, t())), a#(lambda(x), y) -> a#(x, 1()))
    (a#(lambda(x), y) -> a#(x, a(y, t())), a#(lambda(x), y) -> a#(x, a(y, t())))
    (a#(lambda(x), y) -> a#(x, a(y, t())), a#(lambda(x), y) -> lambda#(a(x, 1())))
    (a#(lambda(x), y) -> a#(x, a(y, t())), a#(lambda(x), y) -> lambda#(a(x, a(y, t()))))
    (a#(a(x, y), z) -> a#(y, z), a#(lambda(x), y) -> lambda#(a(x, a(y, t()))))
    (a#(a(x, y), z) -> a#(y, z), a#(lambda(x), y) -> lambda#(a(x, 1())))
    (a#(a(x, y), z) -> a#(y, z), a#(lambda(x), y) -> a#(x, a(y, t())))
    (a#(a(x, y), z) -> a#(y, z), a#(lambda(x), y) -> a#(x, 1()))
    (a#(a(x, y), z) -> a#(y, z), a#(lambda(x), y) -> a#(y, t()))
    (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(x, a(y, z)))
    (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(y, z))
    (a#(lambda(x), y) -> a#(y, t()), a#(lambda(x), y) -> lambda#(a(x, a(y, t()))))
    (a#(lambda(x), y) -> a#(y, t()), a#(lambda(x), y) -> lambda#(a(x, 1())))
    (a#(lambda(x), y) -> a#(y, t()), a#(lambda(x), y) -> a#(x, a(y, t())))
    (a#(lambda(x), y) -> a#(y, t()), a#(lambda(x), y) -> a#(x, 1()))
    (a#(lambda(x), y) -> a#(y, t()), a#(lambda(x), y) -> a#(y, t()))
    (a#(lambda(x), y) -> a#(y, t()), a#(a(x, y), z) -> a#(x, a(y, z)))
    (a#(lambda(x), y) -> a#(y, t()), a#(a(x, y), z) -> a#(y, z))
    (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda(x), y) -> lambda#(a(x, a(y, t()))))
    (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda(x), y) -> lambda#(a(x, 1())))
    (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda(x), y) -> a#(x, a(y, t())))
    (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda(x), y) -> a#(x, 1()))
    (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda(x), y) -> a#(y, t()))
    (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(x, a(y, z)))
    (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z))}
   SCCS:
    Scc:
     {a#(lambda(x), y) -> a#(x, a(y, t())),
      a#(lambda(x), y) -> a#(x, 1()),
      a#(lambda(x), y) -> a#(y, t()),
        a#(a(x, y), z) -> a#(x, a(y, z)),
        a#(a(x, y), z) -> a#(y, z)}
    SCC:
     Strict:
      {a#(lambda(x), y) -> a#(x, a(y, t())),
       a#(lambda(x), y) -> a#(x, 1()),
       a#(lambda(x), y) -> a#(y, t()),
         a#(a(x, y), z) -> a#(x, a(y, z)),
         a#(a(x, y), z) -> a#(y, z)}
     Weak:
     {      lambda(x) -> x,
              a(x, y) -> x,
              a(x, y) -> y,
      a(lambda(x), y) -> lambda(a(x, a(y, t()))),
      a(lambda(x), y) -> lambda(a(x, 1())),
        a(a(x, y), z) -> a(x, a(y, z))}
     POLY:
      Argument Filtering:
       pi(t) = [], pi(1) = [], pi(a#) = [0,1], pi(a) = [0,1], pi(lambda) = [0]
      Usable Rules:
       {}
      Interpretation:
       [a#](x0, x1) = x0 + x1,
       [a](x0, x1) = x0 + x1,
       [lambda](x0) = x0 + 1,
       [t] = 0,
       [1] = 0
      Strict:
       {a#(a(x, y), z) -> a#(x, a(y, z)),
        a#(a(x, y), z) -> a#(y, z)}
      Weak:
       {      lambda(x) -> x,
                a(x, y) -> x,
                a(x, y) -> y,
        a(lambda(x), y) -> lambda(a(x, a(y, t()))),
        a(lambda(x), y) -> lambda(a(x, 1())),
          a(a(x, y), z) -> a(x, a(y, z))}
      EDG:
       {(a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(y, z))
        (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(x, a(y, z)))
        (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(x, a(y, z)))
        (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z))}
       SCCS:
        Scc:
         {a#(a(x, y), z) -> a#(x, a(y, z)),
          a#(a(x, y), z) -> a#(y, z)}
        SCC:
         Strict:
          {a#(a(x, y), z) -> a#(x, a(y, z)),
           a#(a(x, y), z) -> a#(y, z)}
         Weak:
         {      lambda(x) -> x,
                  a(x, y) -> x,
                  a(x, y) -> y,
          a(lambda(x), y) -> lambda(a(x, a(y, t()))),
          a(lambda(x), y) -> lambda(a(x, 1())),
            a(a(x, y), z) -> a(x, a(y, z))}
         SPSC:
          Simple Projection:
           pi(a#) = 0
          Strict:
           {a#(a(x, y), z) -> a#(y, z)}
          EDG:
           {(a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(y, z))}
           SCCS:
            Scc:
             {a#(a(x, y), z) -> a#(y, z)}
            SCC:
             Strict:
              {a#(a(x, y), z) -> a#(y, z)}
             Weak:
             {      lambda(x) -> x,
                      a(x, y) -> x,
                      a(x, y) -> y,
              a(lambda(x), y) -> lambda(a(x, a(y, t()))),
              a(lambda(x), y) -> lambda(a(x, 1())),
                a(a(x, y), z) -> a(x, a(y, z))}
             SPSC:
              Simple Projection:
               pi(a#) = 0
              Strict:
               {}
              Qed