1 include "logic/equality.ma".
3 (* Inclusion of: LAT028-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : LAT028-1 : TPTP v3.7.0. Released v2.2.0. *)
9 (* Domain : Lattice Theory (Weakly Associative Lattices) *)
11 (* Problem : Uniqueness of meet (dually join) in WAL *)
13 (* Version : [MP96] (equality) axioms. *)
15 (* English : Let's say we have a weakly-associative lattice (WAL) with 2 meet *)
17 (* operations, say meet1 and meet2. In other words, {join,meet1} *)
19 (* is a WAL, and {join,meet2} is a WAL. Then, we can prove that the *)
21 (* two meet operations are really the same. *)
23 (* Refs : [McC98] McCune (1998), Email to G. Sutcliffe *)
25 (* : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq *)
27 (* Source : [McC98] *)
29 (* Names : WAL-2 [MP96] *)
31 (* Status : Unsatisfiable *)
33 (* Rating : 0.00 v2.2.1 *)
35 (* Syntax : Number of clauses : 11 ( 0 non-Horn; 11 unit; 1 RR) *)
37 (* Number of atoms : 11 ( 11 equality) *)
39 (* Maximal clause size : 1 ( 1 average) *)
41 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
43 (* Number of functors : 5 ( 2 constant; 0-2 arity) *)
45 (* Number of variables : 21 ( 8 singleton) *)
47 (* Maximal term depth : 4 ( 2 average) *)
51 (* -------------------------------------------------------------------------- *)
53 (* ----Include Weakly Associative Lattices theory (equality) axioms *)
55 (* Inclusion of: Axioms/LAT005-0.ax *)
57 (* ------------------------------------------------------------------------------ *)
59 (* File : LAT005-0 : TPTP v3.7.0. Released v2.2.0. *)
61 (* Domain : Lattice Theory (Weakly Associative Lattices) *)
63 (* Axioms : Weakly Associative Lattices theory (equality) axioms *)
65 (* Version : [McC98b] (equality) axioms. *)
69 (* Refs : [McC98] McCune (1998), Email to G. Sutcliffe *)
71 (* : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq *)
73 (* Source : [McC98] *)
79 (* Syntax : Number of clauses : 6 ( 0 non-Horn; 6 unit; 0 RR) *)
81 (* Number of atoms : 6 ( 6 equality) *)
83 (* Maximal clause size : 1 ( 1 average) *)
85 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
87 (* Number of functors : 2 ( 0 constant; 2-2 arity) *)
89 (* Number of variables : 12 ( 4 singleton) *)
91 (* Maximal term depth : 4 ( 2 average) *)
95 (* ------------------------------------------------------------------------------ *)
97 (* ----Axioms for a weakly associative lattice: *)
99 (* ------------------------------------------------------------------------------ *)
101 (* -------------------------------------------------------------------------- *)
103 (* ----{join,meet2} is a weakly-associative lattice: *)
105 (* ----Denial of meet=meet2: *)
107 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
110 ∀join:∀_:Univ.∀_:Univ.Univ.
111 ∀meet:∀_:Univ.∀_:Univ.Univ.
112 ∀meet2:∀_:Univ.∀_:Univ.Univ.
113 ∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join (meet2 X Y) (meet2 Z Y)) Y) Y.
114 ∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet2 (meet2 (join X Y) (join Z Y)) Y) Y.
115 ∀H2:∀X:Univ.∀Y:Univ.eq Univ (meet2 X Y) (meet2 Y X).
116 ∀H3:∀X:Univ.eq Univ (meet2 X X) X.
117 ∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join (meet X Y) (meet Z Y)) Y) Y.
118 ∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet (join X Y) (join Z Y)) Y) Y.
119 ∀H6:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
120 ∀H7:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
121 ∀H8:∀X:Univ.eq Univ (join X X) X.
122 ∀H9:∀X:Univ.eq Univ (meet X X) X.eq Univ (meet a b) (meet2 a b))
143 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9 ##;
144 ntry (nassumption) ##;
147 (* -------------------------------------------------------------------------- *)