Round-six lemma `out_step`