YES
O(n)
TRS:
 {
      b(y, 0()) -> y,
  c(b(y, c(x))) -> c(c(b(a(0(), 0()), y))),
        a(x, y) -> b(x, b(0(), c(y)))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
        b(y, 0()) -> y,
    c(b(y, c(x))) -> c(c(b(a(0(), 0()), y))),
          a(x, y) -> b(x, b(0(), c(y)))
   }
  BOUND:
   Automaton:
    {
     a_2(11, 11) -> 21,
       a_1(5, 5) -> 8,
       a_0(4, 4) -> 4,
         c_3(11) -> 28,
         c_2(23) -> 10,
         c_2(22) -> 23,
          c_2(5) -> 12,
         c_1(20) -> 9,
         c_1(10) -> 6 | 4,
          c_1(9) -> 10,
          c_1(4) -> 6,
          c_0(4) -> 4,
           0_3() -> 27,
           0_2() -> 11,
           0_1() -> 5,
           0_0() -> 4,
     b_3(27, 28) -> 29,
     b_3(11, 29) -> 21,
      b_2(21, 8) -> 22,
     b_2(11, 12) -> 13,
      b_2(5, 13) -> 8,
       b_1(8, 8) -> 20,
       b_1(8, 4) -> 9,
       b_1(5, 6) -> 7,
       b_1(4, 7) -> 4,
       b_0(4, 4) -> 4,
               8 -> 9
    }
   Strict:
    {}
   Qed