BVL-->BVP correctness thm sketched