1 include "logic/equality.ma".
3 (* Inclusion of: LAT018-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : LAT018-1 : TPTP v3.7.0. Bugfixed v2.2.1. *)
9 (* Domain : Lattice Theory (Ortholattices) *)
11 (* Problem : E3 holds in Ortholattices. *)
13 (* Version : [McC98b] (equality) axioms. *)
15 (* English : Prove that from ortholattice axioms, one can derive equation E3. *)
17 (* Refs : [McC98a] McCune (1998), Automatic Proofs and Counterexamples f *)
19 (* : [McC98b] McCune (1998), Email to G. Sutcliffe *)
21 (* Source : [McC98b] *)
23 (* Names : OL-3 [McC98b] *)
25 (* Status : Unsatisfiable *)
27 (* Rating : 0.78 v3.4.0, 1.00 v3.3.0, 0.93 v3.1.0, 1.00 v2.2.1 *)
29 (* Syntax : Number of clauses : 11 ( 0 non-Horn; 11 unit; 1 RR) *)
31 (* Number of atoms : 11 ( 11 equality) *)
33 (* Maximal clause size : 1 ( 1 average) *)
35 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
37 (* Number of functors : 7 ( 4 constant; 0-2 arity) *)
39 (* Number of variables : 19 ( 2 singleton) *)
41 (* Maximal term depth : 7 ( 3 average) *)
43 (* Comments : Ortholattice lemmas are included in McCunes original, but have *)
45 (* been removed here. *)
47 (* Bugfixes : v2.2.1 - Bugfix in LAT003-0.ax. *)
49 (* -------------------------------------------------------------------------- *)
51 (* ----Include ortholattice axioms *)
53 (* Inclusion of: Axioms/LAT003-0.ax *)
55 (* -------------------------------------------------------------------------- *)
57 (* File : LAT003-0 : TPTP v3.7.0. Bugfixed v2.2.1. *)
59 (* Domain : Lattice Theory (Ortholattices) *)
61 (* Axioms : Ortholattice theory (equality) axioms *)
63 (* Version : [McC98b] (equality) axioms. *)
67 (* Refs : [McC98a] McCune (1998), Automatic Proofs and Counterexamples f *)
69 (* : [McC98b] McCune (1998), Email to G. Sutcliffe *)
71 (* Source : [McC98b] *)
77 (* Syntax : Number of clauses : 10 ( 0 non-Horn; 10 unit; 0 RR) *)
79 (* Number of atoms : 10 ( 10 equality) *)
81 (* Maximal clause size : 1 ( 1 average) *)
83 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
85 (* Number of functors : 5 ( 2 constant; 0-2 arity) *)
87 (* Number of variables : 19 ( 2 singleton) *)
89 (* Maximal term depth : 4 ( 2 average) *)
93 (* Bugfixes : v2.2.1 - Added clauses top and bottom. *)
95 (* -------------------------------------------------------------------------- *)
97 (* ----Axioms for an Ortholattice: *)
99 (* -------------------------------------------------------------------------- *)
101 (* -------------------------------------------------------------------------- *)
103 (* ----Denial of equation E3 *)
105 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
108 ∀complement:∀_:Univ.Univ.
109 ∀join:∀_:Univ.∀_:Univ.Univ.
110 ∀meet:∀_:Univ.∀_:Univ.Univ.
113 ∀H0:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (complement (join (complement X) (complement Y))).
114 ∀H1:∀X:Univ.∀Y:Univ.eq Univ (join X (join Y (complement Y))) (join Y (complement Y)).
115 ∀H2:∀X:Univ.eq Univ (complement (complement X)) X.
116 ∀H3:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join X Y) Z) (join X (join Y Z)).
117 ∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet X Y) Z) (meet X (meet Y Z)).
118 ∀H5:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
119 ∀H6:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
120 ∀H7:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.
121 ∀H8:∀X:Univ.eq Univ (meet (complement X) X) n0.
122 ∀H9:∀X:Univ.eq Univ (join (complement X) X) n1.eq Univ (join (complement (join (join (meet (complement a) b) (meet (complement a) (complement b))) (meet a (join (complement a) b)))) (join (complement a) b)) n1)
145 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9 ##;
146 ntry (nassumption) ##;
149 (* -------------------------------------------------------------------------- *)