Alphabet

id:N → N
succ:((N → N) → N → N) → (N → N) → N → N
two:(((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N
zero:(((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N

Variables

F:(N → N) → N → N
Z:N → N
U:N
V:N
I:((N → N) → N → N) → (N → N) → N → N
J:(N → N) → N → N
F1:N → N
Y1:N
G1:((N → N) → N → N) → (N → N) → N → N
H1:(N → N) → N → N
I1:N → N
P1:N

Rules

succ · (λ%Y:N -> N.F · %Y) · (λ%X:N.Z · %X) · U⇒F · Z · (Z · U)
id · V⇒V
two · (λ%V:(N -> N) -> N -> N.I · %V) · (λ%U:N -> N.J · %U) · (λ%Z:N.F1 · %Z) · Y1⇒I · (I · J) · F1 · Y1
zero · (λ%G:(N -> N) -> N -> N.G1 · %G) · (λ%F:N -> N.H1 · %F) · (λ%W:N.I1 · %W) · P1⇒H1 · I1 · P1