YES
O(n)
TRS:
 {
   f(a(), a()) -> f(a(), b()),
   f(a(), b()) -> f(s(a()), c()),
  f(s(X), c()) -> f(X, c()),
   f(c(), c()) -> f(a(), a())
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
     f(a(), a()) -> f(a(), b()),
     f(a(), b()) -> f(s(a()), c()),
    f(s(X), c()) -> f(X, c()),
     f(c(), c()) -> f(a(), a())
   }
  BOUND:
   Automaton:
    {
           c_4() -> 15,
           c_3() -> 10,
           c_2() -> 8,
           c_1() -> 6,
           c_0() -> 5,
         s_3(11) -> 5,
          s_2(5) -> 5,
          s_1(5) -> 5,
          s_0(5) -> 5,
           b_2() -> 8,
           b_1() -> 6,
           b_0() -> 5,
           a_3() -> 11,
           a_2() -> 5,
           a_1() -> 6 | 5,
           a_0() -> 5,
     f_4(11, 15) -> 5,
     f_3(11, 10) -> 5,
      f_3(5, 10) -> 5,
      f_2(11, 8) -> 5,
       f_2(5, 8) -> 5,
      f_1(11, 6) -> 5,
       f_1(5, 6) -> 5,
       f_0(5, 5) -> 5
    }
   Strict:
    {}
   Qed