Round-six lemma `replP_runs`