Профессор Снэйп писал(а):
И даже не так, ещё сложнее

Да, действительно. Положим мы смягчили требование, и просим только, чтобы при использовании указанного правила вывода,

не входил свободно в элементы
задействованные в выводе. Все равно не понятно как тогда доказать, скажем, что из

и

следует

. Как быть? Рассматривать деревья вывода и требовать чтобы при применении пресловутого правила

не входил свободно в элементы

, стоящие в ветке, выходящей из точки применения правила? Чувствую, что-то не так: Ершов и Палютин не могли проглядеть подобный нюанас!