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

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

b(bot) = true
b(-F) = b(F)
b(F1/\F2) = b(F1) && b(F2) && h(F1)==h(F2)

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

p(bot) vale
p(-F) non vale
p(F1/\F2) vale sse p(F1) e p(F2)

Teorema: per ogni formula F, se p(F) e b(F)=true allora
  2^h(F) - 1 = #(F)
Per induzione strutturale su F:

+ caso bot:
   dimostro che se p(bot) e b(bot)=true allora
     2^h(bot) - 1 = #(bot)
   o equivalentemente se VERO allora 2^0 - 1 = 0
   assumo il vero
   dimostro 2^0 - 1 = 0
   ovvio

+ caso -F:
    per ipotesi induttiva se p(F) e b(F) = true allora
     2^h(F) - 1 = #(F)
    dimostro che se p(-F) e b(-F)=true allora
     2^h(-F) - 1 = #(-F)
    o equivalentemente se FALSO e b(F)=true allora
     2^(h(F)+1) - 1 = #(F) + 1
    assumo FALSO e b(F) = true
    quindi FALSO (H1) e b(F) = true (H2)
    assurdo per H1

+ caso F1 /\ F2:
    per ipotesi induttiva se p(F1) e b(F1) = true allora
     2^h(F1) - 1 = #(F1)
    per ipotesi induttiva se p(F2) e b(F2) = true allora
     2^h(F2) - 1 = #(F2)
    demmo dimostrare che se p(F1/\F2) e b(F1/\F2) = true
     allora 2^h(F1/\F2) - 1 = #(F1/\F2)
    o equivalentemente se p(F1) e p(F2) e
     b(F1) && b(F2) && h(F1)=h(F2) = true allora 
     2^(max(h(F1),h(F2))+1) - 1 = #(F1)+#(F2)+1
    assumo p(F1) (H1)
    assumo p(F2) (H2)
    assumo b(F1) (H3)
    assumo b(F2) (H4)
    assumo h(F1)=h(F2) (H5)
    per ipotesi induttiva, H1, H3 ho 2^h(F1) - 1=#(F1) (K1)
    per ipotesi induttiva, H2, H4 ho 2^h(F2) - 1=#(F2) (K2)
    per H5 debbo dimostrare
     2^(max(h(F1),h(F1))+1) - 1 = #(F1)+#(F2)+1
    per le proprietà del massimo debbo dimostrare
     2^(h(F1)+1) - 1 = #(F1)+#(F2)+1
    per le proprietà delle potenze debbo dimostrare
     2*2^h(F1) - 1 =?= #(F1)+#(F2)+1
                   = 2^h(F1) -1 + 2^h(F2) -1 +1   per K1,K2
                   = 2^h(F1) -1 + 2^h(F1) -1 +1   per H5
    ovvio

qed