Round-six lemma `M_runsG`