Completeness in PVS of a nominal unification algorithm
scientific article; zbMATH DE number 6862942