Round-six lemma `axB_run`