Assume you are given $f(x) \in O(n2^{O((\log \log n)^2)})$. My first question is what the exact definition of big-O is in case of nested functions. I have come up with the following:
$\exists c > 0, \exists n_0 > 0, \forall n > n_0 \colon f(x) \leq cn2^{c(\log \log n)^2}$
Is this correct?
Second, assuming my definition is correct, then is the following reasoning valid:
$f(x) \leq cn2^{c(\log log n)^2} = n2^{c(\log \log n)^2 + \log c} \in n 2^{O((\log \log n)^2)}$
So that $f(x) \in O(n2^{O((\log \log n)^2)})$ implies $f(x) \in n 2^{O((\log \log n)^2)}$?