helm/software/matita/contribs/TPTP/HEQ/LAT005-3.ma

   1 set "baseuri" "cic:/matita/TPTP/LAT005-3".
   2 include "logic/equality.ma".
   3
   4 (* Inclusion of: LAT005-3.p *)
   5
   6 (* -------------------------------------------------------------------------- *)
   7
   8 (*  File     : LAT005-3 : TPTP v3.2.0. Released v1.0.0. *)
   9
  10 (*  Domain   : Lattice Theory *)
  11
  12 (*  Problem  : SAM's lemma *)
  13
  14 (*  Version  : [McC88] (equality) axioms. *)
  15
  16 (*  English  : Let L be a modular lattice with 0 and 1.  Suppose that A and  *)
  17
  18 (*             B are elements of L such that (A v B) and (A ^ B) both have  *)
  19
  20 (*             not necessarily unique complements. Then, (A v B)' =  *)
  21
  22 (*             ((A v B)' v ((A ^ B)' ^ B)) ^ ((A v B)' v ((A ^ B)' ^ A)). *)
  23
  24 (*  Refs     : [GO+69] Guard et al. (1969), Semi-Automated Mathematics *)
  25
  26 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
  27
  28 (*  Source   : [McC88] *)
  29
  30 (*  Names    : SAM's lemma [McC88] *)
  31
  32 (*  Status   : Unsatisfiable *)
  33
  34 (*  Rating   : 0.43 v3.2.0, 0.14 v3.1.0, 0.44 v2.7.0, 0.50 v2.6.0, 0.43 v2.5.0, 0.80 v2.4.0, 1.00 v2.3.0, 0.83 v2.2.1, 0.89 v2.2.0, 0.86 v2.1.0, 1.00 v2.0.0 *)
  35
  36 (*  Syntax   : Number of clauses     :   19 (   0 non-Horn;  15 unit;   6 RR) *)
  37
  38 (*             Number of atoms       :   24 (  19 equality) *)
  39
  40 (*             Maximal clause size   :    3 (   1 average) *)
  41
  42 (*             Number of predicates  :    2 (   0 propositional; 2-2 arity) *)
  43
  44 (*             Number of functors    :    8 (   6 constant; 0-2 arity) *)
  45
  46 (*             Number of variables   :   29 (   4 singleton) *)
  47
  48 (*             Maximal term depth    :    4 (   2 average) *)
  49
  50 (*  Comments : [McC88] specifies that the axioms for complement should not be *)
  51
  52 (*             included ("clauses 1-13 from axioms"). However, if this makes *)
  53
  54 (*             clauses 87 and 88 pure. I have assumed a typo in the paper and *)
  55
  56 (*             included axioms 14-16. *)
  57
  58 (* -------------------------------------------------------------------------- *)
  59
  60 (* ----Include lattice axioms  *)
  61
  62 (* Inclusion of: Axioms/LAT001-0.ax *)
  63
  64 (* -------------------------------------------------------------------------- *)
  65
  66 (*  File     : LAT001-0 : TPTP v3.2.0. Released v1.0.0. *)
  67
  68 (*  Domain   : Lattice Theory *)
  69
  70 (*  Axioms   : Lattice theory (equality) axioms *)
  71
  72 (*  Version  : [McC88] (equality) axioms. *)
  73
  74 (*  English  :  *)
  75
  76 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
  77
  78 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
  79
  80 (*           : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr *)
  81
  82 (*  Source   : [McC88] *)
  83
  84 (*  Names    :  *)
  85
  86 (*  Status   :  *)
  87
  88 (*  Syntax   : Number of clauses    :    8 (   0 non-Horn;   8 unit;   0 RR) *)
  89
  90 (*             Number of literals   :    8 (   8 equality) *)
  91
  92 (*             Maximal clause size  :    1 (   1 average) *)
  93
  94 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
  95
  96 (*             Number of functors   :    2 (   0 constant; 2-2 arity) *)
  97
  98 (*             Number of variables  :   16 (   2 singleton) *)
  99
 100 (*             Maximal term depth   :    3 (   2 average) *)
 101
 102 (*  Comments :  *)
 103
 104 (* -------------------------------------------------------------------------- *)
 105
 106 (* ----The following 8 clauses characterise lattices  *)
 107
 108 (* -------------------------------------------------------------------------- *)
 109
 110 (* ----Include modular lattice axioms  *)
 111
 112 (* Inclusion of: Axioms/LAT001-1.ax *)
 113
 114 (* -------------------------------------------------------------------------- *)
 115
 116 (*  File     : LAT001-1 : TPTP v3.2.0. Released v1.0.0. *)
 117
 118 (*  Domain   : Lattice Theory *)
 119
 120 (*  Axioms   : Lattice theory modularity (equality) axioms *)
 121
 122 (*  Version  : [McC88] (equality) axioms. *)
 123
 124 (*  English  :  *)
 125
 126 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
 127
 128 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
 129
 130 (*           : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr *)
 131
 132 (*  Source   : [McC88] *)
 133
 134 (*  Names    :  *)
 135
 136 (*  Status   :  *)
 137
 138 (*  Syntax   : Number of clauses    :    5 (   0 non-Horn;   4 unit;   0 RR) *)
 139
 140 (*             Number of literals   :    6 (   6 equality) *)
 141
 142 (*             Maximal clause size  :    2 (   1 average) *)
 143
 144 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
 145
 146 (*             Number of functors   :    4 (   2 constant; 0-2 arity) *)
 147
 148 (*             Number of variables  :    7 (   2 singleton) *)
 149
 150 (*             Maximal term depth   :    3 (   2 average) *)
 151
 152 (*  Comments : Requires LAT001-0.ax *)
 153
 154 (*           : These axioms, with 4 extra redundant axioms about 0 & 1, are  *)
 155
 156 (*             used in [Wos88] p.217. *)
 157
 158 (* -------------------------------------------------------------------------- *)
 159
 160 (* ----Include 1 and 0 in the lattice  *)
 161
 162 (* ----Require the lattice to be modular  *)
 163
 164 (* -------------------------------------------------------------------------- *)
 165
 166 (* ----Include definition of complement  *)
 167
 168 (* Inclusion of: Axioms/LAT001-2.ax *)
 169
 170 (* -------------------------------------------------------------------------- *)
 171
 172 (*  File     : LAT001-2 : TPTP v3.2.0. Released v1.0.0. *)
 173
 174 (*  Domain   : Lattice Theory *)
 175
 176 (*  Axioms   : Lattice theory complement (equality) axioms *)
 177
 178 (*  Version  : [McC88] (equality) axioms. *)
 179
 180 (*  English  :  *)
 181
 182 (*  Refs     : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
 183
 184 (*           : [McC88] McCune (1988), Challenge Equality Problems in Lattice  *)
 185
 186 (*  Source   : [McC88] *)
 187
 188 (*  Names    :  *)
 189
 190 (*  Status   :  *)
 191
 192 (*  Syntax   : Number of clauses    :    3 (   0 non-Horn;   0 unit;   3 RR) *)
 193
 194 (*             Number of literals   :    7 (   4 equality) *)
 195
 196 (*             Maximal clause size  :    3 (   2 average) *)
 197
 198 (*             Number of predicates :    2 (   0 propositional; 2-2 arity) *)
 199
 200 (*             Number of functors   :    4 (   2 constant; 0-2 arity) *)
 201
 202 (*             Number of variables  :    6 (   0 singleton) *)
 203
 204 (*             Maximal term depth   :    2 (   1 average) *)
 205
 206 (*  Comments : Requires LAT001-0.ax *)
 207
 208 (* -------------------------------------------------------------------------- *)
 209
 210 (* ----Definition of complement  *)
 211
 212 (* -------------------------------------------------------------------------- *)
 213
 214 (* -------------------------------------------------------------------------- *)
 215 theorem prove_lemma:
 216  ∀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.eq Univ r1 (meet (join r1 (meet r2 b)) (join r1 (meet r2 a)))
 217 .
 218 intros.
 219 autobatch depth=5 width=5 size=20 timeout=10;
 220 try assumption.
 221 print proofterm.
 222 qed.
 223
 224 (* -------------------------------------------------------------------------- *)