Round-six lemma `rotDU_runs`