; fact
(value '(((lambda (f) 
            (f f)) 
          (lambda (f) 
            (lambda (n) 
              (cond ((zero? n) 1) 
                    (else (((lambda (f) 
                              (f f)) 
                            (lambda (f) 
                              (lambda (n m) 
                                (cond ((zero? m) 0) 
                                      (else (((lambda (f) 
                                                (f f)) 
                                              (lambda (f) 
                                                (lambda (n m) 
                                                  (cond ((zero? m) n) 
                                                        (else ((lambda (n)(add1 n)) ((f f) n ((lambda (n)(sub1 n)) m)))))))) 
                                             n ((f f) n ((lambda (n)(sub1 n)) m)))))))) 
                           n ((f f) ((lambda (n)(sub1 n)) n)))))))) 5))

; y
(lambda (g) 
  ((lambda (f) 
     (f f)) 
   (lambda (f) 
     (g (lambda (x) 
          ((f f) x))))))

; dbl
(value '(((lambda (g) 
            ((lambda (f) 
               (f f)) 
             (lambda (f) 
               (g (lambda (x) 
                    ((f f) x)))))) 
          (lambda (f) 
            (lambda (n) 
              (cond ((zero? n) n) 
                    (else (add1 (add1 (f (sub1 n))))))))) 5))