Since we know that the sequence of control values does not depend on the complex input, the subscript values will always be in bounds if they are in bounds for any particular routine invocation.
This is a modification of the routine that produces the same subscript values and verifies that each value is within bounds in place of doing complex arithmetic on the array elements.
Routine āvā is called with each subscript value instead of its use as a subscript.
For the curious, the first block within the fft routine permutes the
complex numbers so that the number that was at index j moves to
index k where the binary bits of j and k are reversed, left from right.
But this fact is not part of the proof.