F = \f.\n.$iszero n $one ($mul n (f ($pred n)))
Fv = \f.\n.$iszero n (\d.$one) (\d.$mul n (f ($pred n))) (\d.d)
I = \x.x
K = \x.\y.x
Omega = (\x.x x) (\x.x x)
S = \f.\g.\x.f x (g x)
Y = \h.(\x.h (x x)) (\x.h (x x))
YT = (\x.\y.y (x x y)) (\x.\y.y (x x y))
Yp = \h.(\x.h (\a.x x a)) (\x.h (\a.x x a))
Yv = \h.(\x.\a.h (x x) a) (\x.\a.h (x x) a)
add = \m.\n.\f.\x.m f (n f x)
append = $Y (\g.\z.\w.$null z w ($cons ($hd z) (g ($tl z) w)))
cons = \x.\y.$pair $fal ($pair x y)
exp = \m.\n.\f.\x.m n f x
fal = \x.\y.y
five = \f.\x.f (f (f (f (f x))))
four = \f.\x.f (f (f (f x)))
fst = \p.p $tru
hd = \z.$fst ($snd z)
iszero = \n.n (\v.$fal) $tru
mul = \m.\n.\f.\x.m (n f) x
next = \p.$pair ($snd p) ($succ ($snd p))
nil = \z.z
null = $fst
one = \f.\x.f x
pair = \x.\y.\s.s x y
pred = \n.$fst (n $next ($pair $zero $zero))
snd = \p.p $fal
succ = \n.\f.\x.f (n f x)
three = \f.\x.f (f (f x))
tl = \z.$snd ($snd z)
tru = \x.\y.x
two = \f.\x.f (f x)
zero = \f.\x.x