Verification of an Anti-unification Algorithm in PVS. - Mauricio Ayala-Rincón; Thaynara Arielly de Lima; Maria Júlia Dias Lima; Mariano M. Moscato; Temur Kutsia (NFM, 2025)