## Numero 2:

F ::= A | B | ... | F /\ F

Problema: riassociare a sx tutte le parentesi
Soluzione: l(F)

l(A) = A
...
l(F1 /\ F2) = a(l(F1),l(F2))

Problema: date F1 e F2 associate a sx
restiture F1 /\ F2 associato a sx
Soluzione: a(F1,F2)
per ricorsione strutturale su F2

a(F1,A) = F1 /\ A
a(F1, F2 /\ A) = a(F1,F2) /\ A

===================================

## Esercizio 7

F ::= A | F /\ F | F => F

Teorema: ||- F  \/  F == A
Dimostrazione:
Per induzione strutturale su F

caso A:
 dimostro  ||- A \/ A == A
 ovvio

caso F1 /\ F2:
 ipotesi induttiva  ||- F1 \/ F1 == A
 ipotesi induttiva  ||- F2 \/ F2 == A
 dimostro
  (||- F1 /\ F2) \/ (F1 /\ F2 == A)
 ovvero
   (||- F1 /\ ||- F2) \/ (F1 /\ F2 == A)
 per casi sulla prima ipotesi induttiva:
   caso  ||- F1:
     per casi sulla seconda ipotesi induttiva
        caso  ||- F2:
          ovvio perchè (||- F1 /\ ||- F2)
        caso  F2 == A:
          ovvio perchè (F1 /\ F2 == A)
          in quanto in ogni mondo v,
            [| F1 /\ F2 |]v
          = min { [|F1|]v, [|F2|]v }
          = min { 1, [|A|]v }
          = [|A|]v
   caso F1 == A:
     per casi sulla seconda ipotesi induttiva
        caso  ||- F2:
          ovvio perchè (F1 /\ F2 == A)
          in quanto in ogni mondo v,
            [| F1 /\ F2 |]v
          = min { [|F1|]v, [|F2|]v }
          = min { [|A|]v, 1 }
          = [|A|]v
        caso F2 == A:
          ovvio perchè (F1 /\ F2 == A)
          in quanto in ogni mondo v,
            [| F1 /\ F2 |]v
          = min { [|F1|]v, [|F2|]v }
          = min { [|A|]v, [|A|]v }
          = [|A|]v