YES
Trs:
 {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)}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {        0_1() -> q9,
             0_0() -> q4,
          s_2(q10) -> q13,
           s_2(q4) -> q15,
           s_1(q9) -> q10,
           s_1(q4) -> q5,
           s_0(q4) -> q4,
     c_2(q15, q14) -> q16,
     c_2(q13, q16) -> q14,
     c_2(q13, q14) -> q14,
      c_2(q13, q6) -> q14,
      c_2(q13, q4) -> q14,
     c_1(q10, q12) -> q12,
     c_1(q10, q11) -> q12,
      c_1(q5, q16) -> q6,
       c_1(q5, q6) -> q6,
       c_1(q5, q4) -> q6,
      c_1(q4, q12) -> q11,
       c_1(q4, q4) -> q11,
       c_0(q4, q4) -> q4,
     h_2(q16, q12) -> q4,
      h_2(q16, q4) -> q4,
     h_2(q14, q12) -> q4,
     h_2(q14, q11) -> q4,
     h_1(q16, q12) -> q4,
     h_1(q14, q12) -> q4,
      h_1(q6, q12) -> q4,
       h_1(q6, q4) -> q4,
      h_1(q4, q12) -> q4,
       h_0(q4, q4) -> q4}
   Strict:
   {}
   Qed