F ::= \bot | \top | A | B | ...  | F /\ F | F \/ F | -F | F => F

=========
Problema: calcolare altezza
Soluzione: h(F)

h \bot = 1
h \top = 1
h A = 1
h B = 1
... 
h (-F) = 1 + h(F)
h (F1 /\ F2) = 1 + max(h(F1),h(F2))
h (F1 \/ F2) = 1 + max(h(F1),h(F2))
h (F1 => F2) = 1 + max(h(F1),h(F2))

=========
Problema: calcolare il numero di simboli
Soluzione: #(F)

# \bot = 1
# \top = 1
# A = 1
# B = 1
...
# (-F) = 1 + #(F)
# (F1 /\ F2) = 1 + #(F1) + #(F2)
# (F1 \/ F2) = 1 + #(F1) + #(F2)
# (F1 => F2) = 1 + #(F1) + #(F2)

=========
Problema: decidere se NON contiene negazioni
Soluzione: nn(F)

nn \bot = true
nn \top = true
nn A = true
nn B = true
...
nn (-F) = false
nn (F1 /\ F2) = nn(F1) && nn(F2)
nn (F1 \/ F2) = nn(F1) && nn(F2)
nn (F1 => F2) = nn(F1) && nn(F2)

=========
Problema: decidere se è bilanciata
Soluzione: b(F)

b \bot = true
b \top = true
b A = true
b B = true
...
b (-F) = b(F)
b (F1 /\ F2) = b(F1) && b(F2) && h(F1) = h(F2)

=========
Problema: calcolare il max di due numeri
Soluzione: max(x,y) = if x <= y then x else y

=========
Problema: dire se x è <= y
Soluzione: x <= y

O <= y = true
(S x) <= y =
  match y with
  [ O => false
  | S n => x <= n ]

=========
Problema: dire se x è = y
Soluzione: x = y

0 = y =
 match y with
 [ O => true
 | S _ => false ]

(S x) = y =
 match y with
 [ O => false
 | S n => x = n

=========
Teorema: per ogni formula F, nn(F) /\ b(F) => #(F) = 2^h(F) - 1
Procedo per induzione strutturale su F

caso \bot:
  dimostro
    nn \bot /\ b \bot => #(\bot) = 2^h(\bot) - 1
  ovvero
    true /\ true => 1 = 2^1 - 1
  ovvero
    true => 1 = 1
  ovvio

casi \top, A, B, ...: analoghi

caso -F:
  per ipotesi induttiva
     nn(F) /\ b(F) => #(F) = 2^h(F) - 1
  dimostro
     nn(-F) /\ b(-F) => #(-F) = 2^h(-F) - 1
  ovvero
     false /\ b(-F) => #(-F) = 2^h(-F) - 1
  ovvero
     false => #(-F) = 2^h(-F) - 1
  ovvio

caso F1 /\ F2:
  per ipotesi induttiva
     nn(F1) /\ b(F1) => #(F1) = 2^h(F1) - 1
  per ipotesi induttiva
     nn(F2) /\ b(F2) => #(F2) = 2^h(F2) - 1
  debbo dimostrare
     nn(F1/\F2) /\ b(F1/\F2) => #(F1/\F2) = 2^h(F1/\F2) - 1
  ovvero
     nn(F1) /\ nn(F2) /\
     b(F1) /\ b(F2) /\ h(F1) = h(F2) =>
     1 + #(F1) + #(F2) = 2^(1 + max(h(F1),h(F2))) - 1
  assumo
    nn(F1)      (N1)
    nn(F2)      (N2)
    b(F1)       (B1)
    b(F2)       (B2)
    h(F1)=h(F2) (H)
  e dimostro 
     1 + #(F1) + #(F2) =? 2^(1 + max(h(F1),h(F2))) - 1
  da N1, B1 e la prima ipotesi induttiva ottengo
    #(F1) = 2^h(F1) - 1
  da N2, B2 e la seconda ipotesi induttiva ottengo
    #(F2) = 2^h(F2) - 1
  quindi mi basta dimostrare
    1 + 2^h(F1) - 1 + 2^h(F2) - 1 =?
    2^1 * 2^(max(h(F1),h(F2))) - 1
  usando l'ipotesi H mi basta dimostrare
    1 + 2^h(F1) - 1 + 2^h(F1) - 1 =?
    2^1 * 2^(max(h(F1),h(F1))) - 1
  ovvero
    2 * 2^h(F1) -1 =?
    2 * 2^h(F1) - 1
  ovvio
qed.

====================================
informale:
F ::= \bot | \top | A | B | ...  | F /\ F | F \/ F | -F | F => F

formale:
nat ::= O | S nat
F ::= \bot | \top | V nat  | F /\ F | F \/ F | -F | F => F

h \bot = 1
h \top = 1
h (V n) = 1
h (-F) = 1 + h(F)
h (F1 /\ F2) = 1 + max(h(F1),h(F2))
h (F1 \/ F2) = 1 + max(h(F1),h(F2))
h (F1 => F2) = 1 + max(h(F1),h(F2))