Round-six lemma `dgI_runs`