Round-six lemma `T2_runsP`