YES
O(n)
TRS:
 {
                c(y) -> y,
          c(c(c(y))) -> c(c(a(y, 0()))),
  c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                  c(y) -> y,
            c(c(c(y))) -> c(c(a(y, 0()))),
    c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)
   }
  BOUND:
   Automaton:
    {
           0_3() -> 28,
           0_2() -> 16,
           0_1() -> 4,
           0_0() -> 3,
     a_3(16, 28) -> 29,
      a_2(24, 4) -> 6 | 3,
      a_2(4, 16) -> 17,
       a_1(9, 4) -> 6,
       a_1(9, 3) -> 3,
       a_1(3, 4) -> 5,
       a_0(3, 3) -> 3,
         c_3(30) -> 24,
         c_3(29) -> 30,
         c_2(23) -> 24,
         c_2(22) -> 23,
         c_2(18) -> 9,
         c_2(17) -> 18,
         c_2(16) -> 22,
          c_1(8) -> 9,
          c_1(7) -> 8,
          c_1(6) -> 3,
          c_1(5) -> 6,
          c_1(4) -> 7,
          c_0(3) -> 3,
              30 -> 24,
              29 -> 30,
              23 -> 24,
              22 -> 23,
              18 -> 9,
              17 -> 18,
              16 -> 22,
               8 -> 9,
               7 -> 8,
               6 -> 3,
               5 -> 6,
               4 -> 7
    }
   Strict:
    {}
   Qed