Round-six lemma `rotR_runs`