X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction_theories.ma;h=9768e26e2997da01f7c6b1da99a4cdff2ae1c174;hb=060864edadf332c07663e85bdc2299ee64e191ee;hp=d955bd1248441bd0b762e14e198baada68ea71ed;hpb=e18929311cce5baed9bccd9f1de050180f336ed1;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
index d955bd124..9768e26e2 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.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         *)
+(*                                                                        *)
+(**************************************************************************)
+
 (* Esercizio 0
    ===========
 
@@ -57,7 +71,7 @@ L'albero si descrive partendo dalla radice. Le regole
 con premesse multiple sono seguite da `[`, `|` e `]`.
 Ad esempio: 
 
-        apply rule (∧_i (A∨B) ⊥);
+        apply rule (∧#i (A∨B) ⊥);
           [ …continua qui il sottoalbero per (A∨B)
           | …continua qui il sottoalbero per ⊥
           ] 
@@ -67,7 +81,7 @@ gli argomenti delle regole sono le formule che normalmente
 scrivete sopra la linea che rappresenta l'applicazione della
 regola stessa. Ad esempio:
 
-        apply rule (∨_e (A∨B) [h1] C [h2] C);
+        apply rule (∨#e (A∨B) [h1] C [h2] C);
           [ …prova di (A∨B)
           | …prova di C sotto l'ipotesi A (di nome h1)  
           | …prova di C sotto l'ipotesi B (di nome h2)
@@ -224,27 +238,27 @@ apply rule (prove (∀x.x + O = x));
    l'unica forma di `apply rule lem` che potete usare è 
    `apply rule (lem 0 nome_assioma)` *)
 (*BEGIN*)
-apply rule (⇒_e ((∀n.(n + O) = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (∀n.(n + O) = n ⇒ ((S n) + O) = (S n)));
-	[ apply rule (⇒_e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
+apply rule (⇒#e ((∀n.(n + O) = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (∀n.(n + O) = n ⇒ ((S n) + O) = (S n)));
+	[ apply rule (⇒#e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
 	   [ apply rule (lem 0 induct);
-	   | apply rule (∀_e {O} (∀y.(O + y) =y));
+	   | apply rule (∀#e {O} (∀y.(O + y) =y));
 	     apply rule (lem 0 plus_O);
 	   ]
-	| apply rule (∀_i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
-    apply rule (⇒_i [H] (((S n) + O) = (S n)));
-    apply rule (⇒_e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
-	   [ apply rule (⇒_e (((S n) + O) =(S (n + O)) ⇒ (S (n + O)) = (S n)⇒((S n) + O) =(S n)) (((S n) + O) =(S (n + O))));
-	      [ apply rule (∀_e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
-	        apply rule (∀_e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
-          apply rule (∀_e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
+	| apply rule (∀#i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
+    apply rule (⇒#i [H] (((S n) + O) = (S n)));
+    apply rule (⇒#e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
+	   [ apply rule (⇒#e (((S n) + O) =(S (n + O)) ⇒ (S (n + O)) = (S n)⇒((S n) + O) =(S n)) (((S n) + O) =(S (n + O))));
+	      [ apply rule (∀#e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
+	        apply rule (∀#e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
+          apply rule (∀#e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
           apply rule (lem 0 trans);
-	      | apply rule (∀_e {O} (∀m.(S n) + m = (S (n + m))));
-          apply rule (∀_e {n} (∀n.∀m.(S n) + m = (S (n + m))));
+	      | apply rule (∀#e {O} (∀m.(S n) + m = (S (n + m))));
+          apply rule (∀#e {n} (∀n.∀m.(S n) + m = (S (n + m))));
           apply rule (lem 0 plus_S);
 	      ]
-	   | apply rule (⇒_e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
-	      [ apply rule (∀_e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
-          apply rule (∀_e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));
+	   | apply rule (⇒#e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
+	      [ apply rule (∀#e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
+          apply rule (∀#e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));
           apply rule (lem 0 eq_S);
 	      | apply rule (discharge [H]);
 	      ]