Round-six lemma `cntP_sp`