YES
Trs:
 {c(a(a(0(), x), y)) -> a(c(c(c(0()))), y),
          c(c(c(y))) -> c(c(a(y, 0()))),
                c(y) -> y}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {        0_3() -> q28,
             0_2() -> q16,
             0_1() -> q4,
             0_0() -> q3,
     a_3(q16, q28) -> q29,
      a_2(q24, q4) -> q6 | q3,
      a_2(q4, q16) -> q17,
       a_1(q9, q4) -> q6,
       a_1(q9, q3) -> q3,
       a_1(q3, q4) -> q5,
       a_0(q3, q3) -> q3,
          c_3(q30) -> q24,
          c_3(q29) -> q30,
          c_2(q23) -> q24,
          c_2(q22) -> q23,
          c_2(q18) -> q9,
          c_2(q17) -> q18,
          c_2(q16) -> q22,
           c_1(q8) -> q9,
           c_1(q7) -> q8,
           c_1(q6) -> q3,
           c_1(q5) -> q6,
           c_1(q4) -> q7,
           c_0(q3) -> q3,
               q30 -> q24,
               q29 -> q30,
               q23 -> q24,
               q22 -> q23,
               q18 -> q9,
               q17 -> q18,
               q16 -> q22,
                q8 -> q9,
                q7 -> q8,
                q6 -> q3,
                q5 -> q6,
                q4 -> q7}
   Strict:
   {}
   Qed