The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
scientific article; zbMATH DE number 5903837