Round-six lemma `finB_runs`