X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Ftests%2Fbool.ma;h=2b7f815b98afb95e5fb19c90ffe2e6b85a1b52a5;hb=219834c0e605004a33cae194f1216c0b877b8ab4;hp=1b095204629781cda43c51e4677ff7ef65f5de0f;hpb=68f83007f739910e86e41aaa804b59d61a6860d0;p=helm.git

diff --git a/matita/tests/bool.ma b/matita/tests/bool.ma
index 1b0952046..2b7f815b9 100644
--- a/matita/tests/bool.ma
+++ b/matita/tests/bool.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/SK/".
+set "baseuri" "cic:/matita/tests/bool/".
 
 include "legacy/coq.ma".
 
@@ -22,6 +22,8 @@ alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
 alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
 alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con".
 
+(* 
+
 theorem SKK:
   \forall A:Set.
   \forall app: A \to A \to A.
@@ -118,7 +120,7 @@ theorem bool266:
   \forall x,y:A. (mult x (add (inv x) y)) = (mult x y).
 intros.auto paramodulation.
 qed.
-
+*)
 theorem bool507:
   \forall A:Set.
   \forall one:A.
@@ -139,7 +141,7 @@ theorem bool507:
   \forall x,y:A. zero = (mult x (mult (inv x) y)).
 intros.auto paramodulation.
 qed.
-
+(*
 theorem bool515:
   \forall A:Set.
   \forall one:A.
@@ -241,11 +243,6 @@ theorem bool557:
   \forall i2: (\forall x:A. (mult x one) = x).   
   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
-  (*
-  \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
-  \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)). 
-  \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
-  *)
   \forall x,y:A. 
     inv x =  (add (inv x) (inv (add y x))).
 intros.auto paramodulation.
@@ -268,11 +265,6 @@ theorem bool609:
   \forall i2: (\forall x:A. (mult x one) = x).   
   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
-  (*
-  \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
-  \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)). 
-  \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
-  *)
   \forall x,y:A. 
     inv x =  (add (inv (add y x)) (inv x)).
 intros.auto paramodulation.
@@ -376,7 +368,6 @@ theorem bool756simplified:
 intros;
 auto paramodulation.
 qed.
-(* 46 sec. *)
 
 theorem bool756:
   \forall A:Set.
@@ -409,8 +400,7 @@ cut (mult (add y x) (add x (add y z)) = add x (add y (mult x z)));
 [auto paramodulation
 |auto paramodulation]
 qed.
-(*  186 sec *)
-*)
+
 theorem bool756full:
   \forall A:Set.
   \forall one:A.
@@ -432,9 +422,7 @@ theorem bool756full:
     add x y = add x (add y (mult x z)).
 intros;auto paramodulation.
 qed.
-(* war=5; active 225, maxmeta 172568 *)
-(* war=4; active 249, maxmeta 223220 *)
-(*
+
 theorem bool1164:
   \forall A:Set.
   \forall one:A.
@@ -522,7 +510,7 @@ theorem bool1372:
   \forall x,y,z:A.
     add x (add y z) = add (add x z) y.
 intros.auto paramodulation.
-qed.*)
+qed.
 
 theorem bool381:
   \forall A:Set.
@@ -570,7 +558,6 @@ theorem bool5hint1:
     (inv (mult x y)) = (add (inv x) (inv y)).
 intros.auto paramodulation.
 qed.
-(* 90 *)
 
 theorem bool5hint2:
   \forall A:Set.
@@ -595,7 +582,6 @@ theorem bool5hint2:
     (inv (mult x y)) = (add (inv x) (inv y)).
 intros.auto paramodulation.
 qed.
-(* 41 *)
 
 theorem bool5hint3:
   \forall A:Set.
@@ -620,7 +606,6 @@ theorem bool5hint3:
     (inv (mult x y)) = (add (inv x) (inv y)).
 intros.auto paramodulation.
 qed.
-(* 41 *)
 
 theorem bool5:
   \forall A:Set.
@@ -643,3 +628,6 @@ theorem bool5:
     (inv (mult x y)) = (add (inv x) (inv y)).
 intros.auto paramodulation.
 qed.
+
+*)*)
+