§3, p. 6 — MITM-factor stops at the least positive depth (corrected: depths 1 … 2⌈l/2⌉; depth 0 is never tested)

Let $V \subseteq U(2^n)$ be a finite set of unitaries (standing for $\mathcal V_{n,\mathcal G}$), $U$ a unitary and $l \ge 0$. Write $h = \lceil l/2\rceil$.

1. If $d$ is the least positive depth at which $U$ can be implemented over $V$ (that is, $1 \le d$, $U \in S_d$ and $U \notin S_{d'}$ for $1 \le d' < d$), and $d \le 2h$, then MITM-factor$(\mathcal G, U, l)$ returns a circuit $c$ with every layer in $V$, implementing $U$, and of depth exactly

2. If $U \notin S_d$ for every $1 \le d \le 2h$, then MITM-factor$(\mathcal G, U, l)$ returns nothing.

This is the paper's claim that the algorithm "terminates at the smallest depth for which there exists a circuit implementing $U$", stated in the form the pseudocode actually supports (see the note).

Formalization Note. Two corrections to the printed sentence, both forced by the pseudocode. (i) For odd $l$ the last iteration $i = h$ also tests depth $2h = l+1$, so the depths searched are $1,\dots,2\lceil l/2\rceil$ rather than $1,\dots,l$. (ii) The loop starts at $i = 1$, so depth $0$ is never tested: for $U = I$ the algorithm returns a circuit of the least positive depth, not the empty circuit. The statement holds for every finite set of unitaries $V$.