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

Teorema: per ogni F, h(F) <= #(F)
Per induzione strutturale su F:
+ caso bot:
   debbo dimostrare h(bot) <= #(bot)
   o equivalentemente 0 <= 0
   ovvio

+ caso -F:
   per ipotesi induttiva h(F) <= #(F)
   debbo dimostrare h(-F) <= #(-F)
   o equivalentemente h(F) +1 <= #(F) + 1
   ovvio

+ caso F1 /\ F2:
   per ipotesi induttiva h(F1) <= #(F1)
   per ipotesi induttiva h(F2) <= #(F2)
   debbo dimostrare h(F1 /\ F2) <= #(F1 /\ F2)
   o equivalentemente max(h(F1),h(F2))+1 <= #(F1)+#(F2)+1
   ho
      max(h(F1),h(F2))+1
   <= max(#(F1),#(F2))+1   per ipotesi induttiva x2
   <= #(F1)+#(F2)+1        per proprietà del massimo
qed