Copyright (c) 2000 John A. Maiorana. All rights reserved.
lambda-0.1.3
<< << << << << << << << << << << << << << << ==> iszero 0
====>iszero 0
<< ==> iszero 5
====>iszero(5)
<< ==> suc 0
====>^m.^n.m(0 m n)
<< ==> suc 1
====>^m.^n.m((1)m n)
<< ==> suc 2
====>^m.^n.m((2)m n)
<< ==> pred 3
====>false(^m.^n.m((^p.mpair(suc(p true))(p true))((^p.mpair(suc(p true))(p true))(mpair 0 0))true m n))(2)
<< ==> pred 2
====>false(^m.^n.m((^p.mpair(suc(p true))(p true))(mpair 0 0)true m n))(I)
<< ==> pred 1
====>false(^m.^n.m(mpair 0 0 true m n))0
<< ==> pred 0
====>false 0 0
<< ==> (ADD 1) 2
====>^x.^y.(1)x((2)x y)
<< ==> (MUL 2) 3
====>^f.(2)((3)f)
<< ==> (EXP 2) 3
====>^n.(2)((2)((2)n))
<< ==> (EXP 3) 2
====>^n.(3)((3)n)
<< ==> (GT 2) 3
====>not(iszero(false(^m.^n.m((^p.mpair(suc(p true))(p true))(mpair 0 0)true m n))(I)(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false))
<< ==> (GT 3) 2
====>not(iszero(false(^m.^n.m((^p.mpair(suc(p true))(p true))((^p.mpair(suc(p true))(p true))(mpair 0 0))true m n))(2)(^p.mpair(suc(p true))(p true))(^u.u 0 0)false))
<< ==> (EQ 4)((ADD 2) 2)
====>and(iszero(false(^m.^n.m((^p.mpair(suc(p true))(p true))((2)(^p.mpair(suc(p true))(p true))(mpair 0 0))true m n))(3)(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false))(iszero(false(^m.^n.m((^p.mpair(suc(p true))(p true))((2)(^p.mpair(suc(p true))(p true))(mpair 0 0))true m n))(3)(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false))
<< ==> (EQ 5)((ADD 3) 3)
====>and(iszero(false(^m.^n.m((^p.mpair(suc(p true))(p true))((^p.mpair(suc(p true))(p true))((3)(^p.mpair(suc(p true))(p true))(mpair 0 0)))true m n))(5)(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false))(iszero(false(^m.^n.m((^p.mpair(suc(p true))(p true))((^p.mpair(suc(p true))(p true))((3)(^p.mpair(suc(p true))(p true))(mpair 0 0)))true m n))(5)(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false(^p.mpair(suc(p true))(p true))(^u.u 0 0)false))
<< ==> (EQ(ADD((MUL 2)((DIV 6)((MUL 3)((SUB 8) 2))))))(ADD((MUL 2)((DIV 6)((MUL 3)((SUB 8) 2)))))
====>and(iszero(^y.MUL(2)(DIV(6)(MUL(3)(SUB(8)(2))))(ADD(MUL(2)(DIV(6)(MUL(3)(SUB(8)(2))))))(pred(ADD(MUL(2)(DIV(6)(MUL(3)(SUB(8)(2))))))y)))(iszero(^y.MUL(2)(DIV(6)(MUL(3)(SUB(8)(2))))(ADD(MUL(2)(DIV(6)(MUL(3)(SUB(8)(2))))))(pred(ADD(MUL(2)(DIV(6)(MUL(3)(SUB(8)(2))))))y)))
<< exit 0