YES
Time: 0.032796
TRS:
 {.(.(x, y), z) -> .(x, .(y, z))}
 DP:
  DP:
   {.#(.(x, y), z) -> .#(x, .(y, z)),
    .#(.(x, y), z) -> .#(y, z)}
  TRS:
  {.(.(x, y), z) -> .(x, .(y, z))}
  UR:
   {.(.(x, y), z) -> .(x, .(y, z))}
   EDG:
    {(.#(.(x, y), z) -> .#(y, z), .#(.(x, y), z) -> .#(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) -> .#(x, .(y, z)), .#(.(x, y), z) -> .#(y, z))}
    STATUS:
     arrows: 0.000000
     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, 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 + x1
        Strict:
         .#(.(x, y), z) -> .#(y, z)
         1 + 1x + 1y + 1z >= 0 + 1y + 1z
         .#(.(x, y), z) -> .#(x, .(y, z))
         1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z
        Weak:
         .(.(x, y), z) -> .(x, .(y, z))
         2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
       SCCS (1):
        Scc:
         {.#(.(x, y), z) -> .#(x, .(y, z))}
        
        SCC (1):
         Strict:
          {.#(.(x, y), z) -> .#(x, .(y, z))}
         Weak:
         {.(.(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
          Strict:
           .#(.(x, y), z) -> .#(x, .(y, z))
           1 + 1x + 1y + 0z >= 0 + 1x + 0y + 0z
          Weak:
           .(.(x, y), z) -> .(x, .(y, z))
           2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
         Qed