Asta Halkjær From: An Isabelle/HOL Framework for Synthetic Completeness Proofs. CPP 2025: 171-186