| def LIST map suc(append 2(append 1 end)) |
| def mknode (^a.^b.^u.u a b false) |
| def head (^n.n sel_1) |
| def tail (^n.n sel_2) |
| def is_end (^n.n sel_3) |
| def sel_1 (^p.^q.^r.p) |
| def sel_2 (^p.^q.^r.q) |
| def sel_3 (^p.^q.^r.r) |
| def nth ^n.^list.head((pred n) tail list) |
| def renda ^e.^&u.&u e e true |
| def rend (^x.renda(x x))(^x.renda(x x)) |
| def nend ^u.u 0 0 true |
| def end ^&u.&u rend rend true |
| def Appenda ^h.^n.^list.(is_end list)(mknode n end)(mknode(head list)(h n(tail list))) |
| def append (^x.Appenda(x x))(^x.Appenda(x x)) |
| def Mapa ^h.^f.^list.(is_end list)(end)(mknode(f (head list))(h f (tail list))) |
| def map (^x.Mapa(x x))(^x.Mapa(x x)) |
| def mtriple ^a.^b.^c.^u.u a b c |
| def 1st ^a.^b.^c.a |
| def 2nd ^a.^b.^c.b |
| def 3rd ^a.^b.^c.c |
| def div_cond ^p.GE(p 1st)(p 2nd) |
| def div_body ^t.mtriple(sub (t 1st)(t 2nd))(t 2nd)(suc(t 3rd)) |
| def div ^m.^n.while div_cond div_body (mtriple m n 0)3rd |
| def sub ^m.^n.n pred m |
| def force ^$.$ |
| def pred_body ^p.mpair (suc(p true))(p true) |
| def do ^n.^b.^x.n b x |
| def c1 ^p.not(iszero(p true)) |
| def btri ^p.mpair(pred(p true))(add(p true)(p false)) |
| def tri ^k.while c1 btri(mpair k 0)false |
| def Wh ^f.^c.^b.^x.(c x) (f c b (b x)) x |
| def while (^x.Wh(x x))(^x.Wh(x x)) |
| def G ^g.^f.f(g f) |
| def Y2d Y G |
| def Y2 (^x.G(x x))(^x.G(x x)) |
| def Y3 Y2 G |
| def Y4 Y3 G |
| def Y5 Y4 G |
| def YC S(S(K PHI)I)(S(K PHI)I) |
| def PHI S(K W)(S(K B)I) |
| def W ^f.^x.f x x |
| def S ^x.^y.^z.x z(y z) |
| def B ^x.^y.^z.x(y z) |
| def K ^x.^y.x |
| def I ^x.x |
| def true ^p.^q.p |
| def false ^p.^q.q |
| def and ^a.^b.a b false |
| def or ^a.^b.a true b |
| def not ^r.^p.^q.r q p |
| def mpair ^a.^b.^u.u a b |
| def iszero ^n. n (true false) true |
| def pred ^$k.$k(^p.(mpair(suc(p true))(p true)))(mpair 0 0)false |
| def add ^m.^n.m suc n |
| def mul ^m.^n.m(add n)0 |
| def exp ^m.^n.n(mul m)1 |
| def Y ^f.(^x.f(x x))(^x.f(x x)) |
| def F ^h.^n.(iszero n) 1 (mul n (h(pred n))) |
| def fact (^x.F(x x))(^x.F(x x)) |
| def H ^h.or(not h)A |
| 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) |
| def YH ^f.(^x.f(^h.x x h))(^x.f(^h.x x h)) |
| def YG ^f.(^x.^g.f(x x)g)(^x.^g.f(x x)g) |
| def S ^x.^y.^z.x z(y z) |
| def K ^x.^y.x |
| def I ^x.x |
| def triple ^x.^y.^z.^p.p x y z |
| def sel1 ^x.^y.^z.x |
| def sel2 ^x.^y.^z.y |
| def sel3 ^x.^y.^z.z |
| def isend ^t.t sel3 |
| def lpair ^a.^b.triple a b false |
| def B ^x.^y.^z.x(y z) |
| def W ^f.^x.f x x |
| def 0 ^m.^n.n |
| def suc ^p.^m.^n.m(p m n) |
