es56

(define compose (lambda (f g)
                  (lambda (x) (f (g x)))))

(define (ponzipo f n)
  (if (= (f n) 0)
      (mktree f emptytree emptytree)
      (mktree f
              (ponzipo (lambda (x) (if (= x n) (- (f n) 1) (f x))) n)
              (ponzipo (lambda (x) (if (= x n) (- (f n) 1) (f x))) n))))

;; ponzipo e' totale. Si dimostra per induzione sul valore dell'applicazione del primo
;; argomento al secondo argomento, cioe' (f n).
;;Nel caso questa sia 0 allora ponzipo restituisce un
;; valore. Altrimenti restituisce un valore che e' definito se lo
;; e' (ponzipo (lambda (x) (if (= x n) (f (- n 1)) (f x))) n). 
;; Ma per ipotesi induttiva ponzipo e' totale se l'applicazione del primo al secondo
;; argomento e' minore di (f n), come in effetti e' ((lambda (x) (if (= x n) (f (- n 1)) (f x))) n) = (- (f n) 1).

;; In modo ancora piu' formale, il dominio di ponzipo e' il dominio [funzioni-da-naturali-a-naturali x naturali]
;; Su questo dominio possiamo definire la relazione di precedenza (f,n) << (g, n)  sse  (f n) < (g n).
;; tale relazione e' ben fondata perche' le funzioni considerate sono da naturali a naturali.
;; Gli elementi minimali sono le coppie (h m) tali che (= (h m) 0). Su tali elementi ponzipo e' definita.
;; Su quelli non minimali anche, per ipotesi induttiva, poiche' 
;; ((lambda (x) (if (= x n) (f (- n 1)) (f x))), n) << (f n).