matita/matita/contribs/TPTP/HEQ/LAT002-1.ma

   1 set "baseuri" "cic:/matita/TPTP/LAT002-1".
   2 include "logic/equality.ma".
   3
   4 (* Inclusion of: LAT002-1.p *)
   5
   6 (* -------------------------------------------------------------------------- *)
   7
   8 (*  File     : LAT002-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' exists *)
  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    : L1b [McC88] *)
  29
  30 (*  Status   : Unsatisfiable *)
  31
  32 (*  Rating   : 0.43 v3.1.0, 0.78 v2.7.0, 0.83 v2.6.0, 0.71 v2.5.0, 1.00 v2.4.0, 0.83 v2.2.1, 0.89 v2.2.0, 0.86 v2.1.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   :   30 (   5 singleton) *)
  45
  46 (*             Maximal term depth    :    3 (   2 average) *)
  47
  48 (*  Comments :  *)
  49
  50 (* -------------------------------------------------------------------------- *)
  51
  52 (* ----Include lattice axioms  *)
  53
  54 (* Inclusion of: Axioms/LAT001-0.ax *)
  55
  56 (* -------------------------------------------------------------------------- *)
  57
  58 (*  File     : LAT001-0 : TPTP v3.2.0. Released v1.0.0. *)
  59
  60 (*  Domain   : Lattice Theory *)
  61
  62 (*  Axioms   : Lattice theory (equality) axioms *)
  63
  64 (*  Version  : [McC88] (equality) axioms. *)
  65
  66 (*  English  :  *)
  67
  68 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
  69
  70 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
  71
  72 (*           : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr *)
  73
  74 (*  Source   : [McC88] *)
  75
  76 (*  Names    :  *)
  77
  78 (*  Status   :  *)
  79
  80 (*  Syntax   : Number of clauses    :    8 (   0 non-Horn;   8 unit;   0 RR) *)
  81
  82 (*             Number of literals   :    8 (   8 equality) *)
  83
  84 (*             Maximal clause size  :    1 (   1 average) *)
  85
  86 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
  87
  88 (*             Number of functors   :    2 (   0 constant; 2-2 arity) *)
  89
  90 (*             Number of variables  :   16 (   2 singleton) *)
  91
  92 (*             Maximal term depth   :    3 (   2 average) *)
  93
  94 (*  Comments :  *)
  95
  96 (* -------------------------------------------------------------------------- *)
  97
  98 (* ----The following 8 clauses characterise lattices  *)
  99
 100 (* -------------------------------------------------------------------------- *)
 101
 102 (* ----Include modular lattice axioms  *)
 103
 104 (* Inclusion of: Axioms/LAT001-1.ax *)
 105
 106 (* -------------------------------------------------------------------------- *)
 107
 108 (*  File     : LAT001-1 : TPTP v3.2.0. Released v1.0.0. *)
 109
 110 (*  Domain   : Lattice Theory *)
 111
 112 (*  Axioms   : Lattice theory modularity (equality) axioms *)
 113
 114 (*  Version  : [McC88] (equality) axioms. *)
 115
 116 (*  English  :  *)
 117
 118 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
 119
 120 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
 121
 122 (*           : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr *)
 123
 124 (*  Source   : [McC88] *)
 125
 126 (*  Names    :  *)
 127
 128 (*  Status   :  *)
 129
 130 (*  Syntax   : Number of clauses    :    5 (   0 non-Horn;   4 unit;   0 RR) *)
 131
 132 (*             Number of literals   :    6 (   6 equality) *)
 133
 134 (*             Maximal clause size  :    2 (   1 average) *)
 135
 136 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
 137
 138 (*             Number of functors   :    4 (   2 constant; 0-2 arity) *)
 139
 140 (*             Number of variables  :    7 (   2 singleton) *)
 141
 142 (*             Maximal term depth   :    3 (   2 average) *)
 143
 144 (*  Comments : Requires LAT001-0.ax *)
 145
 146 (*           : These axioms, with 4 extra redundant axioms about 0 & 1, are  *)
 147
 148 (*             used in [Wos88] p.217. *)
 149
 150 (* -------------------------------------------------------------------------- *)
 151
 152 (* ----Include 1 and 0 in the lattice  *)
 153
 154 (* ----Require the lattice to be modular  *)
 155
 156 (* -------------------------------------------------------------------------- *)
 157
 158 (* ----Include definition of complement  *)
 159
 160 (* Inclusion of: Axioms/LAT001-2.ax *)
 161
 162 (* -------------------------------------------------------------------------- *)
 163
 164 (*  File     : LAT001-2 : TPTP v3.2.0. Released v1.0.0. *)
 165
 166 (*  Domain   : Lattice Theory *)
 167
 168 (*  Axioms   : Lattice theory complement (equality) axioms *)
 169
 170 (*  Version  : [McC88] (equality) axioms. *)
 171
 172 (*  English  :  *)
 173
 174 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
 175
 176 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
 177
 178 (*  Source   : [McC88] *)
 179
 180 (*  Names    :  *)
 181
 182 (*  Status   :  *)
 183
 184 (*  Syntax   : Number of clauses    :    3 (   0 non-Horn;   0 unit;   3 RR) *)
 185
 186 (*             Number of literals   :    7 (   4 equality) *)
 187
 188 (*             Maximal clause size  :    3 (   2 average) *)
 189
 190 (*             Number of predicates :    2 (   0 propositional; 2-2 arity) *)
 191
 192 (*             Number of functors   :    4 (   2 constant; 0-2 arity) *)
 193
 194 (*             Number of variables  :    6 (   0 singleton) *)
 195
 196 (*             Maximal term depth   :    2 (   1 average) *)
 197
 198 (*  Comments : Requires LAT001-0.ax *)
 199
 200 (* -------------------------------------------------------------------------- *)
 201
 202 (* ----Definition of complement  *)
 203
 204 (* -------------------------------------------------------------------------- *)
 205
 206 (* -------------------------------------------------------------------------- *)
 207 theorem prove_complememt_exists:
 208  ∀Univ:Set.∀W:Univ.∀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.∃W:Univ.complement a W
 209 .
 210 intros.
 211 exists[
 212 2:
 213 autobatch depth=5 width=5 size=20 timeout=10;
 214 try assumption.
 215 |
 216 skip]
 217 print proofterm.
 218 qed.
 219
 220 (* -------------------------------------------------------------------------- *)