Round-six lemma `iLoop_run`