YES
Time: 0.001635
TRS:
 {   ++(x, nil()) -> x,
  ++(++(x, y), z) -> ++(x, ++(y, z)),
     ++(nil(), y) -> y,
   ++(.(x, y), z) -> .(x, ++(y, z))}
 RUF:
  Strict:
   {++(++(x, y), z) -> ++(x, ++(y, z)),
     ++(.(x, y), z) -> .(x, ++(y, z))}
  Weak:
   {}
  DP:
   DP:
    {++#(++(x, y), z) -> ++#(y, z),
     ++#(++(x, y), z) -> ++#(x, ++(y, z)),
      ++#(.(x, y), z) -> ++#(y, z)}
   TRS:
   {++(++(x, y), z) -> ++(x, ++(y, z)),
     ++(.(x, y), z) -> .(x, ++(y, z))}
   EDG:
    {(++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(.(x, y), z) -> ++#(y, z))
     (++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
     (++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(y, z))
     (++#(.(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z))
     (++#(.(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
     (++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))
     (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z))
     (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
     (++#(++(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))}
    SCCS (1):
     Scc:
      {++#(++(x, y), z) -> ++#(y, z),
       ++#(++(x, y), z) -> ++#(x, ++(y, z)),
        ++#(.(x, y), z) -> ++#(y, z)}
     SCC (3):
      Strict:
       {++#(++(x, y), z) -> ++#(y, z),
        ++#(++(x, y), z) -> ++#(x, ++(y, z)),
         ++#(.(x, y), z) -> ++#(y, z)}
      Weak:
      {++(++(x, y), z) -> ++(x, ++(y, z)),
        ++(.(x, y), z) -> .(x, ++(y, z))}
      SPSC:
       Simple Projection:
        pi(++#) = 0
       Strict:
        {++#(++(x, y), z) -> ++#(y, z),
          ++#(.(x, y), z) -> ++#(y, z)}
       EDG:
        {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))
         (++#(.(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z))
         (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z))
         (++#(++(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))}
        SCCS (1):
         Scc:
          {++#(++(x, y), z) -> ++#(y, z),
            ++#(.(x, y), z) -> ++#(y, z)}
         SCC (2):
          Strict:
           {++#(++(x, y), z) -> ++#(y, z),
             ++#(.(x, y), z) -> ++#(y, z)}
          Weak:
          {++(++(x, y), z) -> ++(x, ++(y, z)),
            ++(.(x, y), z) -> .(x, ++(y, z))}
          SPSC:
           Simple Projection:
            pi(++#) = 0
           Strict:
            {++#(.(x, y), z) -> ++#(y, z)}
           EDG:
            {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))}
            SCCS (1):
             Scc:
              {++#(.(x, y), z) -> ++#(y, z)}
             SCC (1):
              Strict:
               {++#(.(x, y), z) -> ++#(y, z)}
              Weak:
              {++(++(x, y), z) -> ++(x, ++(y, z)),
                ++(.(x, y), z) -> .(x, ++(y, z))}
              SPSC:
               Simple Projection:
                pi(++#) = 0
               Strict:
                {}
               Qed