X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction.ma;h=052e00679c98ca5e5fef8018bc46d69d8b610f9b;hb=1118162fa2c7b4dc860da0c3aa434bd2a1631855;hp=8ec8d6fd74407326538e3f780b86f53fe32f95d2;hpb=b14d3611e67633ffa5b661e38331db4ea83ca429;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 8ec8d6fd7..052e00679 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -18,9 +18,57 @@
 
 include "didactic/support/natural_deduction.ma".
 
+theorem EM: ∀A. A ∨ ¬ A.
+assume A: CProp.
+apply rule (prove (A ∨ ¬A));
+apply rule (RAA [H] (⊥)).
+apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+	[ apply rule (discharge [H]).
+	| apply rule (⊥_e (⊥));
+	  apply rule (¬_e (¬¬A) (¬A));
+	   [ apply rule (¬_i [K] (⊥)).
+       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+	      [ apply rule (discharge [H]).
+	      | apply rule (∨_i_r (¬A)).
+          apply rule (discharge [K]).
+	      ]
+	   | apply rule (¬_i [K] (⊥)).
+       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+	      [ apply rule (discharge [H]).
+	      | apply rule (∨_i_l (A)).
+          apply rule (discharge [K]).
+	      ]
+	   ]
+	]
+qed.
 
-
+(*
 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
+apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
+apply rule (⇒_i [H] (¬A ∨ ¬B));
+apply rule (RAA [K] (⊥));
+apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
+	[ apply rule (discharge [K]).
+	| apply rule (∨_i_l (¬A));
+	  apply rule (¬_i [L] (⊥)).
+	  apply rule (¬_e (¬B) (B));
+	   [ apply rule (¬_i [M] (⊥)).
+       apply rule (¬_e (¬(A ∧ B)) (A ∧ B));
+	      [ apply rule (discharge [H]).
+	      | apply rule (∧_i (A) (B));
+	         [ apply rule (discharge [L]).
+	         | apply rule (discharge [M]).
+	         ]
+	      ]
+	   | apply rule (∨_e (B ∨ ¬B) [h1] (B) [h2] (B));
+	       [ apply rule (lem EM);
+	       
 
-
-
+	       | apply rule (discharge [h1]);
+	       |
+	       ]
+ 
+	   apply rule (show EM);
+	   ]
+	]
+*)
\ No newline at end of file