diff --git a/anno2/mie/Mcad/ScalettaMCAD.txt b/anno2/mie/Mcad/ScalettaMCAD.txt
index a3e442f..ee74216 100644
--- a/anno2/mie/Mcad/ScalettaMCAD.txt
+++ b/anno2/mie/Mcad/ScalettaMCAD.txt
@@ -1,11 +1,10 @@
-Introduzione al problema con esempi
-Equivalenza fra modelli con cenni di dimostrazione
-Definizione agreement
-Well-formedness, validity, failure free-termination
-Definizione formale problema
-Teorema 21.2 con dimostrazione
-Algoritmo randomizzato definizione
-Algoritmo di BenOr
-Ottimizzazioni per BenOr
-Failure detector
-Modellazione failure detector
\ No newline at end of file
+Introduzione al problema con esempi
+Equivalenza fra modelli con cenni di dimostrazione
+Definizione agreement e Definizione formale problema
+Well-formedness, validity, failure free-termination
+Teorema 21.2 con dimostrazione -> vedi p 586, dimostrazione in termini degli altri due teoremi
+Algoritmo randomizzato definizione
+Algoritmo di BenOr
+Ottimizzazioni per BenOr
+Failure detector
+Modellazione failure detector
diff --git a/anno2/mie/Mcad/ben1983another.pdf b/anno2/mie/Mcad/ben1983another.pdf
new file mode 100644
index 0000000..4a1eef4
Binary files /dev/null and b/anno2/mie/Mcad/ben1983another.pdf differ
diff --git a/anno2/mie/Mcad/benor.odp b/anno2/mie/Mcad/benor.odp
index f636c59..2fd99ea 100644
Binary files a/anno2/mie/Mcad/benor.odp and b/anno2/mie/Mcad/benor.odp differ
diff --git a/anno2/mie/Mcad/relazione_mcad.md b/anno2/mie/Mcad/relazione_mcad.md
index 25d09dc..9976f33 100644
--- a/anno2/mie/Mcad/relazione_mcad.md
+++ b/anno2/mie/Mcad/relazione_mcad.md
@@ -64,9 +64,27 @@ Se pensiamo che questa decisione casuale ci porta ad una situazione in cui esist
 Torniamo alla situazione iniziale che si puo` ripetere all'infinito senza portare ad una decisione.
 
 
+# Adversary, Lemma 21.5
+
+Consideriamo l'iterazione s.
+Un processo non fallimentare mantiene un valore v "buono" se almeno f+1 messaggi del tipo ("first", s, *) contengono lo stesso valore v.
+Ci possono essere al piu` due valori buoni.
+(Se c'e` un solo valore buono v allora in ogni messaggio del tipo ("second", s, *) contiene il valore null o il valore v.)
+(Se se ci sono due valore buoni allora in ogni messaggio del tipo ("second", s, *) contiene il valore null e x viene scelto a caso.)
+
+Nel caso in cui vi sia un solo valore buono, allora con probabilita` 1/2^n tutti i processi sceglieranno un valore x identico al valore buono.
+Allo stesso modo, nel caso ci fossero due valori buoni, con probabilita` 1/2^n tutti i processi sceglieranno lo stesso valore x.
+(In entrambi i casi i processi avranno lo stesso valore x con probabilita` 1/2^n.)
+Dato che le probabilita` ad ogni iterazione sono indipendenti, possiamo combinarle per ottenere che:
+1 - (probabilita` che almeno un processo non sia d'accordo su ogni iterazione) = 1 - (1 - 1/2^n)^s, ovvero la probabilita` che i processi decidano allo stage s+1.
+
+
+
+
+
+
 Aggiunte:
 Aguilera: 
-- Nel paper si mostra (in maniera intuitiva) perche` la probabilita` di terminazione e` 1.
 - C'e` una variante dove alla fine della fase 2 viene lanciato un "global coin", ovvero il numero casuale e` lo stesso per tutti i processi che lo richiedono.
 Questo accorcia di molto il tempo di esecuzione del programma a costo di avere n/3 < f < n/2 .
 - Lo scopo del paper e` di dimostrare che BenOr funzion con n >= 2f  (piuttosto che 3f per la Lynch)