:: On the Two Short Axiomatizations of Ortholattices :: by Wioletta Truszkowska and Adam Grabowski :: :: Received June 28, 2003 :: Copyright (c) 2003-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, ROBBINS1, SUBSET_1, ARYTM_3, LATTICES, ROBBINS2; notations STRUCT_0, LATTICES, ROBBINS1; constructors ROBBINS1; registrations LATTICES, ROBBINS1, STRUCT_0; begin :: One Axiom for Boolean Algebra definition let L be non empty ComplLLattStr; attr L is satisfying_DN_1 means :: ROBBINS2:def 1 for x, y, z, u being Element of L holds (((x + y)` + z)` + (x + (z` + (z + u)`)`)`)` = z; end; registration cluster TrivComplLat -> satisfying_DN_1; cluster TrivOrtLat -> satisfying_DN_1; end; registration cluster join-commutative join-associative satisfying_DN_1 for non empty ComplLLattStr; end; reserve L for satisfying_DN_1 non empty ComplLLattStr; reserve x, y, z for Element of L; theorem :: ROBBINS2:1 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u, v being Element of L holds ((x + y)` + (((z + u)` + x)` + (y` + (y + v)`)`)`)` = y; theorem :: ROBBINS2:2 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u being Element of L holds ((x + y)` + ((z + x)` + (y` + (y + u)`)`)`)` = y; theorem :: ROBBINS2:3 for L being satisfying_DN_1 non empty ComplLLattStr, x being Element of L holds ((x + x`)` + x)` = x`; theorem :: ROBBINS2:4 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u being Element of L holds ((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + u)`)` )`)` = y; theorem :: ROBBINS2:5 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((x + y)` + ((z + x)` + y)`)` = y; theorem :: ROBBINS2:6 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + (x` + y)`)` = y; theorem :: ROBBINS2:7 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (((x + y)` + x)` + (x + y)`)` = x; theorem :: ROBBINS2:8 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + ((x + y)` + x)`)` = (x + y)`; theorem :: ROBBINS2:9 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y)` + z)` + (x + z)`)` = z; theorem :: ROBBINS2:10 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + ((y + z)` + (y + x)`)`)` = (y + x)`; theorem :: ROBBINS2:11 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((((x + y)` + z)` + (x` + y)`)` + y)` = (x` + y)`; theorem :: ROBBINS2:12 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + ((y + z)` + (z + x)`)`)` = (z + x)`; theorem :: ROBBINS2:13 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u being Element of L holds ((x + y)` + ((z + x)` + (y` + (u + y)`)`)`)` = y; theorem :: ROBBINS2:14 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)` = (y + x)`; theorem :: ROBBINS2:15 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y)` + (y + z)`)` + z)` = (y + z)`; theorem :: ROBBINS2:16 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((x + ((x + y)` + z)`)` + z)` = ((x + y)` + z)`; theorem :: ROBBINS2:17 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (((x + y)` + x)` + y)` = (y + y)`; theorem :: ROBBINS2:18 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x` + (y + x)`)` = x; theorem :: ROBBINS2:19 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + y`)` = y; theorem :: ROBBINS2:20 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + (y + x`)`)` = x`; theorem :: ROBBINS2:21 for L being satisfying_DN_1 non empty ComplLLattStr, x being Element of L holds (x + x)` = x`; theorem :: ROBBINS2:22 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (((x + y)` + x)` + y)` = y`; theorem :: ROBBINS2:23 for L being satisfying_DN_1 non empty ComplLLattStr, x being Element of L holds x`` = x; theorem :: ROBBINS2:24 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + x)`+ y = y``; theorem :: ROBBINS2:25 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)`` = y + x; theorem :: ROBBINS2:26 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + ((y + z)` + (y + x)`)` = (y + x )``; theorem :: ROBBINS2:27 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds x + y = y + x; registration cluster satisfying_DN_1 -> join-commutative for non empty ComplLLattStr; end; theorem :: ROBBINS2:28 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + x)` + y = y; theorem :: ROBBINS2:29 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + y)`+ x = x; theorem :: ROBBINS2:30 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds x + ((y + x)` + y)` = x; theorem :: ROBBINS2:31 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y`)` + (y` + y)` = (x + y`)`; theorem :: ROBBINS2:32 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)` + (y + y`)` = (x + y)`; theorem :: ROBBINS2:33 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)` + (y` + y)` = (x + y)`; theorem :: ROBBINS2:34 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y`)`` + y)` = (y` + y)`; theorem :: ROBBINS2:35 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y`) + y)` = (y` + y)`; theorem :: ROBBINS2:36 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((((x + y`) + z)` + y)` + (y` + y)`)` = y; theorem :: ROBBINS2:37 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + ((y + z)` + (y + x)`)` = y + x; theorem :: ROBBINS2:38 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + (y + ((z + y)` + x)`)` = (z + y)` + x; theorem :: ROBBINS2:39 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + ((y + x)` + (y + z)`)` = y + x; theorem :: ROBBINS2:40 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((x + y)` + ((x + y)` + (x + z)`)`)` + y = y; theorem :: ROBBINS2:41 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y`) + z)` + y)`` = y; theorem :: ROBBINS2:42 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + ((y + x`) + z)` = x; theorem :: ROBBINS2:43 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x` + ((y + x) + z)` = x`; theorem :: ROBBINS2:44 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)` + x = x + y`; theorem :: ROBBINS2:45 for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + (x + y`)`)` = (x + y)`; theorem :: ROBBINS2:46 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((x + y)` + (x + z))` + y = y; theorem :: ROBBINS2:47 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = (x` + y)``; theorem :: ROBBINS2:48 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = x` + y; theorem :: ROBBINS2:49 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)``+ (y + z); theorem :: ROBBINS2:50 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + ( y + z); theorem :: ROBBINS2:51 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x) + (y + z); theorem :: ROBBINS2:52 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x`` + (y + z) = (y + x) + (y + z); theorem :: ROBBINS2:53 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + y) + (x + z) = y + (x + z); theorem :: ROBBINS2:54 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + y) + (x + z) = z + (x + y); theorem :: ROBBINS2:55 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + (y + z) = z + (y + x); theorem :: ROBBINS2:56 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + (y + z) = y + (z + x); theorem :: ROBBINS2:57 for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + y) + z = x + (y + z); registration cluster satisfying_DN_1 -> join-associative for non empty ComplLLattStr; cluster satisfying_DN_1 -> Robbins for non empty ComplLLattStr; end; theorem :: ROBBINS2:58 for L being non empty ComplLLattStr, x, z being Element of L st L is join-commutative join-associative Huntington holds (z + x) *' (z + x`) = z ; theorem :: ROBBINS2:59 for L being join-commutative join-associative non empty ComplLLattStr st L is Robbins holds L is satisfying_DN_1; registration cluster join-commutative join-associative Robbins -> satisfying_DN_1 for non empty ComplLLattStr; end; registration cluster satisfying_DN_1 de_Morgan for preOrthoLattice; end; registration cluster satisfying_DN_1 de_Morgan -> Boolean for preOrthoLattice; cluster Boolean -> satisfying_DN_1 for well-complemented preOrthoLattice; end; begin :: Meredith Two Axioms for Boolean Algebras definition let L be non empty ComplLLattStr; attr L is satisfying_MD_1 means :: ROBBINS2:def 2 for x, y being Element of L holds (x` + y)` + x = x; attr L is satisfying_MD_2 means :: ROBBINS2:def 3 for x, y, z being Element of L holds (x` + y)` + (z + y) = y + (z + x); end; registration cluster satisfying_MD_1 satisfying_MD_2 -> join-commutative join-associative Huntington for non empty ComplLLattStr; cluster join-commutative join-associative Huntington -> satisfying_MD_1 satisfying_MD_2 for non empty ComplLLattStr; end; registration cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan for preOrthoLattice; end; registration cluster satisfying_MD_1 satisfying_MD_2 de_Morgan -> Boolean for preOrthoLattice; cluster Boolean -> satisfying_MD_1 satisfying_MD_2 for well-complemented preOrthoLattice; end;