YES
Time: 0.100371
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)))}
  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))))}
   SCCS (1):
    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 (2):
     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)))}
     BOUND:
      Bound: match(-raise)-bounded by 2
      Automaton:
       {      0_1() -> 4*
              0_0() -> 1*
             s_2(5) -> 8*
             s_2(1) -> 10*
             s_1(4) -> 5*
             s_1(1) -> 2*
             s_0(1) -> 1*
         c_2(10, 9) -> 11*
         c_2(8, 11) -> 9*
          c_2(8, 9) -> 9*
          c_2(8, 3) -> 9*
          c_2(8, 1) -> 9*
          c_1(5, 7) -> 7*
          c_1(5, 6) -> 7*
         c_1(2, 11) -> 11*
          c_1(2, 3) -> 3*
          c_1(2, 1) -> 3*
          c_1(1, 7) -> 6*
          c_1(1, 1) -> 6*
          c_0(1, 1) -> 1*
        h#_2(11, 7) -> 1*
        h#_2(11, 1) -> 1*
         h#_2(9, 7) -> 1*
         h#_2(9, 6) -> 1*
         h#_1(3, 7) -> 1*
         h#_1(3, 1) -> 1*
         h#_1(1, 7) -> 1*
         h#_0(1, 1) -> 1*
         h_2(11, 7) -> 1*
         h_2(11, 1) -> 1*
          h_2(9, 7) -> 1*
          h_2(9, 6) -> 1*
          h_1(3, 7) -> 1*
          h_1(3, 1) -> 1*
          h_1(1, 7) -> 1*
          h_0(1, 1) -> 1*}
      Strict:
       {}
      Qed