Подстановка

Подстановка терма v вместо всех свободных вхождений переменной x в терм u обозначается

u [ x := v ]

и определяется так:

Если хоть одна переменная в поставляемом терме v должна стать связанной, то мы не имеем права применять подстановку.