The [Fabius function](http://en.wikipedia.org/wiki/Fabius_function) is a smooth monotone function $F:[0,1]\to[0,1]$, satisfying the functional equations
$$F(0)=0, \quad F(1-x)=1-F(x)\tag1$$
and
$$F'(x) = 2 \,F(2 x) \quad \text{for} \,\, 0<x<1/2.\tag2$$

[![Fabius graph][1]][1]

The function $F(x)$ assumes rational values at dyadic rational arguments. In particular,
$$F\left(2^{-n}\right) = 2^{-\frac{n(n+1)}{2}}\left[\frac1{n!}+\sum_{m=1}^{\lfloor n/2\rfloor}\frac{(-1)^m \, c_m}{(n - 2 m)!}\right],\tag3$$
where
$$c_m = \frac1{4^m - 1}\left[\frac{(-1)^m}{(2m+1)!}+\sum_{k=1}^{m-1} \frac{(-1)^k \, c_{m-k}}{(2 k + 1)!}\right],\tag4$$
and empty sums are assumed to be zero. These values appear as [A272755](http://oeis.org/A272755)/[A272757](http://oeis.org/A272757) in the OEIS.

Let
$$a_n = F\left(2^{-n}\right) \, 2^{\binom {n-1}2}  \, (2n)! \, \prod_{m=1}^n\left(2^m - 1\right)\tag5$$
This sequence appears as [A277471](http://oeis.org/A277471) in the OEIS. It looks like all its terms are integers. How can we prove that?

  [1]: https://i.sstatic.net/RGqBP.png