]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/tests/paramodulation/BOO075-1.ma
1) added simplification of actives w.r.t. selected
[helm.git] / helm / software / matita / tests / paramodulation / BOO075-1.ma
1
2
3 inductive eq (A:Type) (x:A) : A \to Prop \def refl_eq : eq A x x.
4
5 theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y \to eq A y x.
6 intros.elim H. apply refl_eq.
7 qed.
8
9 theorem eq_elim_r:
10  \forall A:Type.\forall x:A. \forall P: A \to Prop.
11    P x \to \forall y:A. eq A y x \to P y.
12 intros. elim (sym_eq ? ? ? H1).assumption.
13 qed.
14
15 theorem eq_elim_r':
16  \forall A:Type.\forall x:A. \forall P: A \to Set.
17    P x \to \forall y:A. eq A y x \to P y.
18 intros. elim (sym_eq ? ? ? H).assumption.
19 qed.
20
21 theorem eq_elim_r'':
22  \forall A:Type.\forall x:A. \forall P: A \to Type.
23    P x \to \forall y:A. eq A y x \to P y.
24 intros. elim (sym_eq ? ? ? H).assumption.
25 qed.
26
27 theorem trans_eq : 
28     \forall A:Type.\forall x,y,z:A. eq A x y \to eq A y z \to eq A x z.
29 intros.elim H1.assumption.
30 qed.
31
32 default "equality"
33  cic:/matita/tests/paramodulation/BOO075-1/eq.ind
34  cic:/matita/tests/paramodulation/BOO075-1/sym_eq.con
35  cic:/matita/tests/paramodulation/BOO075-1/trans_eq.con
36  cic:/matita/tests/paramodulation/BOO075-1/eq_ind.con
37  cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r.con
38  cic:/matita/tests/paramodulation/BOO075-1/eq_rec.con
39  cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r'.con
40  cic:/matita/tests/paramodulation/BOO075-1/eq_rect.con
41  cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r''.con
42  cic:/matita/tests/paramodulation/BOO075-1/eq_f.con
43  cic:/matita/tests/paramodulation/BOO075-1/eq_f1.con.
44
45 theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
46   \forall x,y:A. eq A x y \to eq B (f x) (f y).
47 intros.elim H.reflexivity.
48 qed.
49
50 theorem eq_f1: \forall  A,B:Type.\forall f:A\to B.
51   \forall x,y:A. eq A x y \to eq B (f y) (f x).
52 intros.elim H.reflexivity.
53 qed.
54
55 inductive ex (A:Type) (P:A \to Prop) : Prop \def
56     ex_intro: \forall x:A. P x \to ex A P.
57 interpretation "exists" 'exists \eta.x =
58   (cic:/matita/tests/paramodulation/BOO075-1/ex.ind#xpointer(1/1) _ x).
59
60 notation < "hvbox(\exists ident i opt (: ty) break . p)"
61   right associative with precedence 20
62 for @{ 'exists ${default
63   @{\lambda ${ident i} : $ty. $p)}
64   @{\lambda ${ident i} . $p}}}.
65
66
67 (* Inclusion of: BOO075-1.p *)
68 (* -------------------------------------------------------------------------- *)
69 (*  File     : BOO075-1 : TPTP v3.1.1. Released v2.6.0. *)
70 (*  Domain   : Boolean Algebra *)
71 (*  Problem  : Sh-1 is a single axiom for Boolean algebra, part 1 *)
72 (*  Version  : [EF+02] axioms. *)
73 (*  English  :  *)
74 (*  Refs     : [EF+02] Ernst et al. (2002), More First-order Test Problems in *)
75 (*           : [MV+02] McCune et al. (2002), Short Single Axioms for Boolean *)
76 (*  Source   : [TPTP] *)
77 (*  Names    :  *)
78 (*  Status   : Unsatisfiable *)
79 (*  Rating   : 0.00 v2.6.0 *)
80 (*  Syntax   : Number of clauses     :    2 (   0 non-Horn;   2 unit;   1 RR) *)
81 (*             Number of atoms       :    2 (   2 equality) *)
82 (*             Maximal clause size   :    1 (   1 average) *)
83 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
84 (*             Number of functors    :    3 (   2 constant; 0-2 arity) *)
85 (*             Number of variables   :    3 (   1 singleton) *)
86 (*             Maximal term depth    :    5 (   2 average) *)
87 (*  Comments : A UEQ part of BOO039-1 *)
88 (* -------------------------------------------------------------------------- *)
89 theorem prove_meredith_2_basis_1:
90  \forall Univ:Set.
91 \forall a:Univ.
92 \forall b:Univ.
93 \forall nand:Univ\rarr Univ\rarr Univ.
94 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (nand (nand A (nand (nand B A) A)) (nand B (nand C A))) B.eq Univ (nand (nand a a) (nand b a)) a
95 .
96 intros.
97 autobatch paramodulation timeout=600;
98 try assumption.
99 print proofterm.
100 qed.
101 (* -------------------------------------------------------------------------- *)