X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdidactic%2Fshannon.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdidactic%2Fshannon.ma;h=d88f46ad76f45f2bdaa3f47a080901f05b6c0dd2;hb=4257ad7d31bc2db6c40ad55878f190963e51c1ec;hp=be31459eba4f78964e5672ff092dd13e93d322f2;hpb=87fdda71e8e0dcf886852f70be9a4b3d627b8e9c;p=helm.git

diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma
index be31459eb..d88f46ad7 100644
--- a/helm/software/matita/contribs/didactic/shannon.ma
+++ b/helm/software/matita/contribs/didactic/shannon.ma
@@ -212,10 +212,10 @@ case FAnd.
   case Left.
     by H3, H we proved 
       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 0 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
@@ -230,10 +230,10 @@ case FAnd.
   case Right.
     by H3, H we proved 
       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 1 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
@@ -258,10 +258,10 @@ case FOr.
   case Left.
     by H3, H we proved 
       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 0 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
@@ -276,10 +276,10 @@ case FOr.
   case Right.
     by H3, H we proved 
       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 1 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
@@ -304,10 +304,10 @@ case FImpl.
   case Left.
     by H3, H we proved 
       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 0 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
@@ -322,10 +322,10 @@ case FImpl.
   case Right.
     by H3, H we proved 
       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 1 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
@@ -348,7 +348,7 @@ case FNot.
   case Left.
     by H1, H we proved 
       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
+    by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
       = ([[ if eqb 0 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.
@@ -362,7 +362,7 @@ case FNot.
   case Right.
     by H1, H we proved 
       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
+    by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
       = ([[ if eqb 1 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.