Round-six lemma `retChk_ok`