Round-six lemma `p2E_runs`