§3, p. 6 — S_i is exactly the set of unitaries of the circuits of i layers

Let $V \subseteq U(2^n)$ be a finite set of unitaries, standing for $\mathcal V_{n,\mathcal G}$. For every $i \ge 0$:

1. a list $c$ of unitaries is a circuit of $i$ layers over $V$ (as generated recursively by MITM-factor, extending circuits of $i-1$ layers by one more layer) if and only if $c$ has length $i$ and all its entries lie in $V$;
2. the set $S_i = VS_{i-1}$ ($S_0 = \{I\}$) built by MITM-factor is exactly the set of unitaries implemented by these circuits:

So the sets the algorithm generates step by step are the sets "$S_i$ of all unitaries implementable in depth $i$" of Lemma 1, and the circuits it extends are all depth-$i$ circuits.

Formalization Note. A circuit is a List of layers and implements its List.prod, with the head of the list leftmost, as in "$U_1U_2\cdots U_m$" on p. 4.