The source pulls the loops to the front one at a time, replacing a loop nested under a conditional or followed by further code by a loop whose body tests a Boolean flag recording the position in the original control flow ($PartD/ForPrenex.lean$, $PartD/ForNest.lean$, $PartD/ForMerge.lean$). The concept's prenex form is transported through $prenexForm_toSrcProg$: loop freedom, nesting of loops and the one-output bound all commute with $toSrcProg$, so the source's prenex program comes back as $ofSrcProg$ of it, with the same semantics by $eval_ofSrcProg$.

Lemma D.1.3 of Transducers, Part D; formalised by Aristotle (Harmonic).