YES
Time: 0.045057
TRS:
 {   ++(x, nil()) -> x,
  ++(++(x, y), z) -> ++(x, ++(y, z)),
     ++(nil(), y) -> y,
   ++(.(x, y), z) -> .(x, ++(y, z))}
 DP:
  DP:
   {++#(++(x, y), z) -> ++#(y, z),
    ++#(++(x, y), z) -> ++#(x, ++(y, z)),
     ++#(.(x, y), z) -> ++#(y, z)}
  TRS:
  {   ++(x, nil()) -> x,
   ++(++(x, y), z) -> ++(x, ++(y, z)),
      ++(nil(), y) -> y,
    ++(.(x, y), z) -> .(x, ++(y, z))}
  UR:
   {   ++(x, nil()) -> x,
    ++(++(x, y), z) -> ++(x, ++(y, z)),
       ++(nil(), y) -> y,
     ++(.(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))}
    STATUS:
     arrows: 0.000000
     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, nil()) -> x,
        ++(++(x, y), z) -> ++(x, ++(y, z)),
           ++(nil(), y) -> y,
         ++(.(x, y), z) -> .(x, ++(y, z))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [++](x0, x1) = x0 + x1 + 1,
         
         [.](x0, x1) = x0,
         
         [nil] = 1,
         
         [++#](x0, x1) = x0 + x1
        Strict:
         ++#(.(x, y), z) -> ++#(y, z)
         0 + 1y + 0x + 1z >= 0 + 1y + 1z
         ++#(++(x, y), z) -> ++#(x, ++(y, z))
         1 + 1y + 1x + 1z >= 1 + 1y + 1x + 1z
         ++#(++(x, y), z) -> ++#(y, z)
         1 + 1y + 1x + 1z >= 0 + 1y + 1z
        Weak:
         ++(.(x, y), z) -> .(x, ++(y, z))
         1 + 1y + 0x + 1z >= 1 + 1y + 0x + 1z
         ++(nil(), y) -> y
         2 + 1y >= 1y
         ++(++(x, y), z) -> ++(x, ++(y, z))
         2 + 1y + 1x + 1z >= 2 + 1y + 1x + 1z
         ++(x, nil()) -> x
         2 + 1x >= 1x
       SCCS (1):
        Scc:
         {++#(++(x, y), z) -> ++#(x, ++(y, z)),
           ++#(.(x, y), z) -> ++#(y, z)}
        
        SCC (2):
         Strict:
          {++#(++(x, y), z) -> ++#(x, ++(y, z)),
            ++#(.(x, y), z) -> ++#(y, z)}
         Weak:
         {   ++(x, nil()) -> x,
          ++(++(x, y), z) -> ++(x, ++(y, z)),
             ++(nil(), y) -> y,
           ++(.(x, y), z) -> .(x, ++(y, z))}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [++](x0, x1) = x0 + x1 + 1,
           
           [.](x0, x1) = x0,
           
           [nil] = 1,
           
           [++#](x0, x1) = x0
          Strict:
           ++#(.(x, y), z) -> ++#(y, z)
           0 + 1y + 0x + 0z >= 0 + 1y + 0z
           ++#(++(x, y), z) -> ++#(x, ++(y, z))
           1 + 1y + 1x + 0z >= 0 + 0y + 1x + 0z
          Weak:
           ++(.(x, y), z) -> .(x, ++(y, z))
           1 + 1y + 0x + 1z >= 1 + 1y + 0x + 1z
           ++(nil(), y) -> y
           2 + 1y >= 1y
           ++(++(x, y), z) -> ++(x, ++(y, z))
           2 + 1y + 1x + 1z >= 2 + 1y + 1x + 1z
           ++(x, nil()) -> x
           2 + 1x >= 1x
         SCCS (1):
          Scc:
           {++#(.(x, y), z) -> ++#(y, z)}
          
          SCC (1):
           Strict:
            {++#(.(x, y), z) -> ++#(y, z)}
           Weak:
           {   ++(x, nil()) -> x,
            ++(++(x, y), z) -> ++(x, ++(y, z)),
               ++(nil(), y) -> y,
             ++(.(x, y), z) -> .(x, ++(y, z))}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [++](x0, x1) = x0 + x1 + 1,
             
             [.](x0, x1) = x0 + 1,
             
             [nil] = 1,
             
             [++#](x0, x1) = x0
            Strict:
             ++#(.(x, y), z) -> ++#(y, z)
             1 + 1y + 0x + 0z >= 0 + 1y + 0z
            Weak:
             ++(.(x, y), z) -> .(x, ++(y, z))
             2 + 1y + 0x + 1z >= 2 + 1y + 0x + 1z
             ++(nil(), y) -> y
             2 + 1y >= 1y
             ++(++(x, y), z) -> ++(x, ++(y, z))
             2 + 1y + 1x + 1z >= 2 + 1y + 1x + 1z
             ++(x, nil()) -> x
             2 + 1x >= 1x
           Qed