+ Nome2: ...
+ Cognome2: ...
+ Matricola2: ...
+ Account2: ...
+
+ Prima di abbandonare la postazione:
+
+ * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella)
+ /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui
+ account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma
+
+ * mandatevi via email o stampate il file. Per stampare potete usare
+ usare l'editor gedit che offre la funzionalità di stampa
+*)
+
+(*DOCBEGIN
+
+Il teorema di dualità
+=====================
+
+Il teorema di dualizzazione dice che date due formule `F1` ed `F2`,
+se le due formule sono equivalenti (`F1 ≡ F2`) allora anche le
+loro dualizzate lo sono (`dualize F1 ≡ dualize F2`).
+
+L'ingrediente principale è la funzione di dualizzazione di una formula `F`:
+
+ * Scambia FTop con FBot e viceversa
+
+ * Scambia il connettivo FAnd con FOr e viceversa
+
+ * Sostituisce il connettivo FImpl con FAnd e nega la
+ prima sottoformula.
+
+ Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in
+ `¬A ∧ (B ∨ ⊤)`.
+
+Per dimostrare il teorema di dualizzazione in modo agevole è necessario
+definire altre nozioni:
+
+* La funzione `negate` che presa una formula `F` ne nega gli atomi.
+ Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare `¬A ∨ (⊤ → ¬B)`.
+
+* La funzione `invert` permette di invertire un mondo `v`.
+ Ovvero, per ogni indice di atomo `i`, se `v i` restituisce
+ `1` allora `(invert v) i` restituisce `0` e viceversa.
+
+DOCEND*)
+
+(* ATTENZIONE
+ ==========
+
+ Non modificare quanto segue
+*)
+include "nat/minus.ma".