(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/SK/".
+set "baseuri" "cic:/matita/tests/bool/".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
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.
\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.
\forall x,y:A. zero = (mult x (mult (inv x) y)).
intros.auto paramodulation.
qed.
-
+(*
theorem bool515:
\forall A:Set.
\forall one:A.
\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.
\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.
intros;
auto paramodulation.
qed.
-(* 46 sec. *)
theorem bool756:
\forall A:Set.
[auto paramodulation
|auto paramodulation]
qed.
-(* 186 sec *)
-*)
+
theorem bool756full:
\forall A:Set.
\forall one:A.
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.
\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.
(inv (mult x y)) = (add (inv x) (inv y)).
intros.auto paramodulation.
qed.
-(* 90 *)
theorem bool5hint2:
\forall A:Set.
(inv (mult x y)) = (add (inv x) (inv y)).
intros.auto paramodulation.
qed.
-(* 41 *)
theorem bool5hint3:
\forall A:Set.
(inv (mult x y)) = (add (inv x) (inv y)).
intros.auto paramodulation.
qed.
-(* 41 *)
theorem bool5:
\forall A:Set.
(inv (mult x y)) = (add (inv x) (inv y)).
intros.auto paramodulation.
qed.
+
+*)*)
+