-- Combinadores basicos
 i  = \x. x ; 
 k  = \x y. x;        
 s  = \x y z. x z (y z);

-- Combinador de ponto fixo      
 fix      = \f. (\x. f (x x)) (\x. f (x x)) ;

-- Logica booleana
 true     =  \a b. a ;
 false    =  \a b. b ;
 if       =  \c a b. c a b ;
 and      =  \a b. a b a ;
 or       =  \a b. a a b ;
 not      =  \p. p false true ;
 xor      =  \a b. (or (and (not a) b) (and a (not b))) ;
 sss      =  \a b. (not (xor a b)) ;

-- Pares
 pair     = \a b c. c a b ;
 fst      = \p. p true ;
 snd      = \p. p false ;

-- Numeros naturais
 zero     = \f x. x ;
 succ     = \n p. \q. p (n p q) ;
 pred     = \n. fst (n (\p.(pair (snd p) (succ (snd p)))) (pair zero zero)) ;
 add      = \m n p q. (m p) (n p q) ;
 sub      = \m n. (n pred) m ;
 isZero   = \n. n (\x. false) true ;
 equal    = \m n. and (isZero (sub m n)) (isZero (sub n m)) ;
 lessEq   = \m n. isZero (sub m n) ;
 great    = \m n. not ( isZero (sub m n)) ;
 greatEq  = \m n. isZero (sub n m) ;
 less     = \m n. not (isZero (sub n m)) ;
 mult     = \m n p q. m (n p) q ;
 div      = fix (\M. \m n. if (less m n) zero (succ (M (sub m n) n))) ;
 mod      = fix (\M. \m n. if (less m n) m (M (sub m n) n)) ; 
 exp      = \m n. n m ;
 fatorial = fix (\M. \n. if (isZero (pred n)) 1 (mult n (M (pred n)))) ;

-- Listas
 empty    = \x. true ;
 cons     = \h t. pair h t ;
 isEmpty  = \l. l (\x y.false) ;
 head     = fst ;
 tail     = snd ;
 length   = fix (\M. \l. if (isEmpty l) 0 (succ (M (tail l)))) ;

>> isEmpty (cons 2 empty)