YES
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:
  Strict:
   {              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)))}
  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)))}
  EDG:
   {(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))))
    (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))), 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))), h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z))))}
   SCCS:
    Scc:
     {              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)))}
    SCC:
     Strict:
      {              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)))}
     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)))}
     UR:
      {}
      BOUND:
       Bound: match(-raise)-DP-bounded by 0
       Automaton:
        {      a_0() -> 2*
               0_0() -> 3*
              s_0(4) -> 7*
              s_0(3) -> 4*
              s_0(2) -> 9*
          c_0(9, 10) -> 10*
           c_0(9, 8) -> 10*
           c_0(9, 2) -> 8*
          c_0(7, 10) -> 8*
           c_0(7, 8) -> 8*
           c_0(7, 2) -> 8*
           c_0(4, 6) -> 6*
           c_0(4, 5) -> 6*
           c_0(2, 6) -> 6*
           c_0(2, 5) -> 6*
           c_0(2, 2) -> 5*
         h#_0(10, 6) -> 1*
         h#_0(10, 5) -> 1*
         h#_0(10, 2) -> 1*
          h#_0(8, 6) -> 1*
          h#_0(8, 5) -> 1*
          h#_0(2, 6) -> 1*}
       Strict:
        {h#(x, c(y, z)) -> h#(c(s(y), x), z)}
       EDG:
        {(h#(x, c(y, z)) -> h#(c(s(y), x), z), h#(x, c(y, z)) -> h#(c(s(y), x), z))}
        SCCS:
         Scc:
          {h#(x, c(y, z)) -> h#(c(s(y), x), z)}
         SCC:
          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)))}
          SPSC:
           Simple Projection:
            pi(h#) = 1
           Strict:
            {}
           Qed