YES
Time: 0.008178
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:
  DP:
   {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)}
  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))}
  EDG:
   {(a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(y, z))
    (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#(lambda x, y) -> 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#(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) -> lambda# a(x, a(y, t())))
    (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#(y, z), a#(lambda x, y) -> 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#(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) -> lambda# a(x, a(y, t())))
    (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# 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) -> a#(x, 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#(y, t()))
    (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#(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))
    (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# 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) -> a#(x, 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#(y, t()))
    (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#(a(x, y), z) -> a#(y, z))}
   SCCS (1):
    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 (5):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [a](x0, x1) = x0 + x1,
       
       [lambda](x0) = x0 + 1,
       
       [1] = 0,
       
       [t] = 0,
       
       [a#](x0, x1) = x0 + x1
      Strict:
       a#(a(x, y), z) -> a#(y, z)
       0 + 1x + 1y + 1z >= 0 + 1y + 1z
       a#(a(x, y), z) -> a#(x, a(y, z))
       0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
       a#(lambda x, y) -> a#(y, t())
       1 + 1x + 1y >= 0 + 1y
       a#(lambda x, y) -> a#(x, 1())
       1 + 1x + 1y >= 0 + 1x
       a#(lambda x, y) -> a#(x, a(y, t()))
       1 + 1x + 1y >= 0 + 1x + 1y
      Weak:
       
     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 (1):
       Scc:
        {a#(a(x, y), z) -> a#(x, a(y, z)),
         a#(a(x, y), z) -> a#(y, z)}
       SCC (2):
        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 (1):
           Scc:
            {a#(a(x, y), z) -> a#(y, z)}
           SCC (1):
            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