YES
Time: 0.002525
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)))}
    STATUS:
     arrows: 0.500000
     SCCS (1):
      Scc:
       {.#(.(x, y), z) -> .#(y, z)}
      
      SCC (1):
       Strict:
        {.#(.(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 + 1,
         
         [.#](x0, x1) = x0
        Strict:
         .#(.(x, y), z) -> .#(y, z)
         1 + 0x + 1y + 0z >= 0 + 1y + 0z
        Weak:
         .(.(x, y), z) -> .(x, .(y, z))
         1 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z
       Qed