# Time to construct a GNBA for LTL formula

I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula:

Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ over alphabet $2^{AP}$ such that:

1. $\operatorname{Word}(\varphi)=L_{\omega}(G_{\varphi})$.

2. $G_{\varphi}$ can be costructed in time and space $2^{O(|\varphi|)}$, where $|\varphi|$ is the size of $\varphi$.

3. The number of accepting states of $G_{\varphi}$ is bounded above by $O(|\varphi|)$.

My problem lies in the proof of (2), that is, in the proof it says that the number of states in $G_{\varphi}$ is bounded by $2^{|\operatorname{subf}(\varphi)|}$ but since $|\operatorname{subf}(\varphi)| \leq 2\cdot|\varphi|$ (where $\operatorname{subf}(\varphi)$ is the set of all subformulae) the number of states is bounded by $2^{O(|\varphi|)}$.

But why does $|\operatorname{subf}(\varphi)| \leq 2\cdot|\varphi|$ hold?

$\qquad \varphi \land \psi$
has two direct subformulae $\varphi$ and $\psi$. This can be continued recursively and we see that
$\qquad \displaystyle |\operatorname{subf}(\varphi)| \leq \sum_{\circ \in \operatorname{op}(\varphi)} \operatorname{arity}(\circ)$,
where $\operatorname{op}(\varphi)$ is the multi-set of operators occurring in $\varphi$. Informally speaking, every operator contributes its operands to the set of subformulae. Note that we have $\leq$ and not $=$ because a subformula might occur multiple times.
In LTL, all operators have at most arity two, so $|\operatorname{subf}(\varphi)| \leq 2|\varphi|$ provided that $|.|$ counts (at least) operator occurrences.