Round-six lemma `revE_runs`