I=\x.x; K=\x y.x; S=\x y z.x y(x z); B=\x y z.x (y z); C=\x y z.x z y; W=\x y.x y y; SOMEGA=\x.x x; OMEGA=SOMEGA SOMEGA; Y=\g.(\x.g (x x))(\x.g (x x)); ZERO=\f x.x; SUCC=\n f x.f(n f x); PLUS=\m n.m SUCC n; MULT=\m n.m (PLUS n) 0; EXP=\b e.e b; PRED=\n f x.n(\g h.h(g f))(\u.x)(\u.u); SUB=\m n.n PRED m; ISZERO=\n.n(\x.false)true; LEQ=\m n.ISZERO (MINUS m n); AND=\p q.p q p; OR=\p.p p;