| 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 |
