YES
Trs:
 {      a(x, y) -> b(x, b(0(), c(y))),
  c(b(y, c(x))) -> c(c(b(a(0(), 0()), y))),
      b(y, 0()) -> y}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {a_2(q11, q11) -> q21,
       a_1(q5, q5) -> q8,
       a_0(q4, q4) -> q4,
          c_3(q11) -> q28,
          c_2(q23) -> q10,
          c_2(q22) -> q23,
           c_2(q5) -> q12,
          c_1(q20) -> q9,
          c_1(q10) -> q6 | q4,
           c_1(q9) -> q10,
           c_1(q4) -> q6,
           c_0(q4) -> q4,
             0_3() -> q27,
             0_2() -> q11,
             0_1() -> q5,
             0_0() -> q4,
     b_3(q27, q28) -> q29,
     b_3(q11, q29) -> q21,
      b_2(q21, q8) -> q22,
     b_2(q11, q12) -> q13,
      b_2(q5, q13) -> q8,
       b_1(q8, q8) -> q20,
       b_1(q8, q4) -> q9,
       b_1(q5, q6) -> q7,
       b_1(q4, q7) -> q4,
       b_0(q4, q4) -> q4,
                q8 -> q9}
   Strict:
   {}
   Qed