using the new by foo we proved semantics

[helm.git] / helm / software / matita / contribs / didactic / shannon.ma

diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma
index be31459eba4f78964e5672ff092dd13e93d322f2..d88f46ad76f45f2bdaa3f47a080901f05b6c0dd2 100644 (file)
--- 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.