\left[\forall_{{_{-}a} \in \{-t + 1~\ldotp \ldotp~0\}}~\left(\left(U^{2^{-{_{-}a}}} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \left(2^{-{_{-}a}} \cdot \varphi\right)} \cdot \lvert u \rangle\right)\right)\right] \Rightarrow \left(\left(\left(U^{2^{-\left(-t + 1\right)}} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \left(2^{-\left(-t + 1\right)} \cdot \varphi\right)} \cdot \lvert u \rangle\right)\right) \land \left(\left(U^{2^{-\left(-t + 2\right)}} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \left(2^{-\left(-t + 2\right)} \cdot \varphi\right)} \cdot \lvert u \rangle\right)\right) \land \ldots \land \left(\left(U^{2^{-0}} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \left(2^{-0} \cdot \varphi\right)} \cdot \lvert u \rangle\right)\right)\right)