:: Robbins Algebras vs. Boolean Algebras :: by Adam Grabowski :: :: Received June 12, 2001 :: Copyright (c) 2001-2016 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 STRUCT_0, BINOP_1, LATTICES, FUNCT_5, XBOOLE_0, SUBSET_1, FUNCT_1, ARYTM_3, EQREL_1, XXREAL_2, ARYTM_1, ROBBINS1, CARD_1; notations TARSKI, ORDINAL1, CARD_1, STRUCT_0, LATTICES, BINOP_1, FUNCT_2, FUNCT_5; constructors BINOP_1, LATTICES, FUNCT_5; registrations RELSET_1, STRUCT_0, LATTICES, LATTICE2, CARD_1; requirements SUBSET, NUMERALS; definitions LATTICES, STRUCT_0; equalities LATTICES; expansions LATTICES, STRUCT_0; theorems STRUCT_0, LATTICES, BINOP_1; schemes BINOP_1; begin :: Preliminaries definition struct (1-sorted) ComplStr (# carrier -> set, Compl -> UnOp of the carrier #); end; definition struct(\/-SemiLattStr, ComplStr) ComplLLattStr (# carrier -> set, L_join -> BinOp of the carrier, Compl -> UnOp of the carrier #); end; definition struct(/\-SemiLattStr, ComplStr) ComplULattStr (# carrier -> set, L_meet -> BinOp of the carrier, Compl -> UnOp of the carrier #); end; definition struct (ComplLLattStr, LattStr) OrthoLattStr (# carrier -> set, L_join, L_meet -> BinOp of the carrier, Compl -> UnOp of the carrier #); end; definition func TrivComplLat -> strict ComplLLattStr equals ComplLLattStr (#{0}, op2, op1 #); coherence; end; definition func TrivOrtLat -> strict OrthoLattStr equals OrthoLattStr (#{0}, op2, op2, op1 #); coherence; end; registration cluster TrivComplLat -> 1-element; coherence; cluster TrivOrtLat -> 1-element; coherence; end; registration cluster strict 1-element for OrthoLattStr; existence proof take TrivOrtLat; thus thesis; end; cluster strict 1-element for ComplLLattStr; existence proof take TrivComplLat; thus thesis; end; end; registration let L be 1-element ComplLLattStr; cluster the ComplStr of L -> 1-element; coherence; end; registration cluster strict 1-element for ComplStr; existence proof take the ComplStr of TrivOrtLat; thus thesis; end; end; definition let L be non empty ComplStr; let x be Element of L; func x -> Element of L equals (the Compl of L).x; coherence; end; notation let L be non empty ComplLLattStr, x,y be Element of L; synonym x + y for x "\/" y; end; definition let L be non empty ComplLLattStr; let x,y be Element of L; func x *' y -> Element of L equals (x "\/" y); coherence; end; definition let L be non empty ComplLLattStr; attr L is Robbins means :Def5: for x, y being Element of L holds ((x + y) + (x + y)) = x; attr L is Huntington means :Def6: for x, y being Element of L holds (x + y ) + (x + y) = x; end; definition let G be non empty \/-SemiLattStr; attr G is join-idempotent means :Def7: for x being Element of G holds x "\/" x = x; end; registration cluster TrivComplLat -> join-commutative join-associative Robbins Huntington join-idempotent; coherence by STRUCT_0:def 10; cluster TrivOrtLat -> join-commutative join-associative Huntington Robbins; coherence by STRUCT_0:def 10; end; registration cluster TrivOrtLat -> meet-commutative meet-associative meet-absorbing join-absorbing; coherence by STRUCT_0:def 10; end; registration cluster strict join-associative join-commutative Robbins join-idempotent Huntington for non empty ComplLLattStr; existence proof take TrivComplLat; thus thesis; end; end; registration cluster strict Lattice-like Robbins Huntington for non empty OrthoLattStr; existence proof take TrivOrtLat; thus thesis; end; end; definition let L be join-commutative non empty ComplLLattStr, x,y be Element of L; redefine func x + y; commutativity by LATTICES:def 4; end; theorem Th1: :: 4.8 for L being Huntington join-commutative join-associative non empty ComplLLattStr, a, b being Element of L holds (a *' b) + (a *' b) = a by Def6; theorem Th2: :: 4.9 for L being Huntington join-commutative join-associative non empty ComplLLattStr, a being Element of L holds a + a = a + a proof let L be Huntington join-commutative join-associative non empty ComplLLattStr, a be Element of L; set y = a, z = y; a = ((a + y) + (a + y)) & a = ((a + a) + (a + a)) by Def6; then a + a = (y + z) + (y + y) + (y + y) + (y + z) by LATTICES:def 5 .= (y + y) + (y + y) + (y + z) + (y + z) by LATTICES:def 5 .= (y + y) + (y + y) + ((y + z) + (y + z)) by LATTICES:def 5 .= y + ((y + z) + (y + z)) by Def6 .= y + y by Def6; hence thesis; end; theorem Th3: :: 4.10 for L being join-commutative join-associative Huntington non empty ComplLLattStr, x being Element of L holds x = x proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, x be Element of L; set y = x; (y + y) + (y + y) = y & (y + y) + (y + y) = x by Def6; hence thesis by Th2; end; theorem Th4: :: 4.11 revised p. 557 without idempotency for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a + a = b + b proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b be Element of L; thus a + a = (a + b) + (a + b) + a by Def6 .= (a + b) + (a + b) + ((a + b) + (a + b)) by Def6 .= (a + b) + ((a + b) + ((a + b) + (a + b))) by LATTICES:def 5 .= (a + b) + ((a + b) + ((a + b) + (a + b))) by LATTICES:def 5 .= (a + b) + (a + b) + ((a + b) + (a + b)) by LATTICES:def 5 .= b + ((a + b) + (a + b)) by Def6 .= b + b by Def6; end; theorem Th5: :: 4.12 for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr ex c being Element of L st for a being Element of L holds c + a = c & a + a = c proof let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr; set b = the Element of L; take c = b + b; let a be Element of L; thus c + a = a + a + a by Th4 .= a + (a + a) by LATTICES:def 5 .= a + a by Def7 .= c by Th4; thus thesis by Th4; end; theorem Th6: :: 4.12 for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr holds L is upper-bounded proof let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr; consider c being Element of L such that A1: for a being Element of L holds c + a = c & a + a = c by Th5; for a being Element of L holds a + c = c & a + a = c by A1; hence thesis by A1; end; registration cluster join-commutative join-associative join-idempotent Huntington -> upper-bounded for non empty ComplLLattStr; coherence by Th6; end; definition let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr; redefine func Top L means :Def8: ex a being Element of L st it = a + a; compatibility proof let IT be Element of L; hereby set a = the Element of L; assume A1: IT = Top L; take a; for b being Element of L holds a + a + b = a + a & b + (a + a) = a + a proof let b be Element of L; a + a + b = b + b + b by Th4 .= b + (b + b) by LATTICES:def 5 .= b + b by Def7 .= a + a by Th4; hence thesis; end; hence IT = a + a by A1,LATTICES:def 17; end; given a being Element of L such that A2: IT = a + a; A3: for b being Element of L holds a + a + b = a + a proof let b be Element of L; a + a + b = b + b + b by Th4 .= b + (b + b) by LATTICES:def 5 .= b + b by Def7 .= a + a by Th4; hence thesis; end; then for b being Element of L holds b + (a + a) = a + a; hence thesis by A2,A3,LATTICES:def 17; end; end; theorem Th7: :: 4.13 for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr ex c being Element of L st for a being Element of L holds c *' a = c & (a + a) = c proof let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr; set b = the Element of L; take c = (b + b); let a be Element of L; thus c *' a = ((b + b) + a) by Th3 .= ((a + a) + a) by Th4 .= (a + (a + a)) by LATTICES:def 5 .= (a + a) by Def7 .= c by Th4; thus thesis by Th4; end; definition let L be join-commutative join-associative non empty ComplLLattStr; let x,y be Element of L; redefine func x *' y; commutativity proof let a, b be Element of L; thus a *' b = (a + b) .= b *' a; end; end; definition let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr; func Bot L -> Element of L means :Def9: for a being Element of L holds it *' a = it; existence proof ex c being Element of L st for a being Element of L holds c *' a = c & (a + a) = c by Th7; hence thesis; end; uniqueness proof let c1,c2 be Element of L such that A1: for a being Element of L holds c1 *' a = c1 and A2: for a being Element of L holds c2 *' a = c2; thus c1 = c2 *' c1 by A1 .= c2 by A2; end; end; theorem Th8: for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr, a being Element of L holds Bot L = (a + a) proof let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr, a be Element of L; for b being Element of L holds (a + a) *' b = (a + a) proof let b be Element of L; (a + a) *' b = ((b + b) + b) by Th4 .= ((b + b) + b) by Th3 .= (b + (b + b)) by LATTICES:def 5 .= (b + b) by Def7 .= (a + a) by Th4; hence thesis; end; hence thesis by Def9; end; theorem Th9: for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr holds (Top L) = Bot L & Top L = (Bot L) proof let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr; set a = the Element of L; thus (Top L) = (a + a) by Def8 .= Bot L by Th8; hence thesis by Th3; end; theorem Th10: :: 4.14 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L st a = b holds a = b proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L; assume A1: a = b; thus a = a by Th3 .= b by A1,Th3; end; theorem Th11: :: 4.15 proof without join-idempotency, no top at all for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a + (b + b) = a proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b be Element of L; set O = b + b; A1: O = O by Th3; A2: O = (O + O) + (O + O) by Def6 .= (O + O) + O by A1,Th4; A3: O = a + a by Th4; O = O + O by Th4 .= O + O + (O + O) by A2,LATTICES:def 5 .= O + (O + O) by Th4; then A4: O + O = O + O + (O + O) by LATTICES:def 5 .= O by Th4; hence a + O = ((a + a) + (a + a)) + ((a + a) + (a + a)) by A2,A3 ,Def6 .= (a + a) + ((a + a) + (a + a)) by A2,A4,A3,LATTICES:def 5 .= a by A2,A4,A3,Def6; end; theorem Th12: :: 4.5 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a + a = a proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L; A1: (a + a) = (a + a) + (a + a) by Th11 .= (a + a) + (a + a) by Th3 .= a by Def6; thus a + a = (a + a) by Th3 .= a by A1,Th3; end; registration cluster join-commutative join-associative Huntington -> join-idempotent for non empty ComplLLattStr; coherence by Th12; end; theorem Th13: :: 4.15 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a + Bot L = a proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L; a = (a + a) + (a + a) by Def6 .= a + (a + a) by Def7 .= a + (a + a) by Th3; hence thesis by Th8; end; theorem :: 4.16 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a *' Top L = a proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L; a *' Top L = (a + Bot L) by Th9 .= a by Th13 .= a by Th3; hence thesis; end; theorem Th15: :: 4.17 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a *' a = Bot L proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L; thus a *' a = (Top L) by Def8 .= Bot L by Th9; end; theorem Th16: :: 4.19 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds a *' (b *' c) = a *' b *' c proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c be Element of L; thus a *' b *' c = (a + b + c) by Th3 .= (a + (b + c)) by LATTICES:def 5 .= a *' (b *' c) by Th3; end; theorem Th17: :: 4.20 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a + b = (a *' b) proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b be Element of L; a *' b = (a + b) by Th3 .= (a + b) by Th3; hence thesis by Th3; end; theorem :: 4.21 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a *' a = a proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L; thus a *' a = a by Def7 .= a by Th3; end; theorem :: 4.22 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a + Top L = Top L proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L; thus a + Top L = a + (a + a) by Def8 .= a + a + a by LATTICES:def 5 .= a + a by Def7 .= Top L by Def8; end; theorem Th20: :: 4.24 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a + (a *' b) = a proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L; thus a + (a *' b) = (a *' b) + ((a *' b) + (a *' b)) by Def6 .= (a *' b) + (a *' b) + (a *' b) by LATTICES:def 5 .= (a *' b) + (a *' b) by Def7 .= a by Def6; end; theorem Th21: :: 4.25 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a *' (a + b) = a proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L; thus a *' (a + b) = (a + (a *' b)) by Th17 .= (a + (a *' b)) by Th3 .= a by Th20 .= a by Th3; end; theorem Th22: :: 4.26 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L st a + b = Top L & b + a = Top L holds a = b proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b be Element of L; assume A1: a + b = Top L & b + a = Top L; thus a = (a + b) + (a + b) by Def6 .= b by A1,Def6; end; theorem Th23: :: 4.27 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L st a + b = Top L & a *' b = Bot L holds a = b proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b be Element of L; assume a + b = Top L; then A1: a + b = Top L by Th3; assume A2: a *' b = Bot L; b + a = (a + b) by Th3 .= Top L by A2,Th9; hence thesis by A1,Th22; end; theorem Th24: :: 4.28 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) = Top L proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c be Element of L; set A = a *' b *' c, B = a *' b *' c, C = a *' b *' c; set D = a *' b *' c, E = a *' b *' c, F = a *' b *' c; set G = a *' b *' c, H = a *' b *' c; A + B + C + D + E + F + G + H = (a *' b) + C + D + E + F + G + H by Def6 .= (a *' b) + (C + D) + E + F + G + H by LATTICES:def 5 .= (a *' b) + (a *' b) + E + F + G + H by Def6 .= (a *' b) + (a *' b) + (E + F) + G + H by LATTICES:def 5 .= (a *' b) + (a *' b) + (a *' b) + G + H by Def6 .= (a *' b) + (a *' b) + (a *' b) + (G + H) by LATTICES:def 5 .= (a *' b) + (a *' b) + (a *' b) + (a *' b) by Def6 .= a + (a *' b) + (a *' b) by Def6 .= a + ((a *' b) + (a *' b)) by LATTICES:def 5 .= a + a by Def6; hence thesis by Def8; end; theorem Th25: :: 4.29 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds (a *' c) *' (b *' c) = Bot L & (a *' b *' c) *' (a *' b *' c) = Bot L & (a *' b *' c) *' (a *' b *' c) = Bot L & (a *' b *' c) *' (a *' b *' c) = Bot L & (a *' b *' c) *' (a *' b *' c) = Bot L proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c be Element of L; A1: for a, b, c being Element of L holds (a *' c) *' (b *' c) = Bot L proof let a, b, c be Element of L; thus (a *' c) *' (b *' c) = (a *' c) *' c *' b by Th16 .= a *' (c *' c) *' b by Th16 .= a *' Bot L *' b by Th15 .= Bot L *' b by Def9 .= Bot L by Def9; end; hence (a *' c) *' (b *' c) = Bot L; thus a *' b *' c *' (a *' b *' c) = a *' (b *' c) *' (a *' b *' c) by Th16 .= b *' c *' a *' (a *' b) *' c by Th16 .= b *' c *' a *' a *' b *' c by Th16 .= b *' c *' (a *' a) *' b *' c by Th16 .= b *' c *' (a *' a) *' (b *' c) by Th16 .= b *' c *' Bot L *' (b *' c) by Th15 .= Bot L *' (b *' c) by Def9 .= Bot L by Def9; thus (a *' b *' c) *' (a *' b *' c) = a *' (b *' c) *' (a *' b *' c) by Th16 .= (b *' c) *' a *' (a *' (b *' c)) by Th16 .= (b *' c) *' a *' a *' (b *' c) by Th16 .= (b *' c) *' (a *' a) *' (b *' c) by Th16 .= (b *' c) *' Bot L *' (b *' c) by Th15 .= Bot L *' (b *' c) by Def9 .= Bot L by Def9; thus (a *' b *' c) *' (a *' b *' c) = (a *' (b *' c)) *' (a *' b *' c) by Th16 .= (a *' (b *' c)) *' (a *' (b *' c)) by Th16 .= Bot L by A1; thus (a *' b *' c) *' (a *' b *' c) = (a *' (b *' c)) *' (a *' b *' c ) by Th16 .= (a *' (b *' c)) *' (a *' (b *' c)) by Th16 .= Bot L by A1; end; theorem Th26: :: 4.30 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds (a *' b) + (a *' c) = (a *' b *' c) + (a *' b *' c) + (a *' b *' c) proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c be Element of L; set A = a *' b *' c; a *' c = (a *' c *' b) + (a *' c *' b) by Def6 .= A + (a *' c *' b) by Th16 .= A + (a *' b *' c) by Th16; hence (a *' b) + (a *' c) = A + (a *' b *' c) + (A + (a *' b *' c)) by Def6 .= A + ((a *' b *' c) + A) + (a *' b *' c) by LATTICES:def 5 .= A + A + (a *' b *' c) + (a *' b *' c) by LATTICES:def 5 .= A + (a *' b *' c) + (a *' b *' c) by Def7; end; theorem Th27: :: 4.31 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds (a *' (b + c)) = (a *' b  *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c ) proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c be Element of L; set D = a *' b *' c, E = a *' b *' c, F = a *' b *' c; set G = a *' b *' c, H = a *' b *' c; A1: a = (a *' b) + (a *' b) by Def6 .= E + F + (a *' b) by Def6 .= E + F + (G + H) by Def6; A2: b *' c = (a *' (b *' c)) + (a *' (b *' c)) by Th1 .= D + (a *' (b *' c)) by Th16 .= D + H by Th16; (a *' (b + c)) = a + (b + c) by Th3 .= a + (b *' c) by Th17 .= a + (b *' c) by Th3; hence (a *' (b + c)) = E + F + (G + H) + H + D by A1,A2,LATTICES:def 5 .= E + F + G + H + H + D by LATTICES:def 5 .= E + F + G + (H + H) + D by LATTICES:def 5 .= E + F + G + H + D by Def7 .= D + (E + F + (G + H)) by LATTICES:def 5 .= D + (E + F) + (G + H) by LATTICES:def 5 .= D + (E + F) + G + H by LATTICES:def 5 .= D + E + F + G + H by LATTICES:def 5; end; theorem Th28: :: 4.32 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds ((a *' b) + (a *' c)) + (a *' (b + c)) = Top L proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c be Element of L; set A = a *' b *' c, B = a *' b *' c, C = a *' b *' c; set D = a *' b *' c, E = a *' b *' c, F = a *' b *' c; set G = a *' b *' c, H = a *' b *' c; set ABC = A + B + C, GH = G + H; (a *' (b + c)) = D + E + F + G + H & (a *' b) + (a *' c) = ABC by Th26,Th27; then (a *' b) + (a *' c) + (a *' (b + c)) = ABC + (D + E + F + GH) by LATTICES:def 5 .= ABC + (D + E + (F + GH)) by LATTICES:def 5 .= ABC + (D + E) + (F + GH) by LATTICES:def 5 .= ABC + D + E + (F + GH) by LATTICES:def 5 .= ABC + D + (E + (F + GH)) by LATTICES:def 5 .= ABC + D + (E + (F + G + H)) by LATTICES:def 5 .= ABC + D + E + (F + G + H) by LATTICES:def 5 .= ABC + D + E + (F + GH) by LATTICES:def 5 .= ABC + D + E + F + GH by LATTICES:def 5 .= ABC + D + E + F + G + H by LATTICES:def 5 .= Top L by Th24; hence thesis; end; theorem Th29: :: 4.33 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds ((a *' b) + (a *' c)) *' (a *' (b + c)) = Bot L proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c be Element of L; set A = a *' b *' c, B = a *' b *' c, C = a *' b *' c; set D = a *' b *' c, E = a *' b *' c, F = a *' b *' c; set G = a *' b *' c, H = a *' b *' c; set DEFG = D + E + F + G; (A *' D) + (A *' E) = Bot L + (A *' E) by Th25 .= Bot L + Bot L by Th25 .= Bot L by Def7; then Top L = Bot L + (A *' (D + E)) by Th28 .= (A *' (D + E)) by Th13; then Bot L = (A *' (D + E)) by Th9 .= A *' (D + E) by Th3; then (A *' (D + E)) + (A *' F) = Bot L + Bot L by Th25 .= Bot L by Def7; then Top L = Bot L + (A *' (D + E + F)) by Th28 .= (A *' (D + E + F)) by Th13; then A1: Bot L = (A *' (D + E + F)) by Th9 .= A *' (D + E + F) by Th3; A *' G = Bot L by Th25; then (A *' (D + E + F)) + (A *' G) = Bot L by A1,Def7; then Top L = Bot L + (A *' DEFG) by Th28 .= (A *' DEFG) by Th13; then Bot L = (A *' DEFG) by Th9 .= A *' DEFG by Th3; then (A *' DEFG) + (A *' H) = Bot L + Bot L by Th25 .= Bot L by Def7; then A2: Top L = Bot L + (A *' (DEFG + H)) by Th28 .= (A *' (DEFG + H)) by Th13; (B *' D) + (B *' E) = Bot L + (B *' E) by Th25 .= Bot L + Bot L by Th25 .= Bot L by Def7; then Top L = Bot L + (B *' (D + E)) by Th28 .= (B *' (D + E)) by Th13; then Bot L = (B *' (D + E)) by Th9 .= B *' (D + E) by Th3; then (B *' (D + E)) + (B *' F) = Bot L + Bot L by Th25 .= Bot L by Def7; then Top L = Bot L + (B *' (D + E + F)) by Th28 .= (B *' (D + E + F)) by Th13; then Bot L = (B *' (D + E + F)) by Th9 .= B *' (D + E + F) by Th3; then (B *' (D + E + F)) + (B *' G) = Bot L + Bot L by Th25 .= Bot L by Def7; then Top L = Bot L + (B *' DEFG) by Th28 .= (B *' DEFG) by Th13; then A3: Bot L = (B *' DEFG) by Th9 .= B *' DEFG by Th3; C *' D = Bot L by Th25; then (C *' D) + (C *' E) = Bot L + Bot L by Th25 .= Bot L by Def7; then Top L = Bot L + (C *' (D + E)) by Th28 .= (C *' (D + E)) by Th13; then Bot L = (C *' (D + E)) by Th9 .= C *' (D + E) by Th3; then (C *' (D + E)) + (C *' F) = Bot L + Bot L by Th25 .= Bot L by Def7; then Top L = Bot L + (C *' (D + E + F)) by Th28 .= (C *' (D + E + F)) by Th13; then Bot L = (C *' (D + E + F)) by Th9 .= C *' (D + E + F) by Th3; then (C *' (D + E + F)) + (C *' G) = Bot L + Bot L by Th25 .= Bot L by Def7; then Top L = Bot L + (C *' DEFG) by Th28 .= (C *' DEFG) by Th13; then Bot L = (C *' DEFG) by Th9 .= C *' DEFG by Th3; then (C *' DEFG) + (C *' H) = Bot L + Bot L by Th25 .= Bot L by Def7; then A4: Top L = Bot L + (C *' (DEFG + H)) by Th28 .= (C *' (DEFG + H)) by Th13; B *' H = Bot L by Th25; then (B *' DEFG) + (B *' H) = Bot L by A3,Def7; then A5: Top L = Bot L + (B *' (DEFG + H)) by Th28 .= (B *' (DEFG + H)) by Th13; A6: B *' (DEFG + H) = (B *' (DEFG + H)) by Th3 .= Bot L by A5,Th9; A *' (DEFG + H) = (A *' (DEFG + H)) by Th3 .= Bot L by A2,Th9; then (A *' (DEFG + H)) + (B *' (DEFG + H)) = Bot L by A6,Def7; then Top L = Bot L + ((A + B) *' (DEFG + H)) by Th28 .= ((A + B) *' (DEFG + H)) by Th13; then A7: Bot L = ((A + B) *' (DEFG + H)) by Th9 .= (A + B) *' (DEFG + H) by Th3; C *' (DEFG + H) = (C *' (DEFG + H)) by Th3 .= Bot L by A4,Th9; then ((A + B) *' (DEFG + H)) + (C *' (DEFG + H)) = Bot L by A7,Def7; then Top L = Bot L + ((A + B + C) *' (DEFG + H)) by Th28 .= ((A + B + C) *' (DEFG + H)) by Th13; then A8: Bot L = ((A + B + C) *' (DEFG + H)) by Th9 .= (A + B + C) *' (DEFG + H) by Th3; (a *' (b + c)) = DEFG + H by Th27; hence thesis by A8,Th26; end; theorem Th30: :: 4.34 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c) proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c be Element of L; (a *' b) + (a *' c) + (a *' (b + c)) = Top L & ((a *' b) + (a *' c)) *' (a *' (b + c)) = Bot L by Th28,Th29; then ((a *' b) + (a *' c)) = (a *' (b + c)) by Th23; hence thesis by Th10; end; theorem :: 4.35 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c) proof let L be join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c be Element of L; thus a + (b *' c) = (a *' (b + c)) by Th17 .= (a *' (b + c)) by Th3 .= ((a *' b) + (a *' c)) by Th30 .= ((a *' b) *' (a *' c)) by Th17 .= (a *' b) *' (a *' c) by Th3 .= (a + b) *' (a *' c) by Th17 .= (a + b) *' (a + c) by Th17; end; begin :: Pre-Ortholattices definition let L be non empty OrthoLattStr; attr L is well-complemented means :Def10: for a being Element of L holds a is_a_complement_of a; end; registration cluster TrivOrtLat -> Boolean well-complemented; coherence proof set L = TrivOrtLat; thus L is bounded; thus L is complemented proof let b be Element of L; take a = b; a "\/" b = Top L & a "/\" b = Bottom L by STRUCT_0:def 10; hence thesis; end; thus L is distributive by STRUCT_0:def 10; let a be Element of L; A1: a "\/" a = a "\/" a & a "/\" a = a "/\" a; a "\/" a = Top L & a "/\" a = Bottom L by STRUCT_0:def 10; hence a is_a_complement_of a by A1; end; end; definition mode preOrthoLattice is Lattice-like non empty OrthoLattStr; end; registration cluster strict Boolean well-complemented for preOrthoLattice; existence proof take TrivOrtLat; thus thesis; end; end; theorem Th32: for L being distributive well-complemented preOrthoLattice, x being Element of L holds x = x proof let L be distributive well-complemented preOrthoLattice; let x be Element of L; x is_a_complement_of x by Def10; then A1: x + x = Top L & x "/\" x = Bottom L; x is_a_complement_of x by Def10; then x "\/" x = Top L & x "/\" x = Bottom L; hence thesis by A1,LATTICES:12; end; theorem Th33: for L being bounded distributive well-complemented preOrthoLattice, x, y being Element of L holds x "/\" y = (x "\/" y) proof let L be bounded distributive well-complemented preOrthoLattice; let x, y be Element of L; A1: x "\/" Top L = Top L; A2: y "\/" Top L = Top L; A3: y is_a_complement_of y by Def10; then A4: y "\/" y = Top L; (x "/\" y) is_a_complement_of (x "/\" y) by Def10; then A5: (x "/\" y) "\/" (x "/\" y) = Top L & (x "/\" y) "/\" (x "/\" y) = Bottom L; A6: x is_a_complement_of x by Def10; then A7: x "\/" x = Top L; A8: y "/\" y = Bottom L by A3; A9: x "/\" x = Bottom L by A6; A10: (x "\/" y) "/\" (x "/\" y) = (x "/\" y "/\" x) "\/" (x "/\" y "/\" y ) by LATTICES:def 11 .= (y "/\" (x "/\" x)) "\/" (x "/\" y "/\" y) by LATTICES:def 7 .= (y "/\" Bottom L) "\/" (x "/\" (y "/\" y)) by A9,LATTICES:def 7 .= Bottom L "\/" (x "/\" Bottom L) by A8 .= Bottom L "\/" Bottom L .= Bottom L; (x "\/" y) "\/" (x "/\" y) = (x "\/" y "\/" x) "/\" (x "\/" y "\/" y) by LATTICES:11 .= (y "\/" x "\/" x) "/\" Top L by A4,A1,LATTICES:def 5 .= Top L "/\" Top L by A7,A2,LATTICES:def 5 .= Top L; then (x "/\" y) = x "\/" y by A10,A5,LATTICES:12; hence thesis by Th32; end; begin :: Correspondence between boolean preOrthoLattice and boolean lattice :: according to the definition given in \cite{LATTICES.ABS} definition let L be non empty ComplLLattStr; func CLatt L -> strict OrthoLattStr means :Def11: the carrier of it = the carrier of L & the L_join of it = the L_join of L & the Compl of it = the Compl of L & for a, b being Element of L holds (the L_meet of it).(a,b) = a *' b; existence proof deffunc F(Element of L, Element of L)= $1 *'$2; consider K being BinOp of the carrier of L such that A1: for a, b being Element of L holds K.(a,b) = F(a,b) from BINOP_1: sch 4; take OrthoLattStr (# the carrier of L, the L_join of L, K, the Compl of L #); thus thesis by A1; end; uniqueness proof let L1, L2 be strict OrthoLattStr such that A2: the carrier of L1 = the carrier of L and A3: the L_join of L1 = the L_join of L & the Compl of L1 = the Compl of L and A4: for a, b being Element of L holds (the L_meet of L1).(a,b) = a *' b and A5: the carrier of L2 = the carrier of L and A6: the L_join of L2 = the L_join of L & the Compl of L2 = the Compl of L and A7: for a, b being Element of L holds (the L_meet of L2).(a,b) = a *' b; reconsider A = the L_meet of L1, B = the L_meet of L2 as BinOp of the carrier of L by A2,A5; now let a, b be Element of L; thus A.(a,b) = a *' b by A4 .= B.(a,b) by A7; end; hence thesis by A2,A3,A5,A6,BINOP_1:2; end; end; registration let L be non empty ComplLLattStr; cluster CLatt L -> non empty; coherence proof the carrier of CLatt L = the carrier of L by Def11; hence thesis; end; end; registration let L be join-commutative non empty ComplLLattStr; cluster CLatt L -> join-commutative; coherence proof let a,b be Element of CLatt L; the carrier of L = the carrier of CLatt L & the L_join of L = the L_join of CLatt L by Def11; hence thesis by BINOP_1:def 2; end; end; registration let L be join-associative non empty ComplLLattStr; cluster CLatt L -> join-associative; coherence proof set K = the L_join of L, M = the L_join of CLatt L; let a, b, c be Element of CLatt L; the carrier of L = the carrier of CLatt L & K = M by Def11; hence thesis by BINOP_1:def 3; end; end; registration let L be join-commutative join-associative non empty ComplLLattStr; cluster CLatt L -> meet-commutative; coherence proof let a, b be Element of CLatt L; reconsider a9 = a, b9 = b as Element of L by Def11; thus a "/\" b = b9 *' a9 by Def11 .= b "/\" a by Def11; end; end; theorem for L being non empty ComplLLattStr, a, b being Element of L, a9, b9 being Element of CLatt L st a = a9 & b = b9 holds a *' b = a9 "/\" b9 & a + b = a9 "\/" b9 & a = a9 by Def11; registration let L be join-commutative join-associative Huntington non empty ComplLLattStr; cluster CLatt L -> meet-associative join-absorbing meet-absorbing; coherence proof hereby let a, b, c be Element of CLatt L; reconsider a9 = a, b9 = b, c9 = c as Element of L by Def11; A1: b9 *' c9 = b "/\" c by Def11; a9 *' b9 = a "/\" b by Def11; hence a "/\" b "/\" c = a9 *' b9 *' c9 by Def11 .= a9 *' (b9 *' c9) by Th16 .= a "/\" (b "/\" c) by A1,Def11; end; hereby let a, b be Element of CLatt L; reconsider a9 = a, b9 = b as Element of L by Def11; a9 + b9 = a "\/" b by Def11; hence a "/\" (a "\/" b) = a9 *' (a9 + b9) by Def11 .= a by Th21; end; let a, b be Element of CLatt L; reconsider a9 = a, b9 = b as Element of L by Def11; a9 *' b9 = a "/\" b by Def11; hence (a "/\" b) "\/" b = (a9 *' b9) + b9 by Def11 .= b by Th20; end; end; registration let L be Huntington non empty ComplLLattStr; cluster CLatt L -> Huntington; coherence proof let x, y be Element of CLatt L; reconsider x9 = x, y9 = y as Element of L by Def11; A1: x = x9 by Def11; y = y9 by Def11; then x + y = x9 + y9 by A1,Def11; then A2: (x + y) = (x9 + y9) by Def11; x + y = x9 + y9 by A1,Def11; then (x + y) = (x9 + y9) by Def11; hence (x + y) + (x + y) = (x9 + y9) + (x9 + y9) by A2,Def11 .= x by Def6; end; end; registration let L be join-commutative join-associative Huntington non empty ComplLLattStr; cluster CLatt L -> lower-bounded; coherence proof thus CLatt L is lower-bounded proof set c9 = Bot L; reconsider c = c9 as Element of CLatt L by Def11; take c; let a be Element of CLatt L; reconsider a9 = a as Element of L by Def11; thus c "/\" a = c9 *' a9 by Def11 .= c by Def9; hence a "/\" c = c; end; end; end; theorem Th35: for L being join-commutative join-associative Huntington non empty ComplLLattStr holds Bot L = Bottom CLatt L proof let L be join-commutative join-associative Huntington non empty ComplLLattStr; reconsider C = Bot L as Element of CLatt L by Def11; for a being Element of CLatt L holds C "/\" a = C & a "/\" C = C proof let a be Element of CLatt L; reconsider a9 = a as Element of L by Def11; thus C "/\" a = Bot L *' a9 by Def11 .= C by Def9; hence thesis; end; hence thesis by LATTICES:def 16; end; registration let L be join-commutative join-associative Huntington non empty ComplLLattStr; cluster CLatt L -> complemented distributive bounded; coherence proof thus CLatt L is complemented proof let b be Element of CLatt L; take a = b; reconsider a9 = a, b9 = b as Element of L by Def11; thus a + b = Top CLatt L by Def8; thus b + a = Top CLatt L by Def8; A1: a9 = a by Def11 .= b9 by Th3; thus a "/\" b = a9 *' b9 by Def11 .= Bot L by A1,Th8 .= Bottom CLatt L by Th35; hence b "/\" a = Bottom CLatt L; end; hereby let a, b, c be Element of CLatt L; reconsider a9 = a, b9 = b, c9 = c as Element of L by Def11; A2: a "/\" b = a9 *' b9 & a "/\" c = a9 *' c9 by Def11; b9 + c9 = b "\/" c by Def11; hence a "/\" (b "\/" c) = a9 *' (b9 + c9) by Def11 .= (a9 *' b9) + (a9 *' c9) by Th30 .= (a "/\" b) "\/" (a "/\" c) by A2,Def11; end; thus CLatt L is lower-bounded; thus thesis; end; end; begin :: Proofs according to Bernd Ingo Dahn notation let G be non empty ComplLLattStr, x be Element of G; synonym -x for x; end; definition let G be join-commutative non empty ComplLLattStr; redefine attr G is Huntington means for x, y being Element of G holds -(-x + -y) + -(x + -y) = y; compatibility proof thus G is Huntington implies for x, y being Element of G holds -(-x + -y) + -(x + -y) = y; assume A1: for x, y being Element of G holds -(-x + -y) + -(x + -y) = y; let x, y be Element of G; (x + y) + (x + y) = x by A1; hence thesis; end; end; definition let G be non empty ComplLLattStr; attr G is with_idempotent_element means ex x being Element of G st x + x = x; correctness; end; reserve G for Robbins join-associative join-commutative non empty ComplLLattStr; reserve x, y, z, u, v for Element of G; definition let G be non empty ComplLLattStr, x, y be Element of G; func \delta (x, y) -> Element of G equals -(-x + y); coherence; end; definition let G be non empty ComplLLattStr, x, y be Element of G; func Expand (x, y) -> Element of G equals \delta (x + y, \delta(x, y)); coherence; end; definition let G be non empty ComplLLattStr, x be Element of G; func x _0 -> Element of G equals -(-x + x); coherence; func Double x -> Element of G equals x + x; coherence; end; definition let G be non empty ComplLLattStr, x be Element of G; func x _1 -> Element of G equals x _0 + x; coherence; func x _2 -> Element of G equals x _0 + Double x; coherence; func x _3 -> Element of G equals x _0 + (Double x + x); coherence; func x _4 -> Element of G equals x _0 + (Double x + Double x); coherence; end; theorem Th36: \delta ((x + y), (\delta (x, y))) = y proof thus \delta ((x + y), (\delta (x, y))) = -(-(x + y) + -(-x + y)) .= y by Def5; end; theorem Expand (x, y) = y by Th36; theorem \delta (-x + y, z) = -(\delta (x, y) + z); theorem \delta (x, x) = x _0; theorem Th40: \delta (Double x, x _0) = x proof thus \delta (Double x, x _0) = Expand (x, x) .= x by Th36; end; theorem Th41: :: Lemma 1 \delta (x _2, x) = x _0 proof thus \delta (x _2, x) = \delta (Double x + x _0, \delta (Double x, x _0)) by Th40 .= x _0 by Th36; end; theorem Th42: x _4 + x _0 = x _3 + x _1 proof thus x _4 + x _0 = (x _0 + Double x) + Double x + x _0 by LATTICES:def 5 .= (x _0 + Double x) + x + x + x _0 by LATTICES:def 5 .= x _3 + x + x _0 by LATTICES:def 5 .= x _3 + x _1 by LATTICES:def 5; end; theorem Th43: x _3 + x _0 = x _2 + x _1 proof thus x _3 + x _0 = (x _0 + Double x) + x + x _0 by LATTICES:def 5 .= x _2 + x _1 by LATTICES:def 5; end; theorem Th44: x _3 + x = x _4 proof thus x _3 + x = x _0 + (Double x + x + x) by LATTICES:def 5 .= x _4 by LATTICES:def 5; end; theorem Th45: :: Lemma 2 \delta (x _3, x _0) = x proof thus x = Expand (x _2, x) by Th36 .= \delta (x + x _2, x _0) by Th41 .= \delta (x _3, x _0) by LATTICES:def 5; end; theorem :: Left Argument Substitution -x = -y implies \delta (x, z) = \delta (y,z); theorem Th47: :: Exchange \delta (x, -y) = \delta (y, -x) proof thus \delta (x, -y) = -(-x + -y) .= \delta (y, -x); end; theorem Th48: :: Lemma 3 \delta (x _3, x) = x _0 proof set alpha = -x _3 + x _1 + -Double x; x = Expand (-x _3 + x _0, x) by Th36 .= \delta (-x _3 + x _1, -(\delta (x _3, x _0) + x)) by LATTICES:def 5 .= \delta (-x _3 + x _1, -Double x) by Th45; then A1: -Double x = \delta (-x _3 + x _1 + -Double x, x) by Th36; A2: x = \delta (Double x, x _0) by Th40 .= \delta (-alpha + x, x _0) by A1; -x _3 = Expand (x _1 + -Double x, -x _3) by Th36 .= \delta (-x _3 + x _1 + -Double x, \delta (x _1 + -Double x, -x _3)) by LATTICES:def 5 .= \delta (alpha, \delta (x _0 + (x + Double x), \delta (Double x, x _1) )) by Th47 .= \delta (alpha, \delta (Double x + x _1, \delta (Double x, x _1))) by LATTICES:def 5 .= -(-alpha + x _1) by Th36; hence \delta (x _3, x) = \delta (-alpha + (x _0 + x), x) .= Expand (-alpha + x, x _0) by A2,LATTICES:def 5 .= x _0 by Th36; end; theorem Th49: :: Lemma 4 \delta (x _1 + x _3, x) = x _0 proof x _0 = Expand (x _4, x _0) by Th36 .= \delta (x _4 + x _0, \delta (x _4, \delta (x _3, x))) by Th48 .= \delta (x _3 + x _1, \delta (x _4, \delta (x _3, x))) by Th42 .= \delta (x _3 + x _1, Expand (x _3, x)) by Th44 .= \delta (x _3 + x _1, x) by Th36; hence thesis; end; theorem Th50: :: Lemma 5 \delta (x _1 + x _2, x) = x _0 proof thus x _0 = Expand (x _3, x _0) by Th36 .= \delta (x _1 + x _2, \delta(x _3, x _0)) by Th43 .= \delta (x _1 + x _2, x) by Th45; end; theorem Th51: :: Lemma 6 \delta (x _1 + x _3, x _0) = x proof thus x = Expand (x _1 + x _2, x) by Th36 .= \delta (x _1 + (x _2 + x), \delta(x _1 + x _2, x)) by LATTICES:def 5 .= \delta (x _1 + x _3, \delta(x _1 + x _2, x)) by LATTICES:def 5 .= \delta (x _1 + x _3, x _0) by Th50; end; definition let G, x; func \beta x -> Element of G equals -(x _1 + x _3) + x + -(x _3); coherence; end; theorem Th52: :: Lemma 7 \delta (\beta x, x) = -x _3 proof thus -x _3 = \delta (\beta x, \delta (-(x _1 + x _3) + x, -(x _3))) by Th36 .= \delta (\beta x, \delta (x _3, \delta (x _1 + x _3, x))) by Th47 .= \delta (\beta x, \delta (x _3, x _0)) by Th49 .= \delta (\beta x, x) by Th45; end; theorem Th53: :: Lemma 8 \delta (\beta x, x) = -(x _1 + x _3) proof thus -(x _1 + x _3) = \delta (-(x _1 + x _3) + (x + -(x _3)), \delta (x + -( x _3), -(x _1 + x _3))) by Th36 .= \delta (\beta x, \delta (x + -(x _3), -(x _1 + x _3))) by LATTICES:def 5 .= \delta (\beta x, \delta (x _1 + x _3, \delta (x _3, x))) by Th47 .= \delta (\beta x, \delta (x _1 + x _3, x _0)) by Th48 .= \delta (\beta x, x) by Th51; end; theorem :: Winker Second Condition ex y, z st -(y + z) = -z proof set x = the Element of G; take y = x _1, z = x _3; -(y + z) = \delta (\beta x, x) by Th53 .= -z by Th52; hence thesis; end; begin :: Proofs according to Bill McCune theorem (for z holds --z = z) implies G is Huntington proof assume A1: for z holds --z = z; let x, y; A2: --(-(-x + -y) + -(x + -y)) = --y by Def5; -(-x + -y) + -(x + -y) = --(-(-x + -y) + -(x + -y)) by A1 .= y by A1,A2; hence thesis; end; theorem Th56: G is with_idempotent_element implies G is Huntington proof assume G is with_idempotent_element; then consider C being Element of G such that A1: C + C = C; A2: now let x; thus C + x = -(-(-C + (C+x)) + -(C + (C+x))) by Def5 .= -(-(-C + C+x) + -(C + (C+x))) by LATTICES:def 5 .= -(-(C + -C + x) + -(C + x)) by A1,LATTICES:def 5; end; assume G is non Huntington; then consider B, A being Element of G such that A3: -(-B + -A) + -(B + -A) <> A; set D = C + -C + -C; A4: C = -(-C + -(C + -C)) by A1,Def5; then A5: -(C + -(C + -C + -C)) = -C by Def5; then -(-C + -(C + -C + -C)) = -(-(-(C + -C + -C) + C) + -(C + C + (-C + -C))) by A1,LATTICES:def 5 .= -(-(-(C + -C + -C) + C) + -(C + (C + (-C + -C)))) by LATTICES:def 5 .= -(-(-D + C) + -(D + C)) by LATTICES:def 5 .= C by Def5; then A6: -(C + -C) = -(C + -C + -C) by A5,Def5; C = -(-(C + C) + -(-C + -(C + -C) + C)) by A4,Def5 .= -(-C + -(C + -C + -(C + -C))) by A1,LATTICES:def 5; then A7: C = C + -(C + -C) by A2,A5,A6; A8: now let x; thus x = -(-(C + -(C + -C) + x) + -(-C + -(C + -C) + x)) by A4,A7,Def5 .= -(-(C + (-(C + -C) + x)) + -(-C + -(C + -C) + x)) by LATTICES:def 5 .= -(-(C + (-(C + -C) + x)) + -(-C + (-(C + -C) + x))) by LATTICES:def 5 .= -(C + -C) + x by Def5; end; A9: now let x; thus -(C + -C) = -(-(-x + -(C + -C)) + -(x + -(C + -C))) by Def5 .= -(--x + -(x + -(C + -C))) by A8 .= -(--x + -x) by A8; end; A10: now let x; thus --x = -(-(-x + --x) + -(x + --x)) by Def5 .= -(-(C + -C) + -(x + --x)) by A9 .= --(x + --x) by A8; end; A11: now let x; thus -x = -(-(---x + -x) + -(--x + -x)) by Def5 .= -(-(---x + -x) + -(C + -C)) by A9 .= --(---x + -x) by A8 .= ---x by A10; end; A12: now let x, y; thus y = -(-(-x + y) + -(x + y)) by Def5 .= ---(-(-x + y) + -(x + y)) by A11 .= --y by Def5; end; now let x, y; thus -(-x + y) + -(x + y) = --(-(-x + y) + -(x + y)) by A12 .= -y by Def5; end; then -(-B + -A) + -(B + -A) = --A .= A by A12; hence thesis by A3; end; registration cluster TrivComplLat -> with_idempotent_element; coherence proof set x = the Element of TrivComplLat; take x; thus x = x + x by STRUCT_0:def 10; end; end; registration cluster with_idempotent_element -> Huntington for Robbins join-associative join-commutative non empty ComplLLattStr; coherence by Th56; end; theorem Th57: (ex c, d being Element of G st c + d = c) implies G is Huntington proof A1: now let x, y, z; set k = -(-x + y); thus -(-(-(-x + y) + x + y) + y) = -(-(k + x + y) + -(k + -(x + y))) by Def5 .= -(-(k + (x + y)) + -(k + -(x + y))) by LATTICES:def 5 .= -(-x + y) by Def5; end; A2: now let x, y, z; set k = -(-x + y); -(-(k + x + y) + y) = k by A1; hence z = -(-(-(-(-x + y) + x + y) + y + z) + -(-(-x + y) + z)) by Def5; end; given C, D being Element of G such that A3: C + D = C; A4: now let x, y, z; set k = -(-x + y) + -(x + y); thus -(-(-(-x + y) + -(x + y) + z) + -(y + z)) = -(-(k + z) + -(-k + z)) by Def5 .= z by Def5; end; A5: now let x; thus D = -(-(-(-x + C) + -(x + C) + D) + -(C + D)) by A4 .= -(-C + -(D + -(C + -x) + -(C + x))) by A3,LATTICES:def 5; end; set e = -(C + -C); set K = -(C + C + -(C + -C)); A6: K = -(C + -(C + -C) + C) by LATTICES:def 5; A7: now let x, y; thus -(-(D + -(C + x) + y) + -(C + x + y)) = -(-(-(C + x) + (D + y)) + -(C + D + x + y)) by A3,LATTICES:def 5 .= -(-(-(C + x) + (D + y)) + -(C + x + D + y)) by LATTICES:def 5 .= -(-(-(C + x) + (D + y)) + -((C + x) + (D + y))) by LATTICES:def 5 .= D + y by Def5; end; set L = -(D + -C); set E = D + -C; A8: -(-C + -(D + -C)) = D by A3,Def5; then A9: -(D + -(C + -E)) = -E by Def5; -(L + -(C + L)) = -(-(D + -(C + L)) + -((D + C) + L)) by A3,A8,Def5 .= -(-(D + -(C + L)) + -(D + (C + L))) by LATTICES:def 5 .= D by Def5; then -(D + -(D + -C + -(C + -(D + -C)))) = -(C + -(D + -C)) by Def5; then A10: -(C + -(D + -C)) = -(D + -(D + -(C + -(D + -C)) + -C)) by LATTICES:def 5 .= -C by A8,A9,Def5; set L = C + -(D + -C); A11: C = -(-(D + -L + C) + -(-(D + -C) + C)) by A9,Def5 .= -(-L + -(C + -L)) by A3,LATTICES:def 5; then -(C + -(C + -(C + -C))) = -(C + -C) by A10,Def5; then C = -(-(C + -C) + K) by A6,Def5; then -(C + -(C + -C + K)) = K by Def5; then K = -(-(K + C + -C) + C) by LATTICES:def 5 .= -(-(-(-(C + -C) + C + C) + C + -C) + C) by LATTICES:def 5 .= -C by A11,A2,A10; then D + -(C + -C) = -(-(D + -(C + C) + -(C + -C)) + -C) by A7 .= -(-C + -(D + -(C + -C) + -(C + C))) by LATTICES:def 5 .= D by A5; then A12: C + -(C + -C) = C by A3,LATTICES:def 5; now let x; thus x = -(-(C + -(C + -C) + x) + -(-C + -(C + -C) + x)) by A11,A10,A12 ,Def5 .= -(-(C + (-(C + -C) + x)) + -(-C + -(C + -C) + x)) by LATTICES:def 5 .= -(-(C + (-(C + -C) + x)) + -(-C + (-(C + -C) + x))) by LATTICES:def 5 .= -(C + -C) + x by Def5; end; then e = e + e; then G is with_idempotent_element; hence thesis; end; theorem Th58: ex y, z st y + z = z proof A1: now let x, y; thus -(x + y) = -(-(-(-x + y) + -(x + y)) + -(-x + y + -(x + y))) by Def5 .= -(y + -(-x + y + -(x + y))) by Def5 .= -(-(-(x + y) + -x + y) + y) by LATTICES:def 5; end; A2: now let x, y; thus -(-x + y) = -(-(-(x + y) + -(-x + y)) + -((x + y) + -(-x + y))) by Def5 .= -(y + -(x + y + -(-x + y))) by Def5 .= -(-(-(-x + y) + x + y) + y) by LATTICES:def 5; end; A3: now let x, y; thus y = -(-(-(-(-x + y) + x + y) + y) + -((-(-x + y) + x + y) + y)) by Def5 .= -(-(-x + y) + -((-(-x + y) + x + y) + y)) by A2 .= -(-(-(-x + y) + x + Double y) + -(-x + y)) by LATTICES:def 5; end; A4: now let x, y, z; thus z = -(-(-(-(-(-x + y) + x + Double y) + -(-x + y)) + z) + -(-(-(-x + y) + x + Double y) + -(-x + y) + z)) by Def5 .= -(-(-(-(-x + y) + x + Double y) + -(-x + y) + z) + -(y + z)) by A3; end; A5: now let x, y, z; set k = -(-(-x + y) + x + Double y) + -(-x + y) + z; thus -(y + z) = -(-(-k + -(y + z)) + -(k + -(y + z))) by Def5 .= -(z + -(k + -(y + z))) by A4 .= -(-(-(-(-x + y) + x + Double y) + -(-x + y) + -(y + z) + z) + z) by LATTICES:def 5; end; A6: now let x, y, z, u; set k = -(-(-(-x + y) + x + Double y) + -(-x + y) + -(y + z) + z) + z; thus u = -(-(-k + u) + -(k + u)) by Def5 .= -(-(-(y + z) + u) + -(k + u)) by A5; end; A7: now let x, y, z, v; set k = -(-(Double v + v) + v); set l = -(-(Double v + v) + v) + Double v; set v5 = Double v + Double v + v; A8: -(Double v + v + l) = -(-(-(Double v + v + l) + -(Double v + v) + l) + l) by A1 .= -(-(-(Double v + v + l) + l + -(Double v + v)) + l) by LATTICES:def 5; thus k = -(-(-(v + Double v) + k) + -((-(-(-(-(Double v + v) + v) + ( Double v + v) + Double v) + -(-(Double v + v) + v) + -(v + Double v) + Double v ) + Double v) + k)) by A6 .= -(-(-(v + Double v) + k) + -((-(-(Double v + v + k + Double v) + k + Double v + -(v + Double v)) + Double v) + k)) by LATTICES:def 5 .= -(-(-(v + Double v) + k) + -((-(-((Double v + v) + k + Double v) + (k + Double v) + -(v + Double v)) + Double v) + k)) by LATTICES:def 5 .= -(-(-(v + Double v) + k) + -((-(-(Double v + v + (k + Double v)) + l + -(v + Double v)) + Double v) + k)) by LATTICES:def 5 .= -(-(-(v + Double v) + k) + -(-(-(Double v + v + l) + l + -(v + Double v)) + l)) by LATTICES:def 5 .= -(-(-(Double v + v) + k) + -(Double v + v + Double v + k)) by A8, LATTICES:def 5 .= -(-(-(Double v + v) + k) + -(v5 + k)) by LATTICES:def 5; end; A9: now let x; set k = -(-(Double x + x) + x) + -(Double x + x); set l = -(-(-(Double x + x) + x) + (Double x + Double x + x)); A10: -(Double x + x) = -(-(-(-(-(Double x + x) + x) + (Double x + x) + Double x) + -(-(Double x + x) + x) + -(Double x + x)) + -(x + -(Double x + x))) by A4 .= -(-(-(-(-(Double x + x) + x) + (Double x + x) + Double x) + k) + -( x + -(Double x + x))) by LATTICES:def 5 .= -(-(-(-(-(Double x + x) + x) + (Double x + x + Double x)) + k) + -( x + -(Double x + x))) by LATTICES:def 5 .= -(-(l + k) + -(x + -(Double x + x))) by LATTICES:def 5; l = -(-(-k + l) + -(k + l)) by Def5 .= -(-(-(Double x + x) + x) + -(k + l)) by A7; hence -(-(-(Double x + x) + x) + (Double x + Double x + x)) = -(Double x + x) by A10; end; A11: now let x; A12: -(-(Double x + x) + x) = -(-(-(-(Double x + x) + x) + (Double x + x) + x) + x) by A2 .= -(-(-(-(Double x + x) + x) + (Double x + x + x)) + x) by LATTICES:def 5 .= -(-(-(-(Double x + x) + x) + (Double x + Double x)) + x) by LATTICES:def 5; thus x = -(-(-(-(-(Double x + x) + x) + (Double x + Double x)) + x) + -(-( -(Double x + x) + x) + (Double x + Double x) + x)) by Def5 .= -(-(-(-(-(Double x + x) + x) + (Double x + Double x)) + x) + -(-(-( Double x + x) + x) + ((Double x + Double x) + x))) by LATTICES:def 5 .= -(-(-(Double x + x) + x) + -(Double x + x)) by A9,A12; end; A13: now let x, y; thus y = -(-(-(-(-(Double x + x) + x) + -(Double x + x)) + y) + -(-(-( Double x + x) + x) + -(Double x + x) + y)) by Def5 .= -(-(-(-(Double x + x) + x) + -(Double x + x) + y) + -(x + y)) by A11; end; A14: now let x; thus -(-(Double x + x) + x) + Double x = -(-(-(Double x + x) + (-(-(Double x + x) + x) + Double x)) + -((Double x + x) + (-(-(Double x + x) + x) + Double x))) by Def5 .= -(-(-(Double x + x) + (-(-(Double x + x) + x) + Double x)) + -((-(- (Double x + x) + x) + ((Double x + x) + Double x)))) by LATTICES:def 5 .= -(-(-(Double x + x) + (-(-(Double x + x) + x) + Double x)) + -((-(- (Double x + x) + x) + (Double x + Double x + x)))) by LATTICES:def 5 .= -(-(-(Double x + x) + (-(-(Double x + x) + x) + Double x)) + -( Double x + x)) by A9 .= -(-(-(-(Double x + x) + x) + -(Double x + x) + Double x) + -(Double x + x)) by LATTICES:def 5; end; A15: now let x, y; thus Double x = -(-(-(-(Double x + x) + x) + -(Double x + x) + Double x ) + -(x + Double x)) by A13 .= -(-(Double x + x) + x) + Double x by A14; end; set x = the Element of G; set c = Double x, d = -(-(Double x + x) + x); take d, c; thus thesis by A15; end; registration cluster Robbins -> Huntington for join-associative join-commutative non empty ComplLLattStr; coherence proof let K be join-associative join-commutative non empty ComplLLattStr; assume A1: K is Robbins; then ex y, z be Element of K st y + z = z by Th58; hence thesis by A1,Th57; end; end; definition let L be non empty OrthoLattStr; attr L is de_Morgan means :Def23: for x, y being Element of L holds x "/\" y = (x "\/" y); end; registration let L be non empty ComplLLattStr; cluster CLatt L -> de_Morgan; coherence proof let x, y be Element of CLatt L; reconsider x9 = x, y9 = y as Element of L by Def11; x9 = x & y9 = y by Def11; then x9 "\/" y9 = x "\/" y by Def11; then (x "\/" y) = x9 *' y9 by Def11; hence thesis by Def11; end; end; theorem Th59: for L being well-complemented join-commutative meet-commutative non empty OrthoLattStr, x being Element of L holds x + x = Top L & x "/\" x = Bottom L proof let L be well-complemented join-commutative meet-commutative non empty OrthoLattStr, x be Element of L; A1: x is_a_complement_of x by Def10; hence x + x = Top L; thus thesis by A1; end; theorem Th60: for L being bounded distributive well-complemented preOrthoLattice holds (Top L) = Bottom L proof let L be bounded distributive well-complemented preOrthoLattice; set x = the Element of L; (Top L) = (x + x) by Th59 .= x "/\" x by Th33 .= Bottom L by Th59; hence thesis; end; registration cluster TrivOrtLat -> de_Morgan; coherence by STRUCT_0:def 10; end; registration cluster strict de_Morgan Boolean Robbins Huntington for preOrthoLattice; existence proof take TrivOrtLat; thus thesis; end; end; registration cluster join-associative join-commutative de_Morgan -> meet-commutative for non empty OrthoLattStr; coherence proof let L be non empty OrthoLattStr; assume L is join-associative join-commutative de_Morgan; then reconsider L1 = L as join-associative join-commutative de_Morgan non empty OrthoLattStr; let a,b be Element of L; reconsider a1=a, b1=b as Element of L1; thus a "/\" b = a1 *' b1 by Def23 .= b1 *' a1 .= b "/\" a by Def23; end; end; theorem Th61: for L being Huntington de_Morgan preOrthoLattice holds Bot L = Bottom L proof let L be Huntington de_Morgan preOrthoLattice; reconsider C = Bot L as Element of L; A1: for a being Element of L holds C "/\" a = C & a "/\" C = C proof let a be Element of L; reconsider a9 = a as Element of L; thus C "/\" a = Bot L *' a9 by Def23 .= C by Def9; hence thesis; end; then L is lower-bounded; hence thesis by A1,LATTICES:def 16; end; registration cluster Boolean -> Huntington for well-complemented preOrthoLattice; coherence proof let L be well-complemented preOrthoLattice; assume A1: L is Boolean; then reconsider L9 = L as Boolean preOrthoLattice; A2: for x being Element of L9 holds Top L9 "/\" x = x; now let x, y be Element of L; thus (x "\/" y) "\/" (x "\/" y) = (x "/\" y) + (x + y) by A1,Th33 .= (x + (x + y)) "/\" (y + (x + y)) by A1,LATTICES:11 .= (x + (x + y)) "/\" (y + (x + y)) by A1,Th32 .= (x + (x "/\" y)) "/\" (y + (x + y)) by A1,Th33 .= x "/\" (y + (x + y)) by LATTICES:def 8 .= x "/\" (y + (x + y)) by A1,Th32 .= x "/\" (y + (x "/\" y)) by A1,Th33 .= x "/\" ((y + x) "/\" (y + y)) by A1,LATTICES:11 .= (x "/\" (y + x)) "/\" (y + y) by LATTICES:def 7 .= x "/\" (y + y) by LATTICES:def 9 .= x "/\" Top L by Th59 .= x by A2; end; hence thesis; end; end; registration cluster Huntington -> Boolean for de_Morgan preOrthoLattice; coherence proof let L be de_Morgan preOrthoLattice; assume A1: L is Huntington; then reconsider L9 = L as Huntington preOrthoLattice; A2: L is lower-bounded proof set c9 = Bot L9; reconsider c = c9 as Element of L; take c; let a be Element of L; reconsider a9 = a as Element of L9; thus c "/\" a = c9 *' a9 by Def23 .= c by Def9; thus a "/\" c = c9 *' a9 by Def23 .= c by Def9; end; L9 is upper-bounded; hence L is bounded by A2; thus L is complemented proof let b be Element of L; take a = b; A3: L9 is join-idempotent; hence a + b = Top L by Def8; thus b + a = Top L by A3,Def8; thus a "/\" b = (a + b) by Def23 .= Bot L9 by Th8 .= Bottom L by Th61; hence b "/\" a = Bottom L; end; thus L is distributive proof let a, b, c be Element of L; A4: a "/\" b = a *' b & a "/\" c = a *' c by Def23; thus a "/\" (b "\/" c) = a *' (b + c) by Def23 .= (a "/\" b) "\/" (a "/\" c) by A1,A4,Th30; end; end; end; registration cluster Robbins de_Morgan -> Boolean for preOrthoLattice; coherence; cluster Boolean -> Robbins for well-complemented preOrthoLattice; coherence proof let L be well-complemented preOrthoLattice; assume L is Boolean; then reconsider L9 = L as Boolean well-complemented preOrthoLattice; now let x, y be Element of L9; thus ((x + y) + (x + y)) = (x + y) "/\" (x + y) by Th33 .= ((x + y) "/\" x) + ((x + y) "/\" y) by LATTICES:def 11 .= ((x + y) "/\" x) + ((x "/\" y) + (y "/\" y)) by LATTICES:def 11 .= ((x + y) "/\" x) + ((x "/\" y) + (y + y)) by Th33 .= x + ((x "/\" y) + (y + y)) by LATTICES:def 9 .= x + (x "/\" y) + (y + y) by LATTICES:def 5 .= x + (y + y) by LATTICES:def 8 .= x + (Top L9)` by Th59 .= x + Bottom L9 by Th60 .= x; end; hence thesis; end; end;