Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### On the Two Short Axiomatizations of Ortholattices

**by****Wioletta Truszkowska, and****Adam Grabowski**- Received June 28, 2003
- MML identifier: ROBBINS2

- [ Mizar article, MML identifier index ]

environ vocabulary LATTICES, SUBSET_1, ARYTM_3, ROBBINS1, ROBBINS2; notation STRUCT_0, LATTICES, ROBBINS1; constructors REALSET1, ROBBINS1; clusters ROBBINS1; begin :: One Axiom for Boolean Algebra definition let L be non empty ComplLattStr; 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; definition cluster TrivComplLat -> satisfying_DN_1; cluster TrivOrtLat -> satisfying_DN_1; end; definition cluster join-commutative join-associative satisfying_DN_1 (non empty ComplLattStr); end; reserve L for satisfying_DN_1 (non empty ComplLattStr); reserve x, y, z, u, v for Element of L; theorem :: ROBBINS2:1 :: A61 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z, u, v being Element of L holds ((x + y)` + (((z + u)` + x)` + (y` + (y + v)`)`)`)` = y; theorem :: ROBBINS2:2 :: A62 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z, u being Element of L holds ((x + y)` + ((z + x)` + (y` + (y + u)`)`)`)` = y; theorem :: ROBBINS2:3 :: A63 for L being satisfying_DN_1 (non empty ComplLattStr), x being Element of L holds ((x + x`)` + x)` = x`; theorem :: ROBBINS2:4 :: A64 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z, u being Element of L holds ((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + u)`)`)`)` = y; theorem :: ROBBINS2:5 :: A65 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds ((x + y)` + ((z + x)` + y)`)` = y; theorem :: ROBBINS2:6 :: A66 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds ((x + y)` + (x` + y)`)` = y; theorem :: ROBBINS2:7 :: A67 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (((x + y)` + x)` + (x + y)`)` = x; theorem :: ROBBINS2:8 :: A68 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x + ((x + y)` + x)`)` = (x + y)`; theorem :: ROBBINS2:9 :: A69 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (((x + y)` + z)` + (x + z)`)` = z; theorem :: ROBBINS2:10 :: A70 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (x + ((y + z)` + (y + x)`)`)` = (y + x)`; theorem :: ROBBINS2:11 :: A71 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds ((((x + y)` + z)` + (x` + y)`)` + y)` = (x` + y)`; theorem :: ROBBINS2:12 :: A72 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (x + ((y + z)` + (z + x)`)`)` = (z + x)`; theorem :: ROBBINS2:13 :: A73 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z, u being Element of L holds ((x + y)` + ((z + x)` + (y` + (u + y)`)`)`)` = y; theorem :: ROBBINS2:14 :: A74 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x + y)` = (y + x)`; theorem :: ROBBINS2:15 :: A75 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (((x + y)` + (y + z)`)` + z)` = (y + z)`; theorem :: ROBBINS2:16 :: A76 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds ((x + ((x + y)` + z)`)` + z)` = ((x + y)` + z)`; theorem :: ROBBINS2:17 :: A77 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (((x + y)` + x)` + y)` = (y + y)`; theorem :: ROBBINS2:18 :: A78 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x` + (y + x)`)` = x; theorem :: ROBBINS2:19 :: A79 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds ((x + y)` + y`)` = y; theorem :: ROBBINS2:20 :: A80 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x + (y + x`)`)` = x`; theorem :: ROBBINS2:21 :: A81 for L being satisfying_DN_1 (non empty ComplLattStr), x being Element of L holds (x + x)` = x`; theorem :: ROBBINS2:22 :: A83 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (((x + y)` + x)` + y)` = y`; theorem :: ROBBINS2:23 :: A85 for L being satisfying_DN_1 (non empty ComplLattStr), x being Element of L holds x`` = x; theorem :: ROBBINS2:24 :: A86 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds ((x + y)` + x)`+ y = y``; theorem :: ROBBINS2:25 :: A87 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x + y)`` = y + x; theorem :: ROBBINS2:26 :: A88 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds x + ((y + z)` + (y + x)`)` = (y + x )``; theorem :: ROBBINS2:27 :: A89 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds x + y = y + x; definition cluster satisfying_DN_1 -> join-commutative (non empty ComplLattStr); end; theorem :: ROBBINS2:28 :: A90 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds ((x + y)` + x)` + y = y; theorem :: ROBBINS2:29 :: A91 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds ((x + y)` + y)`+ x = x; theorem :: ROBBINS2:30 :: A92 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds x + ((y + x)` + y)` = x; theorem :: ROBBINS2:31 :: A93 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x + y`)` + (y` + y)` = (x + y`)`; theorem :: ROBBINS2:32 :: A94 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x + y)` + (y + y`)` = (x + y)`; theorem :: ROBBINS2:33 :: A95 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x + y)` + (y` + y)` = (x + y)`; theorem :: ROBBINS2:34 :: A96 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds ((x + y`)`` + y)` = (y` + y)`; theorem :: ROBBINS2:35 :: A97 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds ((x + y`) + y)` = (y` + y)`; theorem :: ROBBINS2:36 :: A98 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds ((((x + y`) + z)` + y)` + (y` + y)`)` = y; theorem :: ROBBINS2:37 :: A99 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds x + ((y + z)` + (y + x)`)` = y + x; theorem :: ROBBINS2:38 :: A100 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds x + (y + ((z + y)` + x)`)` = (z + y)` + x; theorem :: ROBBINS2:39 :: A101 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds x + ((y + x)` + (y + z)`)` = y + x; theorem :: ROBBINS2:40 :: A102 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds ((x + y)` + ((x + y)` + (x + z)`)`)` + y = y; theorem :: ROBBINS2:41 :: A103 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (((x + y`) + z)` + y)`` = y; theorem :: ROBBINS2:42 :: A104 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds x + ((y + x`) + z)` = x; theorem :: ROBBINS2:43 :: A105 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds x` + ((y + x) + z)` = x`; theorem :: ROBBINS2:44 :: A107 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x + y)` + x = x + y`; theorem :: ROBBINS2:45 :: A108 for L being satisfying_DN_1 (non empty ComplLattStr), x, y being Element of L holds (x + (x + y`)`)` = (x + y)`; theorem :: ROBBINS2:46 :: A109 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds ((x + y)` + (x + z))` + y = y; theorem :: ROBBINS2:47 :: A110 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = (x` + y)``; theorem :: ROBBINS2:48 :: A111 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = x` + y; theorem :: ROBBINS2:49 :: A112 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)``+ (y + z); theorem :: ROBBINS2:50 :: A113 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + (y + z); theorem :: ROBBINS2:51 :: A114 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x) + (y + z); theorem :: ROBBINS2:52 :: A115 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds x`` + (y + z) = (y + x) + (y + z); theorem :: ROBBINS2:53 :: A117 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (x + y) + (x + z) = y + (x + z); theorem :: ROBBINS2:54 :: A118 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (x + y) + (x + z) = z + (x + y); theorem :: ROBBINS2:55 :: A119 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds x + (y + z) = z + (y + x); theorem :: ROBBINS2:56 :: A120 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds x + (y + z) = y + (z + x); theorem :: ROBBINS2:57 :: A121 for L being satisfying_DN_1 (non empty ComplLattStr), x, y, z being Element of L holds (x + y) + z = x + (y + z); definition cluster satisfying_DN_1 -> join-associative (non empty ComplLattStr); cluster satisfying_DN_1 -> Robbins (non empty ComplLattStr); end; theorem :: ROBBINS2:58 for L being non empty ComplLattStr, 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 non empty ComplLattStr st L is join-commutative join-associative Robbins holds L is satisfying_DN_1; definition cluster join-commutative join-associative Robbins -> satisfying_DN_1 (non empty ComplLattStr); end; definition cluster satisfying_DN_1 de_Morgan preOrthoLattice; end; definition cluster satisfying_DN_1 de_Morgan -> Boolean preOrthoLattice; cluster Boolean -> satisfying_DN_1 (well-complemented preOrthoLattice); end; begin :: Meredith Two Axioms for Boolean Algebras definition let L be non empty ComplLattStr; 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; definition cluster satisfying_MD_1 satisfying_MD_2 -> join-commutative join-associative Huntington (non empty ComplLattStr); cluster join-commutative join-associative Huntington -> satisfying_MD_1 satisfying_MD_2 (non empty ComplLattStr); end; definition cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan preOrthoLattice; end; definition cluster satisfying_MD_1 satisfying_MD_2 de_Morgan -> Boolean preOrthoLattice; cluster Boolean -> satisfying_MD_1 satisfying_MD_2 (well-complemented preOrthoLattice); end;

Back to top