Round-six lemma `fwdP_spec`