Not = λx.x?False:True
Xor = λx.λy.x?(Not y):y
And = λx.λy.x?y:False
Or = λx.λy.x?True:y Inc = λn.λf.λx.f (n f x)
Add = λm.λn.λf.λx.m f (n f x)
Mul = λm.λn.λf.λx.m (Add n) 0
Pow = λm.λn.λf.λx.m (Mul n) 1
Dec = λn.fst (n (λx.<snd x, (Inc (snd x))>) (pair 0 0))
Sub = λm.λn.n Dec m
Div = λm.λn.m (λx.((Inc x)*n > m)?x:(Inc x)) 0
IsZero = λn.n (λx.False) True
IsOdd = λn.n Not False
IsLess = λm.λn.IsZero (Sub m n)
IsEqual = λm.λn.And (IsLess m n) (IsLess n m)
Fact = λn.fst (n (λp.<(fst p) * (snd p), Inc (snd p)>) 1)
Fib = λn.fst (n (λp.<(fst p) + (snd p), (snd p)>) <0, 1>)