]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/TPTP/HEQ/LAT001-1.ma
5d32be12d8d45ab4ef5f97c0d1454cc4e7595f43
[helm.git] / matita / matita / contribs / TPTP / HEQ / LAT001-1.ma
1 set "baseuri" "cic:/matita/TPTP/LAT001-1".
2 include "logic/equality.ma".
3
4 (* Inclusion of: LAT001-1.p *)
5
6 (* -------------------------------------------------------------------------- *)
7
8 (*  File     : LAT001-1 : TPTP v3.2.0. Released v1.0.0. *)
9
10 (*  Domain   : Lattice Theory *)
11
12 (*  Problem  : If X' = U v V and Y' = U ^ V, then U' = X v (Y ^ V) *)
13
14 (*  Version  : [McC88] (equality) axioms. *)
15
16 (*  English  : The theorem states that there is a complement of "a" in a *)
17
18 (*             modular lattice with 0 and 1. *)
19
20 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
21
22 (*           : [GO+69] Guard et al. (1969), Semi-Automated Mathematics *)
23
24 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
25
26 (*  Source   : [McC88] *)
27
28 (*  Names    : L1a [McC88] *)
29
30 (*  Status   : Unsatisfiable *)
31
32 (*  Rating   : 0.71 v3.2.0, 0.57 v3.1.0, 0.78 v2.7.0, 0.83 v2.6.0, 0.86 v2.5.0, 1.00 v2.0.0 *)
33
34 (*  Syntax   : Number of clauses     :   19 (   0 non-Horn;  15 unit;   6 RR) *)
35
36 (*             Number of atoms       :   24 (  18 equality) *)
37
38 (*             Maximal clause size   :    3 (   1 average) *)
39
40 (*             Number of predicates  :    2 (   0 propositional; 2-2 arity) *)
41
42 (*             Number of functors    :    8 (   6 constant; 0-2 arity) *)
43
44 (*             Number of variables   :   29 (   4 singleton) *)
45
46 (*             Maximal term depth    :    3 (   2 average) *)
47
48 (*  Comments : No further information is available from [McC88] or [GO+69] *)
49
50 (*             about [Bum65]. *)
51
52 (* -------------------------------------------------------------------------- *)
53
54 (* ----Include lattice axioms  *)
55
56 (* Inclusion of: Axioms/LAT001-0.ax *)
57
58 (* -------------------------------------------------------------------------- *)
59
60 (*  File     : LAT001-0 : TPTP v3.2.0. Released v1.0.0. *)
61
62 (*  Domain   : Lattice Theory *)
63
64 (*  Axioms   : Lattice theory (equality) axioms *)
65
66 (*  Version  : [McC88] (equality) axioms. *)
67
68 (*  English  :  *)
69
70 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
71
72 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
73
74 (*           : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr *)
75
76 (*  Source   : [McC88] *)
77
78 (*  Names    :  *)
79
80 (*  Status   :  *)
81
82 (*  Syntax   : Number of clauses    :    8 (   0 non-Horn;   8 unit;   0 RR) *)
83
84 (*             Number of literals   :    8 (   8 equality) *)
85
86 (*             Maximal clause size  :    1 (   1 average) *)
87
88 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
89
90 (*             Number of functors   :    2 (   0 constant; 2-2 arity) *)
91
92 (*             Number of variables  :   16 (   2 singleton) *)
93
94 (*             Maximal term depth   :    3 (   2 average) *)
95
96 (*  Comments :  *)
97
98 (* -------------------------------------------------------------------------- *)
99
100 (* ----The following 8 clauses characterise lattices  *)
101
102 (* -------------------------------------------------------------------------- *)
103
104 (* ----Include modular lattice axioms  *)
105
106 (* Inclusion of: Axioms/LAT001-1.ax *)
107
108 (* -------------------------------------------------------------------------- *)
109
110 (*  File     : LAT001-1 : TPTP v3.2.0. Released v1.0.0. *)
111
112 (*  Domain   : Lattice Theory *)
113
114 (*  Axioms   : Lattice theory modularity (equality) axioms *)
115
116 (*  Version  : [McC88] (equality) axioms. *)
117
118 (*  English  :  *)
119
120 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
121
122 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
123
124 (*           : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr *)
125
126 (*  Source   : [McC88] *)
127
128 (*  Names    :  *)
129
130 (*  Status   :  *)
131
132 (*  Syntax   : Number of clauses    :    5 (   0 non-Horn;   4 unit;   0 RR) *)
133
134 (*             Number of literals   :    6 (   6 equality) *)
135
136 (*             Maximal clause size  :    2 (   1 average) *)
137
138 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
139
140 (*             Number of functors   :    4 (   2 constant; 0-2 arity) *)
141
142 (*             Number of variables  :    7 (   2 singleton) *)
143
144 (*             Maximal term depth   :    3 (   2 average) *)
145
146 (*  Comments : Requires LAT001-0.ax *)
147
148 (*           : These axioms, with 4 extra redundant axioms about 0 & 1, are  *)
149
150 (*             used in [Wos88] p.217. *)
151
152 (* -------------------------------------------------------------------------- *)
153
154 (* ----Include 1 and 0 in the lattice  *)
155
156 (* ----Require the lattice to be modular  *)
157
158 (* -------------------------------------------------------------------------- *)
159
160 (* ----Include definition of complement  *)
161
162 (* Inclusion of: Axioms/LAT001-2.ax *)
163
164 (* -------------------------------------------------------------------------- *)
165
166 (*  File     : LAT001-2 : TPTP v3.2.0. Released v1.0.0. *)
167
168 (*  Domain   : Lattice Theory *)
169
170 (*  Axioms   : Lattice theory complement (equality) axioms *)
171
172 (*  Version  : [McC88] (equality) axioms. *)
173
174 (*  English  :  *)
175
176 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
177
178 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
179
180 (*  Source   : [McC88] *)
181
182 (*  Names    :  *)
183
184 (*  Status   :  *)
185
186 (*  Syntax   : Number of clauses    :    3 (   0 non-Horn;   0 unit;   3 RR) *)
187
188 (*             Number of literals   :    7 (   4 equality) *)
189
190 (*             Maximal clause size  :    3 (   2 average) *)
191
192 (*             Number of predicates :    2 (   0 propositional; 2-2 arity) *)
193
194 (*             Number of functors   :    4 (   2 constant; 0-2 arity) *)
195
196 (*             Number of variables  :    6 (   0 singleton) *)
197
198 (*             Maximal term depth   :    2 (   1 average) *)
199
200 (*  Comments : Requires LAT001-0.ax *)
201
202 (* -------------------------------------------------------------------------- *)
203
204 (* ----Definition of complement  *)
205
206 (* -------------------------------------------------------------------------- *)
207
208 (* -------------------------------------------------------------------------- *)
209 theorem prove_complememt:
210  ∀Univ:Set.∀X:Univ.∀Y:Univ.∀Z:Univ.∀a:Univ.∀b:Univ.∀complement:∀_:Univ.∀_:Univ.Prop.∀join:∀_:Univ.∀_:Univ.Univ.∀meet:∀_:Univ.∀_:Univ.Univ.∀n0:Univ.∀n1:Univ.∀r1:Univ.∀r2:Univ.∀H0:complement r2 (meet a b).∀H1:complement r1 (join a b).∀H2:∀X:Univ.∀Y:Univ.∀_:eq Univ (join X Y) n1.∀_:eq Univ (meet X Y) n0.complement X Y.∀H3:∀X:Univ.∀Y:Univ.∀_:complement X Y.eq Univ (join X Y) n1.∀H4:∀X:Univ.∀Y:Univ.∀_:complement X Y.eq Univ (meet X Y) n0.∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.∀_:eq Univ (meet X Z) X.eq Univ (meet Z (join X Y)) (join X (meet Y Z)).∀H6:∀X:Univ.eq Univ (join X n1) n1.∀H7:∀X:Univ.eq Univ (meet X n1) X.∀H8:∀X:Univ.eq Univ (join X n0) X.∀H9:∀X:Univ.eq Univ (meet X n0) n0.∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join X Y) Z) (join X (join Y Z)).∀H11:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet X Y) Z) (meet X (meet Y Z)).∀H12:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).∀H13:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).∀H14:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.∀H15:∀X:Univ.∀Y:Univ.eq Univ (meet X (join X Y)) X.∀H16:∀X:Univ.eq Univ (join X X) X.∀H17:∀X:Univ.eq Univ (meet X X) X.complement a (join r1 (meet r2 b))
211 .
212 intros.
213 autobatch depth=5 width=5 size=20 timeout=10;
214 try assumption.
215 print proofterm.
216 qed.
217
218 (* -------------------------------------------------------------------------- *)