§3, p. 6 — iteration i of MITM-factor tests depth 2i − 1, then depth 2i

Let $V \subseteq U(2^n)$ be a finite set of unitaries (standing for $\mathcal V_{n,\mathcal G}$), $U$ a unitary and $i \ge 1$. Consider iteration $i$ of MITM-factor, which tests $S_{i-1}^\dagger U \cap S_i \neq \emptyset$ and then $S_i^\dagger U \cap S_i \neq \emptyset$.

1. The iteration returns nothing if and only if $U \notin S_{2i-1}$ and $U \notin S_{2i}$.
2. If it returns a circuit $c$, then every layer of $c$ lies in $V$, $c$ implements $U$, and

In words: the first test succeeds exactly when $U$ has a circuit of depth $2i-1$, the second exactly when it has one of depth $2i$, and the returned circuit has that depth.

Formalization Note. $|c|$ is the length of the list $c$ of layers. The statement holds for every finite set of unitaries $V$.