Round-six lemma `bwdP_spec`