YES(?,O(n^1))

Problem:
 f(x1) -> n(c(n(a(x1))))
 c(f(x1)) -> f(n(a(c(x1))))
 n(a(x1)) -> c(x1)
 c(c(x1)) -> c(x1)
 n(s(x1)) -> f(s(s(x1)))
 n(f(x1)) -> f(n(x1))

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {5,4,3}
   transitions:
    f1(30) -> 31*
    s1(29) -> 30*
    s1(38) -> 39*
    s1(28) -> 29*
    c1(20) -> 21*
    c1(26) -> 27*
    c1(8) -> 9*
    n1(7) -> 8*
    n1(9) -> 10*
    a1(6) -> 7*
    a1(18) -> 19*
    c2(52) -> 53*
    c2(42) -> 43*
    c2(54) -> 55*
    f0(2) -> 3*
    f0(1) -> 3*
    n2(41) -> 42*
    n2(43) -> 44*
    n0(2) -> 5*
    n0(1) -> 5*
    a2(40) -> 41*
    c0(2) -> 4*
    c0(1) -> 4*
    c3(60) -> 61*
    a0(2) -> 1*
    a0(1) -> 1*
    s0(2) -> 2*
    s0(1) -> 2*
    1 -> 38,26,6
    2 -> 28,20,18
    6 -> 52*
    10 -> 3*
    18 -> 54*
    19 -> 7*
    21 -> 5*
    27 -> 5*
    30 -> 40*
    31 -> 5*
    39 -> 29*
    40 -> 60*
    44 -> 31*
    53 -> 9,8
    55 -> 9,8
    61 -> 43,42
  problem:
   
  Qed