YES
O(n)
TRS:
 {
  b(b(0(), y), x) -> y,
       c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0()))),
        a(y, 0()) -> b(y, 0())
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
    b(b(0(), y), x) -> y,
         c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0()))),
          a(y, 0()) -> b(y, 0())
   }
  BOUND:
   Automaton:
    {
      a_1(8, 5) -> 9,
      a_1(7, 5) -> 8,
      a_0(4, 4) -> 4,
        c_1(10) -> 4,
         c_1(9) -> 10,
         c_1(6) -> 7,
         c_0(4) -> 4,
          0_2() -> 11,
          0_1() -> 5,
          0_0() -> 4,
     b_2(8, 11) -> 9,
     b_2(7, 11) -> 8,
     b_1(5, 10) -> 6,
      b_1(5, 9) -> 6,
      b_1(5, 4) -> 6,
      b_1(4, 5) -> 4,
      b_0(4, 4) -> 4,
              5 -> 4
    }
   Strict:
    {}
   Qed