§3, p. 6 — |S_i| ≤ |V_{n,G}|^i (the cardinality bound of the running-time analysis)

Let $V \subseteq U(2^n)$ be a finite set of unitaries, standing for $\mathcal V_{n,\mathcal G}$, and let $S_0 = \{I\}$, $S_i = VS_{i-1}$. Then for every $i \ge 0$,

This bound turns the per-iteration cost of MITM-factor, stated in terms of $|S_{i-1}|$ and $|S_i|$, into the bound $2|\mathcal V_{n,\mathcal G}|^i\log(|\mathcal V_{n,\mathcal G}|^i)$ of the running-time analysis. The time bound itself is part of the goal theorem.

Formalization Note. The statement holds for every finite set of unitaries $V$.