YES
Time: 0.024273
TRS:
 {            h(x, c(y, z)) -> h(c(s y, x), z),
  h(c(s x, c(s 0(), y)), z) -> h(y, c(s 0(), c(x, z)))}
 DP:
  DP:
   {            h#(x, c(y, z)) -> h#(c(s y, x), z),
    h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z)))}
  TRS:
  {            h(x, c(y, z)) -> h(c(s y, x), z),
   h(c(s x, c(s 0(), y)), z) -> h(y, c(s 0(), c(x, z)))}
  UR:
   {}
   EDG:
    {(h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))), h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))))
     (h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))), h#(x, c(y, z)) -> h#(c(s y, x), z))
     (h#(x, c(y, z)) -> h#(c(s y, x), z), h#(x, c(y, z)) -> h#(c(s y, x), z))
     (h#(x, c(y, z)) -> h#(c(s y, x), z), h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))))}
    EDG:
     {(h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))), h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))))
      (h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))), h#(x, c(y, z)) -> h#(c(s y, x), z))
      (h#(x, c(y, z)) -> h#(c(s y, x), z), h#(x, c(y, z)) -> h#(c(s y, x), z))
      (h#(x, c(y, z)) -> h#(c(s y, x), z), h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))))}
     EDG:
      {(h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))), h#(x, c(y, z)) -> h#(c(s y, x), z))
       (h#(x, c(y, z)) -> h#(c(s y, x), z), h#(x, c(y, z)) -> h#(c(s y, x), z))}
      EDG:
       {(h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))), h#(x, c(y, z)) -> h#(c(s y, x), z))
        (h#(x, c(y, z)) -> h#(c(s y, x), z), h#(x, c(y, z)) -> h#(c(s y, x), z))}
       STATUS:
        arrows: 0.500000
        SCCS (1):
         Scc:
          {h#(x, c(y, z)) -> h#(c(s y, x), z)}
         
         
         SCC (1):
          Strict:
           {h#(x, c(y, z)) -> h#(c(s y, x), z)}
          Weak:
          {            h(x, c(y, z)) -> h(c(s y, x), z),
           h(c(s x, c(s 0(), y)), z) -> h(y, c(s 0(), c(x, z)))}
          POLY:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [h](x0, x1) = 0,
            
            [c](x0, x1) = x0 + 1,
            
            [s](x0) = 0,
            
            [0] = 0,
            
            [h#](x0, x1) = x0
           Strict:
            h#(x, c(y, z)) -> h#(c(s y, x), z)
            1 + 0y + 0x + 1z >= 0 + 0y + 0x + 1z
           Weak:
            h(c(s x, c(s 0(), y)), z) -> h(y, c(s 0(), c(x, z)))
            0 + 0y + 0x + 0z >= 0 + 0y + 0x + 0z
            h(x, c(y, z)) -> h(c(s y, x), z)
            0 + 0y + 0x + 0z >= 0 + 0y + 0x + 0z
          Qed