def 0 ^m.^n.n
def true ^p.^q.p
def def false ^p.^q.q
def suc ^p.^m.^n.m(p m n)
def pred ^$k.$k(^p.(mpair(suc(p true))(p true)))(mpair 0 0)false
def mpair ^a.^b.^u.u a b
def def iszero ^n. n (true false) true
def ADD ^m.^n.^x.^y.m x(n x y)
def MUL ^m.^n.^f.m(n f)
def EXP ^m.^n.n m
def GT ^m.^n.not(iszero (n pred m))
def EQ ^m.^n.and (iszero (m pred n)) (iszero (n pred n))
def LT ^m.^n.not(iszero(m pred n))
def GE ^m.^n.not(LT m n)
iszero 0
iszero 5
suc 0
suc 1
suc 2
pred 3
pred 2
pred 1
pred 0
ADD 1 2
MUL 2 3
EXP 2 3
EXP 3 2
GT 2 3
GT 3 2
EQ 4 (ADD 2 2)
EQ 5 (ADD 3 3)
(EQ (ADD (MUL 2 (DIV 6 (MUL 3 (SUB 8 2))))) (ADD (MUL 2 (DIV 6 (MUL 3 (SUB 8 2))))))
quit