Операции над нумералами - последователь

Suc ≡ λx y z.y (x y z)
Операция прибавления единицы к нумералу Чёрча.

В самом деле:

Sucn⌉ ≡ (λx y z.y (x y z)) (λf x.fn x) ; def Suc и нумерала
= λy z.y ((λf x.fn x) y) z ; →β, редекс - всё
= λy z.y (λx.yn x) z ; →β
= λy z.y (yn z) ; →β
≡ λy z.yn + 1 z ; def композиции
≡ ⌈n + 1⌉ ; def нумерала