F ::= bot | F /\ F | -F

h(bot) = 0
h(F1 /\ F2) = max(h(F1),h(F2)) + 1
h(-F) = h(F) + 1

# conta il numero di /\ e -
#(bot) = 0
#(F1 /\ F2) = #(F1) + #(F2) + 1
#(-F) = #(F) + 1

p(F)  significa F non contiene /\
p(bot) VALE
p(-F) VALE se p(F) VALE
p(F1 /\ F2) NON VALE

Teorema: per ogni F, se p(F) vale allora h(F) = #(F)
Per induzione strutturale su F:

+ caso bot:
   dimostro che se p(bot) vale allora h(bot) = #(bot)
   se VERO allora 0 = 0
   assumo il vero
   dimostro 0 = 0
   ovvio

+ caso -F:
   ipotesi induttiva: se p(F) allora h(F) = #(F)
   dimostro che se p(-F) allora h(-F) = #(-F)
   o equivalentemente se p(F) allora h(F)+1 = #(F)+1
   assumo p(F) (H)
   per H e l'ipotesi induttiva, h(F) = #(F)
   da cui h(F)+1 = #(F)+1

+ caso F1 /\ F2:
   ipotesi induttiva: se p(F1) allora h(F1) = #(F1)
   ipotesi induttiva: se p(F2) allora h(F2) = #(F2)
   dimostro che se p(F1 /\ F2) allora h(F1/\F2)=#(F1/\F2)
   se FALSO allora max(h(F1),h(F2))+1 = #(F1)+#(F2)+1
   assumo FALSO
   assurdo!

qed.