Описана реализация алгоритма исключения избыточности. Он основан на новой алгебраической системе, обладающей семантикой совокупности правил условной эквациональной теории или условной системы переписывания термов.