Round-six lemma `mainU_runs`