X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction1.ma;h=4a65968db6159a0a96b62a7e879455ff47e27929;hb=e91eb82d2b5e032907758bff0b474d62d57463dc;hp=8f90dd67c20305403c0dda77b0e63f20b1d9ba2e;hpb=ece1166d5202b74ee25bdceef1b4951de979a99b;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction1.ma b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
index 8f90dd67c..4a65968db 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
@@ -1,3 +1,17 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
 (* Istruzioni: 
 
      http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html 
@@ -27,20 +41,20 @@ theorem EM: ∀A:CProp. A ∨ ¬ A.
 assume A: CProp.
 apply rule (prove (A ∨ ¬A));
 apply rule (RAA [H] (⊥)).
-apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+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 (⊥#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 (∨#i_r (¬A)).
           apply rule (discharge [K]).
 	      ]
-	   | apply rule (¬_i [K] (⊥)).
-       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+	   | apply rule (¬#i [K] (⊥)).
+       apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 	      [ apply rule (discharge [H]).
-	      | apply rule (∨_i_l (A)).
+	      | apply rule (∨#i_l (A)).
           apply rule (discharge [K]).
 	      ]
 	   ]
@@ -50,29 +64,29 @@ qed.
 theorem ex0 : (F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E.
 apply rule (prove ((F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
 (*BEGIN*)
-apply rule (⇒_i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
-apply rule (⇒_i [h2] (F ∧ L ⇒ E));
-apply rule (⇒_i [h3] (E));
-apply rule (∨_e (G∨¬G) [h4] (E) [h4] (E));
-	[ apply rule (lem EM);
-	| apply rule (⇒_e (G∧L⇒E) (G∧L));
+apply rule (⇒#i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
+apply rule (⇒#i [h2] (F ∧ L ⇒ E));
+apply rule (⇒#i [h3] (E));
+apply rule (∨#e (G∨¬G) [h4] (E) [h4] (E));
+	[ apply rule (lem 0 EM);
+	| apply rule (⇒#e (G∧L⇒E) (G∧L));
 	    [ apply rule (discharge [h2]);
-	    | apply rule (∧_i (G) (L));
+	    | apply rule (∧#i (G) (L));
 	        [ apply rule (discharge [h4]);
-	        | apply rule (∧_e_r (F∧L));
+	        | apply rule (∧#e_r (F∧L));
 	          apply rule (discharge [h3]);
 	        ]
 	    ]
-	| apply rule (⇒_e (L⇒E) (L));
-	    [ apply rule (⇒_e (F∧¬G ⇒ L ⇒ E) (F∧¬G));
+	| apply rule (⇒#e (L⇒E) (L));
+	    [ apply rule (⇒#e (F∧¬G ⇒ L ⇒ E) (F∧¬G));
 	        [ apply rule (discharge [h1]);
-	        | apply rule (∧_i (F) (¬G));
-	            [ apply rule (∧_e_l (F∧L));
+	        | apply rule (∧#i (F) (¬G));
+	            [ apply rule (∧#e_l (F∧L));
 	              apply rule (discharge [h3]);
 	            | apply rule (discharge [h4]);
 	            ]
 	        ]  
-	    | apply rule (∧_e_r (F∧L));
+	    | apply rule (∧#e_r (F∧L));
 	      apply rule (discharge [h3]);
 	    ]
 	]
@@ -82,29 +96,29 @@ qed.
 theorem ex1 : (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E.
 apply rule (prove (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E);
 (*BEGIN*)
-apply rule (⇒_i [h1] ((G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E));
-apply rule (⇒_i [h2] ((¬L ∨ F) ⇒ L ⇒ E));
-apply rule (⇒_i [h3] (L ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (¬L∨F) [h5] (E) [h5] (E));
+apply rule (⇒#i [h1] ((G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E));
+apply rule (⇒#i [h2] ((¬L ∨ F) ⇒ L ⇒ E));
+apply rule (⇒#i [h3] (L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (¬L∨F) [h5] (E) [h5] (E));
 	[ apply rule (discharge [h3]);
-	| apply rule (⊥_e (⊥));
-    apply rule (¬_e (¬L) (L));
+	| apply rule (⊥#e (⊥));
+    apply rule (¬#e (¬L) (L));
 	    [ apply rule (discharge [h5]);
 	    | apply rule (discharge [h4]);
 	    ]
-	| apply rule (∨_e (G∨E) [h6] (E) [h6] (E));
-	   [ apply rule (⇒_e (F⇒G∨E) (F));
+	| apply rule (∨#e (G∨E) [h6] (E) [h6] (E));
+	   [ apply rule (⇒#e (F⇒G∨E) (F));
 	      [ apply rule (discharge [h1]);
 	      | apply rule (discharge [h5]);
 	      ]
 	   | apply rule (RAA [h7] (⊥));
-       apply rule (¬_e (¬ (L ∧ ¬E)) (L ∧ ¬E));
-	       [ apply rule (⇒_e (G ⇒ ¬ (L ∧ ¬E)) (G));
+       apply rule (¬#e (¬ (L ∧ ¬E)) (L ∧ ¬E));
+	       [ apply rule (⇒#e (G ⇒ ¬ (L ∧ ¬E)) (G));
 	           [apply rule (discharge [h2]);
 	           |apply rule (discharge [h6]);
 	           ]
-	       | apply rule (∧_i (L) (¬E));
+	       | apply rule (∧#i (L) (¬E));
 	           [ apply rule (discharge [h4]);
 	           | apply rule (discharge [h7]);
 	           ]
@@ -118,29 +132,29 @@ qed.
 theorem ex2 : (F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E.
 apply rule (prove ((F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
 (*BEGIN*)
-apply rule (⇒_i [h1] ((H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
-apply rule (⇒_i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
-apply rule (⇒_i [h3] (H ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (G∨¬G) [h5] (E) [h5] (E));
-	[apply rule (lem EM);
-	| apply rule (∨_e (E∨F) [h6] (E) [h6] (E));
-	   [ apply rule (⇒_e (H ⇒ E∨F) (H));
+apply rule (⇒#i [h1] ((H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
+apply rule (⇒#i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
+apply rule (⇒#i [h3] (H ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨¬G) [h5] (E) [h5] (E));
+	[apply rule (lem 0 EM);
+	| apply rule (∨#e (E∨F) [h6] (E) [h6] (E));
+	   [ apply rule (⇒#e (H ⇒ E∨F) (H));
 	       [ apply rule (discharge [h2]);
 	       | apply rule (discharge [h4]);
 	       ]
 	   | apply rule (discharge [h6]);
-	   | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
+	   | apply rule (⇒#e (F∧G ⇒ E) (F∧G));
 	      [apply rule (discharge [h1]);
-	      |apply rule (∧_i (F) (G));
+	      |apply rule (∧#i (F) (G));
 	        [ apply rule (discharge [h6]);
 	        | apply rule (discharge [h5]);
 	        ]
 	      ]
 	   ]
-	| apply rule (⊥_e (⊥));
-    apply rule (¬_e (¬H) (H));
-    	[ apply rule (⇒_e (¬G ⇒ ¬H) (¬G));
+	| apply rule (⊥#e (⊥));
+    apply rule (¬#e (¬H) (H));
+    	[ apply rule (⇒#e (¬G ⇒ ¬H) (¬G));
 	       [ apply rule (discharge [h3]);
 	       | apply rule (discharge [h5]);
 	       ]
@@ -153,22 +167,22 @@ qed.
 theorem ex3 : (F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E.
 apply rule (prove ((F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E)).
 (*BEGIN*)
-apply rule (⇒_i [h1] ((¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E));
-apply rule (⇒_i [h2] ((L ⇒ F) ⇒ L ⇒ E));
-apply rule (⇒_i [h3] (L ⇒ E));
-apply rule (⇒_i [h4] (E));
+apply rule (⇒#i [h1] ((¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E));
+apply rule (⇒#i [h2] ((L ⇒ F) ⇒ L ⇒ E));
+apply rule (⇒#i [h3] (L ⇒ E));
+apply rule (⇒#i [h4] (E));
 apply rule (RAA [h5] (⊥));
-apply rule (∨_e (G∨¬L) [h6] (⊥) [h6] (⊥));
-	[ apply rule (⇒_e (¬E ⇒ G∨¬L) (¬E));
+apply rule (∨#e (G∨¬L) [h6] (⊥) [h6] (⊥));
+	[ apply rule (⇒#e (¬E ⇒ G∨¬L) (¬E));
 	    [ apply rule (discharge [h2]);
 	    | apply rule (discharge [h5]);
 	    ]
-	| apply rule (¬_e (¬E) (E));
+	| apply rule (¬#e (¬E) (E));
     	[ apply rule (discharge [h5]);
-	    | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
+	    | apply rule (⇒#e (F∧G ⇒ E) (F∧G));
 	       [ apply rule (discharge [h1]);
-	       | apply rule (∧_i (F) (G));
-	           [ apply rule (⇒_e (L⇒F) (L));
+	       | apply rule (∧#i (F) (G));
+	           [ apply rule (⇒#e (L⇒F) (L));
 	              [ apply rule (discharge [h3]);
 	              | apply rule (discharge [h4]);
 	              ]
@@ -176,10 +190,10 @@ apply rule (∨_e (G∨¬L) [h6] (⊥) [h6] (⊥));
 	           ]
 	       ]
 	    ]
-	| apply rule (¬_e (¬L) (L));
+	| apply rule (¬#e (¬L) (L));
 	    [ apply rule (discharge [h6]);
 	    | apply rule (discharge [h4]);
 	    ]
 	]
 (*END*)
-qed.
\ No newline at end of file
+qed.