Аннотация:
1. Из сильной конгруэнтности формул следует их конгруэнтность.
2. Сохранение конгруэнтности при прямых формульных подстановках. Непрямое действие формульной подстановки на формулу.
3. Подстановки конгруэнтных формул дают конгруэнтные формулы.
4. Коммутирование формульных подстановок с заменами свободных и вспомогательных переменных.
5. Композиция формульных подстановок. Подстановочное замыкание множества формул.
Обратная связь: