:: Robbins Algebras vs. Boolean Algebras
:: by Adam Grabowski
::
:: Received June 12, 2001
:: Copyright (c) 2001 Association of Mizar Users

definition

attr c₁ is strict;
struct ComplStr -> 1-sorted ;
aggr ComplStr(# carrier, Compl #) -> ComplStr ;
sel Compl c₁ -> UnOp of the carrier of c₁;

end;

definition

attr c₁ is strict;
struct ComplLattStr -> \/-SemiLattStr , ComplStr ;
aggr ComplLattStr(# carrier, L_join, Compl #) -> ComplLattStr ;

end;

definition

attr c₁ is strict;
struct OrthoLattStr -> ComplLattStr , LattStr ;
aggr OrthoLattStr(# carrier, L_join, L_meet, Compl #) -> OrthoLattStr ;

end;

definition

func TrivComplLat -> strict ComplLattStr equals :: ROBBINS1:def 1
ComplLattStr(# 1,op2 ,op1 #);
coherence
ComplLattStr(# 1,op2 ,op1 #) is strict ComplLattStr ;

end;

:: deftheorem defines TrivComplLat ROBBINS1:def 1 :

TrivComplLat = ComplLattStr(# 1,op2 ,op1 #);

definition

func TrivOrtLat -> strict OrthoLattStr equals :: ROBBINS1:def 2
OrthoLattStr(# 1,op2 ,op2 ,op1 #);
coherence
OrthoLattStr(# 1,op2 ,op2 ,op1 #) is strict OrthoLattStr ;

end;

:: deftheorem defines TrivOrtLat ROBBINS1:def 2 :

TrivOrtLat = OrthoLattStr(# 1,op2 ,op2 ,op1 #);

registration

cluster TrivComplLat -> non empty trivial strict ;
coherence
( not TrivComplLat is empty & TrivComplLat is trivial ) by CARD_1:87;
cluster TrivOrtLat -> non empty trivial strict ;
coherence
( not TrivOrtLat is empty & TrivOrtLat is trivial ) by CARD_1:87;

end;

registration

cluster non empty trivial strict OrthoLattStr ;
existence
ex b₁ being OrthoLattStr st
( b₁ is strict & not b₁ is empty & b₁ is trivial )

proof end;

cluster non empty trivial strict ComplLattStr ;
existence
ex b₁ being ComplLattStr st
( b₁ is strict & not b₁ is empty & b₁ is trivial )

proof end;

end;

registration

let L be non empty trivial ComplLattStr ;
cluster ComplStr(# the carrier of L,the Compl of L #) -> non empty trivial ;
coherence
( not ComplStr(# the carrier of L,the Compl of L #) is empty & ComplStr(# the carrier of L,the Compl of L #) is trivial ) ;

end;

registration

cluster non empty trivial strict ComplStr ;
existence
ex b₁ being ComplStr st
( b₁ is strict & not b₁ is empty & b₁ is trivial )

proof end;

end;

definition

let L be non empty ComplStr ;
let x be Element of L;
func x ` -> Element of L equals :: ROBBINS1:def 3
the Compl of L . x;
coherence
the Compl of L . x is Element of L ;

end;

:: deftheorem defines ` ROBBINS1:def 3 :

for L being non empty ComplStr
for x being Element of L holds x ` = the Compl of L . x;

notation

let L be non empty ComplLattStr ;
let x, y be Element of L;
synonym x + y for x "\/" y;

end;

definition

let L be non empty ComplLattStr ;
let x, y be Element of L;
func x *' y -> Element of L equals :: ROBBINS1:def 4
((x ` ) "\/" (y ` )) ` ;
coherence
((x ` ) "\/" (y ` )) ` is Element of L ;

end;

:: deftheorem defines *' ROBBINS1:def 4 :

for L being non empty ComplLattStr
for x, y being Element of L holds x *' y = ((x ` ) "\/" (y ` )) ` ;

definition

let L be non empty ComplLattStr ;
attr L is Robbins means :Def5: :: ROBBINS1:def 5
for x, y being Element of L holds (((x + y) ` ) + ((x + (y ` )) ` )) ` = x;
attr L is Huntington means :Def6: :: ROBBINS1:def 6
for x, y being Element of L holds (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x;

end;

:: deftheorem Def5 defines Robbins ROBBINS1:def 5 :

for L being non empty ComplLattStr holds
( L is Robbins iff for x, y being Element of L holds (((x + y) ` ) + ((x + (y ` )) ` )) ` = x );

:: deftheorem Def6 defines Huntington ROBBINS1:def 6 :

for L being non empty ComplLattStr holds
( L is Huntington iff for x, y being Element of L holds (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x );

definition

let G be non empty \/-SemiLattStr ;
attr G is join-idempotent means :Def7: :: ROBBINS1:def 7
for x being Element of G holds x "\/" x = x;

end;

:: deftheorem Def7 defines join-idempotent ROBBINS1:def 7 :

for G being non empty \/-SemiLattStr holds
( G is join-idempotent iff for x being Element of G holds x "\/" x = x );

registration

cluster TrivComplLat -> join-commutative join-associative strict Robbins Huntington join-idempotent ;
coherence
( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is Robbins & TrivComplLat is Huntington & TrivComplLat is join-idempotent )

proof end;

cluster TrivOrtLat -> join-commutative join-associative strict Robbins Huntington ;
coherence
( TrivOrtLat is join-commutative & TrivOrtLat is join-associative & TrivOrtLat is Huntington & TrivOrtLat is Robbins )

proof end;

end;

registration

cluster TrivOrtLat -> meet-commutative meet-associative meet-absorbing join-absorbing strict ;
coherence
( TrivOrtLat is meet-commutative & TrivOrtLat is meet-associative & TrivOrtLat is meet-absorbing & TrivOrtLat is join-absorbing )

proof end;

end;

registration

cluster non empty join-commutative join-associative strict Robbins Huntington join-idempotent ComplLattStr ;
existence
ex b₁ being non empty ComplLattStr st
( b₁ is strict & b₁ is join-associative & b₁ is join-commutative & b₁ is Robbins & b₁ is join-idempotent & b₁ is Huntington )

proof end;

end;

registration

cluster non empty Lattice-like strict Robbins Huntington OrthoLattStr ;
existence
ex b₁ being non empty OrthoLattStr st
( b₁ is strict & b₁ is Lattice-like & b₁ is Robbins & b₁ is Huntington )

proof end;

end;

definition

let L be non empty join-commutative ComplLattStr ;
let x, y be Element of L;
:: original: +
redefine func x + y -> M2(the carrier of L);
commutativity
for x, y being Element of L holds x + y = y + x by LATTICES:def 4;

end;

theorem Th1: :: ROBBINS1:1

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L holds (a *' b) + (a *' (b ` )) = a by Def6;

theorem Th2: :: ROBBINS1:2

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a being Element of L holds a + (a ` ) = (a ` ) + ((a ` ) ` )

proof end;

theorem Th3: :: ROBBINS1:3

for L being non empty join-commutative join-associative Huntington ComplLattStr
for x being Element of L holds (x ` ) ` = x

proof end;

theorem Th4: :: ROBBINS1:4

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L holds a + (a ` ) = b + (b ` )

proof end;

theorem Th5: :: ROBBINS1:5

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ex c being Element of L st
for a being Element of L holds
( c + a = c & a + (a ` ) = c )

proof end;

theorem Th6: :: ROBBINS1:6

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr holds L is upper-bounded

proof end;

registration

cluster non empty join-commutative join-associative Huntington join-idempotent -> non empty upper-bounded ComplLattStr ;
coherence
for b₁ being non empty ComplLattStr st b₁ is join-commutative & b₁ is join-associative & b₁ is join-idempotent & b₁ is Huntington holds
b₁ is upper-bounded by Th6;

end;

definition

let L be non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ;
redefine func Top L means :Def8: :: ROBBINS1:def 8
ex a being Element of L st it = a + (a ` );
compatibility
for b<sub>1</sub> being M2(the carrier of L) holds
( b<sub>1</sub> = Top L iff ex a being Element of L st b<sub>1</sub> = a + (a ` ) )

proof end;

end;

:: deftheorem Def8 defines Top ROBBINS1:def 8 :

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr
for b₂ being M2(the carrier of b₁) holds
( b₂ = Top L iff ex a being Element of L st b₂ = a + (a ` ) );

theorem Th7: :: ROBBINS1:7

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ex c being Element of L st
for a being Element of L holds
( c *' a = c & (a + (a ` )) ` = c )

proof end;

theorem Th8: :: ROBBINS1:8

for L being non empty join-commutative join-associative ComplLattStr
for a, b being Element of L holds a *' b = b *' a

proof end;

definition

let L be non empty join-commutative join-associative ComplLattStr ;
let x, y be Element of L;
:: original: *'
redefine func x *' y -> Element of L;
commutativity
for x, y being Element of L holds x *' y = y *' x by Th8;

end;

definition

let L be non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ;
func Bot L -> Element of L means :Def9: :: ROBBINS1:def 9
for a being Element of L holds it *' a = it;
existence
ex b₁ being Element of L st
for a being Element of L holds b₁ *' a = b₁

proof end;

uniqueness
for b₁, b₂ being Element of L st ( for a being Element of L holds b₁ *' a = b₁ ) & ( for a being Element of L holds b₂ *' a = b₂ ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines Bot ROBBINS1:def 9 :

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr
for b₂ being Element of L holds
( b₂ = Bot L iff for a being Element of L holds b₂ *' a = b₂ );

theorem Th9: :: ROBBINS1:9

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr
for a being Element of L holds Bot L = (a + (a ` )) `

proof end;

theorem Th10: :: ROBBINS1:10

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr holds
( (Top L) ` = Bot L & Top L = (Bot L) ` )

proof end;

theorem Th11: :: ROBBINS1:11

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L st a ` = b ` holds
a = b

proof end;

theorem Th12: :: ROBBINS1:12

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L holds a + ((b + (b ` )) ` ) = a

proof end;

theorem Th13: :: ROBBINS1:13

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a being Element of L holds a + a = a

proof end;

registration

cluster non empty join-commutative join-associative Huntington -> non empty join-idempotent ComplLattStr ;
coherence
for b₁ being non empty ComplLattStr st b₁ is join-commutative & b₁ is join-associative & b₁ is Huntington holds
b₁ is join-idempotent

proof end;

end;

theorem Th14: :: ROBBINS1:14

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a being Element of L holds a + (Bot L) = a

proof end;

theorem :: ROBBINS1:15

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a being Element of L holds a *' (Top L) = a

proof end;

theorem Th16: :: ROBBINS1:16

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a being Element of L holds a *' (a ` ) = Bot L

proof end;

theorem Th17: :: ROBBINS1:17

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b, c being Element of L holds a *' (b *' c) = (a *' b) *' c

proof end;

theorem Th18: :: ROBBINS1:18

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L holds a + b = ((a ` ) *' (b ` )) `

proof end;

theorem :: ROBBINS1:19

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a being Element of L holds a *' a = a

proof end;

theorem :: ROBBINS1:20

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a being Element of L holds a + (Top L) = Top L

proof end;

theorem Th21: :: ROBBINS1:21

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L holds a + (a *' b) = a

proof end;

theorem Th22: :: ROBBINS1:22

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L holds a *' (a + b) = a

proof end;

theorem Th23: :: ROBBINS1:23

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L st (a ` ) + b = Top L & (b ` ) + a = Top L holds
a = b

proof end;

theorem Th24: :: ROBBINS1:24

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L st a + b = Top L & a *' b = Bot L holds
a ` = b

proof end;

theorem Th25: :: ROBBINS1:25

for L being non empty join-commutative join-associative Huntington ComplLattStr
for 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 end;

theorem Th26: :: ROBBINS1:26

for L being non empty join-commutative join-associative Huntington ComplLattStr
for 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 end;

theorem Th27: :: ROBBINS1:27

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b, c being Element of L holds (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c ` ))) + ((a *' (b ` )) *' c)

proof end;

theorem Th28: :: ROBBINS1:28

for L being non empty join-commutative join-associative Huntington ComplLattStr
for 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 end;

theorem Th29: :: ROBBINS1:29

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b, c being Element of L holds ((a *' b) + (a *' c)) + ((a *' (b + c)) ` ) = Top L

proof end;

theorem Th30: :: ROBBINS1:30

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b, c being Element of L holds ((a *' b) + (a *' c)) *' ((a *' (b + c)) ` ) = Bot L

proof end;

theorem Th31: :: ROBBINS1:31

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c)

proof end;

theorem :: ROBBINS1:32

for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c)

proof end;

definition

let L be non empty OrthoLattStr ;
attr L is well-complemented means :Def10: :: ROBBINS1:def 10
for a being Element of L holds a ` is_a_complement_of a;

end;

:: deftheorem Def10 defines well-complemented ROBBINS1:def 10 :

for L being non empty OrthoLattStr holds
( L is well-complemented iff for a being Element of L holds a ` is_a_complement_of a );

registration

cluster TrivOrtLat -> Boolean strict well-complemented ;
coherence
( TrivOrtLat is Boolean & TrivOrtLat is well-complemented )

proof end;

end;

definition

mode preOrthoLattice is non empty Lattice-like OrthoLattStr ;

end;

registration

cluster Boolean strict well-complemented OrthoLattStr ;
existence
ex b₁ being preOrthoLattice st
( b₁ is strict & b₁ is Boolean & b₁ is well-complemented )

proof end;

end;

theorem Th33: :: ROBBINS1:33

for L being distributive well-complemented preOrthoLattice
for x being Element of L holds (x ` ) ` = x

proof end;

theorem Th34: :: ROBBINS1:34

for L being distributive bounded well-complemented preOrthoLattice
for x, y being Element of L holds x "/\" y = ((x ` ) "\/" (y ` )) `

proof end;

definition

let L be non empty ComplLattStr ;
func CLatt L -> strict OrthoLattStr means :Def11: :: ROBBINS1:def 11
( 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
ex b₁ being strict OrthoLattStr st
( the carrier of b₁ = the carrier of L & the L_join of b₁ = the L_join of L & the Compl of b₁ = the Compl of L & ( for a, b being Element of L holds the L_meet of b₁ . a,b = a *' b ) )

proof end;

uniqueness
for b₁, b₂ being strict OrthoLattStr st the carrier of b₁ = the carrier of L & the L_join of b₁ = the L_join of L & the Compl of b₁ = the Compl of L & ( for a, b being Element of L holds the L_meet of b₁ . a,b = a *' b ) & the carrier of b₂ = the carrier of L & the L_join of b₂ = the L_join of L & the Compl of b₂ = the Compl of L & ( for a, b being Element of L holds the L_meet of b₂ . a,b = a *' b ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines CLatt ROBBINS1:def 11 :

for L being non empty ComplLattStr
for b₂ being strict OrthoLattStr holds
( b₂ = CLatt L iff ( the carrier of b₂ = the carrier of L & the L_join of b₂ = the L_join of L & the Compl of b₂ = the Compl of L & ( for a, b being Element of L holds the L_meet of b₂ . a,b = a *' b ) ) );

registration

let L be non empty ComplLattStr ;
cluster CLatt L -> non empty strict ;
coherence
not CLatt L is empty

proof end;

end;

registration

let L be non empty join-commutative ComplLattStr ;
cluster CLatt L -> join-commutative strict ;
coherence
CLatt L is join-commutative

proof end;

end;

registration

let L be non empty join-associative ComplLattStr ;
cluster CLatt L -> join-associative strict ;
coherence
CLatt L is join-associative

proof end;

end;

registration

let L be non empty join-commutative join-associative ComplLattStr ;
cluster CLatt L -> meet-commutative strict ;
coherence
CLatt L is meet-commutative

proof end;

end;

theorem :: ROBBINS1:35

for L being non empty ComplLattStr
for a, b being Element of L
for a', b' being Element of (CLatt L) st a = a' & b = b' holds
( a *' b = a' "/\" b' & a + b = a' "\/" b' & a ` = a' ` ) by Def11;

registration

let L be non empty join-commutative join-associative Huntington ComplLattStr ;
cluster CLatt L -> meet-associative meet-absorbing join-absorbing strict ;
coherence
( CLatt L is meet-associative & CLatt L is join-absorbing & CLatt L is meet-absorbing )

proof end;

end;

registration

let L be non empty Huntington ComplLattStr ;
cluster CLatt L -> strict Huntington ;
coherence
CLatt L is Huntington

proof end;

end;

registration

let L be non empty join-commutative join-associative Huntington ComplLattStr ;
cluster CLatt L -> lower-bounded strict ;
coherence
CLatt L is lower-bounded

proof end;

end;

theorem Th36: :: ROBBINS1:36

for L being non empty join-commutative join-associative Huntington ComplLattStr holds Bot L = Bottom (CLatt L)

proof end;

registration

let L be non empty join-commutative join-associative Huntington ComplLattStr ;
cluster CLatt L -> distributive bounded complemented strict ;
coherence
( CLatt L is complemented & CLatt L is distributive & CLatt L is bounded )

proof end;

end;

notation

let G be non empty ComplLattStr ;
let x be Element of G;
synonym - x for x ` ;

end;

definition

let G be non empty join-commutative ComplLattStr ;
redefine attr G is Huntington means :Def12: :: ROBBINS1:def 12
for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y;
compatibility
( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y )

proof end;

end;

:: deftheorem Def12 defines Huntington ROBBINS1:def 12 :

for G being non empty join-commutative ComplLattStr holds
( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y );

definition

let G be non empty ComplLattStr ;
attr G is with_idempotent_element means :Def13: :: ROBBINS1:def 13
ex x being Element of G st x + x = x;
correctness
;

end;

:: deftheorem Def13 defines with_idempotent_element ROBBINS1:def 13 :

for G being non empty ComplLattStr holds
( G is with_idempotent_element iff ex x being Element of G st x + x = x );

definition

let G be non empty ComplLattStr ;
let x, y be Element of G;
func \delta x,y -> Element of G equals :: ROBBINS1:def 14
- ((- x) + y);
coherence
- ((- x) + y) is Element of G ;

end;

:: deftheorem defines \delta ROBBINS1:def 14 :

for G being non empty ComplLattStr
for x, y being Element of G holds \delta x,y = - ((- x) + y);

definition

let G be non empty ComplLattStr ;
let x, y be Element of G;
func Expand x,y -> Element of G equals :: ROBBINS1:def 15
\delta (x + y),(\delta x,y);
coherence
\delta (x + y),(\delta x,y) is Element of G ;

end;

:: deftheorem defines Expand ROBBINS1:def 15 :

for G being non empty ComplLattStr
for x, y being Element of G holds Expand x,y = \delta (x + y),(\delta x,y);

definition

let G be non empty ComplLattStr ;
let x be Element of G;
func x _0 -> Element of G equals :: ROBBINS1:def 16
- ((- x) + x);
coherence
- ((- x) + x) is Element of G ;
func Double x -> Element of G equals :: ROBBINS1:def 17
x + x;
coherence
x + x is Element of G ;

end;

:: deftheorem defines _0 ROBBINS1:def 16 :

for G being non empty ComplLattStr
for x being Element of G holds x _0 = - ((- x) + x);

:: deftheorem defines Double ROBBINS1:def 17 :

for G being non empty ComplLattStr
for x being Element of G holds Double x = x + x;

definition

let G be non empty ComplLattStr ;
let x be Element of G;
func x _1 -> Element of G equals :: ROBBINS1:def 18
(x _0 ) + x;
coherence
(x _0 ) + x is Element of G ;
func x _2 -> Element of G equals :: ROBBINS1:def 19
(x _0 ) + (Double x);
coherence
(x _0 ) + (Double x) is Element of G ;
func x _3 -> Element of G equals :: ROBBINS1:def 20
(x _0 ) + ((Double x) + x);
coherence
(x _0 ) + ((Double x) + x) is Element of G ;
func x _4 -> Element of G equals :: ROBBINS1:def 21
(x _0 ) + ((Double x) + (Double x));
coherence
(x _0 ) + ((Double x) + (Double x)) is Element of G ;

end;

:: deftheorem defines _1 ROBBINS1:def 18 :

for G being non empty ComplLattStr
for x being Element of G holds x _1 = (x _0 ) + x;

:: deftheorem defines _2 ROBBINS1:def 19 :

for G being non empty ComplLattStr
for x being Element of G holds x _2 = (x _0 ) + (Double x);

:: deftheorem defines _3 ROBBINS1:def 20 :

for G being non empty ComplLattStr
for x being Element of G holds x _3 = (x _0 ) + ((Double x) + x);

:: deftheorem defines _4 ROBBINS1:def 21 :

for G being non empty ComplLattStr
for x being Element of G holds x _4 = (x _0 ) + ((Double x) + (Double x));

theorem Th37: :: ROBBINS1:37

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x, y being Element of G holds \delta (x + y),(\delta x,y) = y

proof end;

theorem :: ROBBINS1:38

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x, y being Element of G holds Expand x,y = y by Th37;

theorem :: ROBBINS1:39

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x, y, z being Element of G holds \delta ((- x) + y),z = - ((\delta x,y) + z) ;

theorem :: ROBBINS1:40

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta x,x = x _0 ;

theorem Th41: :: ROBBINS1:41

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta (Double x),(x _0 ) = x

proof end;

theorem Th42: :: ROBBINS1:42

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta (x _2 ),x = x _0

proof end;

theorem :: ROBBINS1:43

canceled;

theorem Th44: :: ROBBINS1:44

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds (x _4 ) + (x _0 ) = (x _3 ) + (x _1 )

proof end;

theorem Th45: :: ROBBINS1:45

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds (x _3 ) + (x _0 ) = (x _2 ) + (x _1 )

proof end;

theorem Th46: :: ROBBINS1:46

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds (x _3 ) + x = x _4

proof end;

theorem Th47: :: ROBBINS1:47

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta (x _3 ),(x _0 ) = x

proof end;

theorem :: ROBBINS1:48

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x, y, z being Element of G st - x = - y holds
\delta x,z = \delta y,z ;

theorem Th49: :: ROBBINS1:49

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x, y being Element of G holds \delta x,(- y) = \delta y,(- x)

proof end;

theorem Th50: :: ROBBINS1:50

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta (x _3 ),x = x _0

proof end;

theorem Th51: :: ROBBINS1:51

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta ((x _1 ) + (x _3 )),x = x _0

proof end;

theorem Th52: :: ROBBINS1:52

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta ((x _1 ) + (x _2 )),x = x _0

proof end;

theorem Th53: :: ROBBINS1:53

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta ((x _1 ) + (x _3 )),(x _0 ) = x

proof end;

definition

let G be non empty join-commutative join-associative Robbins ComplLattStr ;
let x be Element of G;
func \beta x -> Element of G equals :: ROBBINS1:def 22
((- ((x _1 ) + (x _3 ))) + x) + (- (x _3 ));
coherence
((- ((x _1 ) + (x _3 ))) + x) + (- (x _3 )) is Element of G ;

end;

:: deftheorem defines \beta ROBBINS1:def 22 :

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \beta x = ((- ((x _1 ) + (x _3 ))) + x) + (- (x _3 ));

theorem Th54: :: ROBBINS1:54

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta (\beta x),x = - (x _3 )

proof end;

theorem Th55: :: ROBBINS1:55

for G being non empty join-commutative join-associative Robbins ComplLattStr
for x being Element of G holds \delta (\beta x),x = - ((x _1 ) + (x _3 ))

proof end;

theorem :: ROBBINS1:56

for G being non empty join-commutative join-associative Robbins ComplLattStr ex y, z being Element of G st - (y + z) = - z

proof end;

theorem :: ROBBINS1:57

for G being non empty join-commutative join-associative Robbins ComplLattStr st ( for z being Element of G holds - (- z) = z ) holds
G is Huntington

proof end;

theorem Th58: :: ROBBINS1:58

for G being non empty join-commutative join-associative Robbins ComplLattStr st G is with_idempotent_element holds
G is Huntington

proof end;

registration

cluster TrivComplLat -> strict with_idempotent_element ;
coherence
TrivComplLat is with_idempotent_element

proof end;

end;

registration

cluster non empty join-commutative join-associative Robbins with_idempotent_element -> non empty join-commutative join-associative Robbins Huntington ComplLattStr ;
coherence
for b₁ being non empty join-commutative join-associative Robbins ComplLattStr st b₁ is with_idempotent_element holds
b₁ is Huntington by Th58;

end;

theorem Th59: :: ROBBINS1:59

for G being non empty join-commutative join-associative Robbins ComplLattStr st ex c, d being Element of G st c + d = c holds
G is Huntington

proof end;

theorem Th60: :: ROBBINS1:60

for G being non empty join-commutative join-associative Robbins ComplLattStr ex y, z being Element of G st y + z = z

proof end;

registration

cluster non empty join-commutative join-associative Robbins -> non empty join-commutative join-associative Huntington ComplLattStr ;
coherence
for b₁ being non empty join-commutative join-associative ComplLattStr st b₁ is Robbins holds
b₁ is Huntington

proof end;

end;

definition

let L be non empty OrthoLattStr ;
attr L is de_Morgan means :Def23: :: ROBBINS1:def 23
for x, y being Element of L holds x "/\" y = ((x ` ) "\/" (y ` )) ` ;

end;

:: deftheorem Def23 defines de_Morgan ROBBINS1:def 23 :

for L being non empty OrthoLattStr holds
( L is de_Morgan iff for x, y being Element of L holds x "/\" y = ((x ` ) "\/" (y ` )) ` );

registration

let L be non empty ComplLattStr ;
cluster CLatt L -> strict de_Morgan ;
coherence
CLatt L is de_Morgan

proof end;

end;

theorem Th61: :: ROBBINS1:61

for L being non empty join-commutative meet-commutative well-complemented OrthoLattStr
for x being Element of L holds
( x + (x ` ) = Top L & x "/\" (x ` ) = Bottom L )

proof end;

theorem Th62: :: ROBBINS1:62

for L being distributive bounded well-complemented preOrthoLattice holds (Top L) ` = Bottom L

proof end;

registration

cluster TrivOrtLat -> strict de_Morgan ;
coherence
TrivOrtLat is de_Morgan

proof end;

end;

registration

cluster Boolean strict Robbins Huntington de_Morgan OrthoLattStr ;
existence
ex b₁ being preOrthoLattice st
( b₁ is strict & b₁ is de_Morgan & b₁ is Boolean & b₁ is Robbins & b₁ is Huntington )

proof end;

end;

registration

cluster non empty join-commutative join-associative de_Morgan -> non empty meet-commutative OrthoLattStr ;
coherence
for b₁ being non empty OrthoLattStr st b₁ is join-associative & b₁ is join-commutative & b₁ is de_Morgan holds
b₁ is meet-commutative

proof end;

end;

theorem Th63: :: ROBBINS1:63

for L being Huntington de_Morgan preOrthoLattice holds Bot L = Bottom L

proof end;

registration

cluster Boolean well-complemented -> Huntington well-complemented OrthoLattStr ;
coherence
for b₁ being well-complemented preOrthoLattice st b₁ is Boolean holds
b₁ is Huntington

proof end;

end;

registration

cluster Huntington de_Morgan -> Boolean de_Morgan OrthoLattStr ;
coherence
for b₁ being de_Morgan preOrthoLattice st b₁ is Huntington holds
b₁ is Boolean

proof end;

end;

registration

cluster Robbins de_Morgan -> Boolean OrthoLattStr ;
coherence
for b₁ being preOrthoLattice st b₁ is Robbins & b₁ is de_Morgan holds
b₁ is Boolean ;
cluster Boolean well-complemented -> Robbins well-complemented OrthoLattStr ;
coherence
for b₁ being well-complemented preOrthoLattice st b₁ is Boolean holds
b₁ is Robbins

proof end;

end;