3622
правки
Изменения
м
→Кр1
То есть пример:
(\ λ f . f f) ((\ λ x . x) z)
Сначала делаем обычную редукцию нормальным порядком и получаем:
((\ λ x . x) z) ((\ λ x . x) z)
А потом после редукции нормальным порядком надо сделать изменения сразу в двух термах, потому что они якобы в коробках, и получим суммарно за 2 редукции: