YES
O(n)
TRS:
 {   f(X, X) -> c(X),
  f(X, c(X)) -> f(s(X), X),
  f(s(X), X) -> f(X, a(X))}
 DUP: We consider a non-duplicating system.
  Trs:
   {   f(X, X) -> c(X),
    f(X, c(X)) -> f(s(X), X),
    f(s(X), X) -> f(X, a(X))}
  BOUND:
   Automaton:
    {
         c_3(14) -> 4,
         c_3(12) -> 4,
         c_3(11) -> 4,
         c_2(14) -> 4,
         c_2(12) -> 4,
         c_2(11) -> 4,
          c_2(8) -> 4,
          c_2(7) -> 4,
         c_1(14) -> 4,
         c_1(12) -> 4,
         c_1(11) -> 4,
          c_1(8) -> 4,
          c_1(7) -> 4,
          c_1(4) -> 4,
         c_0(14) -> 4,
         c_0(12) -> 4,
         c_0(11) -> 4,
          c_0(8) -> 4,
          c_0(7) -> 4,
          c_0(4) -> 4,
         s_2(12) -> 12 | 10 | 8 | 6 | 4,
          s_2(8) -> 12 | 10 | 8 | 6 | 4,
         s_1(14) -> 8 | 6 | 4,
         s_1(12) -> 8 | 6 | 4,
         s_1(11) -> 8 | 6 | 4,
          s_1(8) -> 8 | 6 | 4,
          s_1(7) -> 8 | 6 | 4,
          s_1(4) -> 8 | 6 | 4,
         s_0(14) -> 4,
         s_0(12) -> 4,
         s_0(11) -> 4,
          s_0(8) -> 4,
          s_0(7) -> 4,
          s_0(4) -> 4,
         a_3(12) -> 14 | 13 | 11 | 9 | 7 | 5 | 4,
          a_3(8) -> 14 | 13 | 11 | 9 | 7 | 5 | 4,
         a_2(14) -> 11 | 9 | 7 | 5 | 4,
         a_2(12) -> 11 | 9 | 7 | 5 | 4,
         a_2(11) -> 11 | 9 | 7 | 5 | 4,
          a_2(8) -> 11 | 9 | 7 | 5 | 4,
          a_2(7) -> 11 | 9 | 7 | 5 | 4,
          a_2(4) -> 11 | 9 | 7 | 5 | 4,
         a_1(14) -> 7 | 5 | 4,
         a_1(12) -> 7 | 5 | 4,
         a_1(11) -> 7 | 5 | 4,
          a_1(8) -> 7 | 5 | 4,
          a_1(7) -> 7 | 5 | 4,
          a_1(4) -> 7 | 5 | 4,
         a_0(14) -> 4,
         a_0(12) -> 4,
         a_0(11) -> 4,
          a_0(8) -> 4,
          a_0(7) -> 4,
          a_0(4) -> 4,
     f_3(12, 14) -> 4,
     f_3(12, 13) -> 4,
      f_3(8, 14) -> 4,
      f_3(8, 13) -> 4,
     f_2(14, 14) -> 4,
     f_2(14, 11) -> 4,
      f_2(14, 9) -> 4,
     f_2(12, 14) -> 4,
     f_2(12, 12) -> 4,
     f_2(12, 11) -> 4,
      f_2(12, 9) -> 4,
      f_2(12, 8) -> 4,
     f_2(11, 14) -> 4,
     f_2(11, 11) -> 4,
      f_2(11, 9) -> 4,
     f_2(10, 12) -> 4,
      f_2(10, 8) -> 4,
      f_2(8, 14) -> 4,
      f_2(8, 11) -> 4,
       f_2(8, 9) -> 4,
      f_2(7, 14) -> 4,
      f_2(7, 11) -> 4,
       f_2(7, 9) -> 4,
      f_2(4, 14) -> 4,
      f_2(4, 11) -> 4,
       f_2(4, 9) -> 4,
     f_1(14, 14) -> 4,
     f_1(14, 11) -> 4,
      f_1(14, 7) -> 4,
      f_1(14, 5) -> 4,
     f_1(12, 14) -> 4,
     f_1(12, 12) -> 4,
     f_1(12, 11) -> 4,
      f_1(12, 8) -> 4,
      f_1(12, 7) -> 4,
      f_1(12, 5) -> 4,
      f_1(12, 4) -> 4,
     f_1(11, 14) -> 4,
     f_1(11, 11) -> 4,
      f_1(11, 7) -> 4,
      f_1(11, 5) -> 4,
      f_1(8, 14) -> 4,
      f_1(8, 12) -> 4,
      f_1(8, 11) -> 4,
       f_1(8, 8) -> 4,
       f_1(8, 7) -> 4,
       f_1(8, 5) -> 4,
       f_1(8, 4) -> 4,
      f_1(7, 14) -> 4,
      f_1(7, 11) -> 4,
       f_1(7, 7) -> 4,
       f_1(7, 5) -> 4,
      f_1(6, 14) -> 4,
      f_1(6, 12) -> 4,
      f_1(6, 11) -> 4,
       f_1(6, 8) -> 4,
       f_1(6, 7) -> 4,
       f_1(6, 4) -> 4,
      f_1(4, 14) -> 4,
      f_1(4, 11) -> 4,
       f_1(4, 7) -> 4,
       f_1(4, 5) -> 4,
     f_0(14, 14) -> 4,
     f_0(14, 12) -> 4,
     f_0(14, 11) -> 4,
      f_0(14, 8) -> 4,
      f_0(14, 7) -> 4,
      f_0(14, 4) -> 4,
     f_0(12, 14) -> 4,
     f_0(12, 12) -> 4,
     f_0(12, 11) -> 4,
      f_0(12, 8) -> 4,
      f_0(12, 7) -> 4,
      f_0(12, 4) -> 4,
     f_0(11, 14) -> 4,
     f_0(11, 12) -> 4,
     f_0(11, 11) -> 4,
      f_0(11, 8) -> 4,
      f_0(11, 7) -> 4,
      f_0(11, 4) -> 4,
      f_0(8, 14) -> 4,
      f_0(8, 12) -> 4,
      f_0(8, 11) -> 4,
       f_0(8, 8) -> 4,
       f_0(8, 7) -> 4,
       f_0(8, 4) -> 4,
      f_0(7, 14) -> 4,
      f_0(7, 12) -> 4,
      f_0(7, 11) -> 4,
       f_0(7, 8) -> 4,
       f_0(7, 7) -> 4,
       f_0(7, 4) -> 4,
      f_0(4, 14) -> 4,
      f_0(4, 12) -> 4,
      f_0(4, 11) -> 4,
       f_0(4, 8) -> 4,
       f_0(4, 7) -> 4,
       f_0(4, 4) -> 4
    }
   Strict:
    {}
   Qed