Round-six lemma `outP_spec`