A complete proof of correctness of the Knuth-Bendix completion algorithm
scientific article; zbMATH DE number 3729441