1 include "logic/equality.ma".
3 (* Inclusion of: LAT027-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : LAT027-1 : TPTP v3.7.0. Released v2.2.0. *)
9 (* Domain : Lattice Theory (Weakly Associative Lattices) *)
11 (* Problem : WAL + absorption gives LT, part 2. *)
13 (* Version : [MP96] (equality) axioms. *)
15 (* English : A Weakly associative lattice (WAL) satisfying an absorption *)
17 (* law is associative, and therefore a full lattice, part 2. *)
19 (* Refs : [McC98] McCune (1998), Email to G. Sutcliffe *)
21 (* : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq *)
23 (* Source : [McC98] *)
25 (* Names : WAL-1-b [MP96] *)
27 (* Status : Unsatisfiable *)
29 (* Rating : 0.00 v3.3.0, 0.07 v3.1.0, 0.00 v2.7.0, 0.09 v2.6.0, 0.00 v2.2.1 *)
31 (* Syntax : Number of clauses : 8 ( 0 non-Horn; 8 unit; 1 RR) *)
33 (* Number of atoms : 8 ( 8 equality) *)
35 (* Maximal clause size : 1 ( 1 average) *)
37 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
39 (* Number of functors : 5 ( 3 constant; 0-2 arity) *)
41 (* Number of variables : 15 ( 6 singleton) *)
43 (* Maximal term depth : 4 ( 2 average) *)
47 (* -------------------------------------------------------------------------- *)
49 (* ----Include Weakly Associative Lattices theory (equality) axioms *)
51 (* Inclusion of: Axioms/LAT005-0.ax *)
53 (* ------------------------------------------------------------------------------ *)
55 (* File : LAT005-0 : TPTP v3.7.0. Released v2.2.0. *)
57 (* Domain : Lattice Theory (Weakly Associative Lattices) *)
59 (* Axioms : Weakly Associative Lattices theory (equality) axioms *)
61 (* Version : [McC98b] (equality) axioms. *)
65 (* Refs : [McC98] McCune (1998), Email to G. Sutcliffe *)
67 (* : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq *)
69 (* Source : [McC98] *)
75 (* Syntax : Number of clauses : 6 ( 0 non-Horn; 6 unit; 0 RR) *)
77 (* Number of atoms : 6 ( 6 equality) *)
79 (* Maximal clause size : 1 ( 1 average) *)
81 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
83 (* Number of functors : 2 ( 0 constant; 2-2 arity) *)
85 (* Number of variables : 12 ( 4 singleton) *)
87 (* Maximal term depth : 4 ( 2 average) *)
91 (* ------------------------------------------------------------------------------ *)
93 (* ----Axioms for a weakly associative lattice: *)
95 (* ------------------------------------------------------------------------------ *)
97 (* -------------------------------------------------------------------------- *)
99 (* ----An absorption law. *)
101 (* ----Denial of associativity of join: *)
102 ntheorem prove_associativity_of_join:
103 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
107 ∀join:∀_:Univ.∀_:Univ.Univ.
108 ∀meet:∀_:Univ.∀_:Univ.Univ.
109 ∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet X (join Y (join X Z))) X.
110 ∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join (meet X Y) (meet Z Y)) Y) Y.
111 ∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet (join X Y) (join Z Y)) Y) Y.
112 ∀H3:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
113 ∀H4:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
114 ∀H5:∀X:Univ.eq Univ (join X X) X.
115 ∀H6:∀X:Univ.eq Univ (meet X X) X.eq Univ (join (join a b) c) (join a (join b c)))
133 nauto by H0,H1,H2,H3,H4,H5,H6 ##;
134 ntry (nassumption) ##;
137 (* -------------------------------------------------------------------------- *)