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


begin

definition
attrc1 is strict ;
struct ComplStr  ->  1-sorted ;
aggrComplStr(# carrier, Compl #) ->  ComplStr ;
sel Compl c1 ->  UnOp of the carrier of c1;
end;

definition
attrc1 is strict ;
struct ComplLLattStr  ->  \/-SemiLattStr , ComplStr ;
aggrComplLLattStr(# carrier, L_join, Compl #) ->  ComplLLattStr ;
end;

definition
attrc1 is strict ;
struct ComplULattStr  ->  /\-SemiLattStr , ComplStr ;
aggrComplULattStr(# carrier, L_meet, Compl #) ->  ComplULattStr ;
end;

definition
attrc1 is strict ;
struct OrthoLattStr  ->  ComplLLattStr , LattStr ;
aggrOrthoLattStr(# carrier, L_join, L_meet, Compl #) ->  OrthoLattStr ;
end;

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

:: deftheorem  defines TrivComplLat ROBBINS1:def_1_:_
 TrivComplLat = ComplLLattStr(# 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  -> 1 -element strict ;
coherence
 TrivComplLat is 1 -element
proofend;
cluster TrivOrtLat  -> 1 -element strict ;
coherence
 TrivOrtLat is 1 -element
proofend;
end;

registration
cluster1 -element strict for OrthoLattStr ;
existence
 ex b1 being OrthoLattStr st
( b1 is strict & b1 is 1 -element )
proofend;
cluster1 -element strict for ComplLLattStr ;
existence
 ex b1 being ComplLLattStr st
( b1 is strict & b1 is 1 -element )
proofend;
end;

registration
let L be 1 -element ComplLLattStr ;
cluster ComplStr(# the carrier of L, the Compl of L #) -> 1 -element ;
coherence
 ComplStr(# the carrier of L, the Compl of L #) is 1 -element
proofend;
end;

registration
cluster1 -element strict for ComplStr ;
existence
 ex b1 being ComplStr st
( b1 is strict & b1 is 1 -element )
proofend;
end;

definition
let L be non empty ComplStr ;
let x be Element of L;
funcx `  ->  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 ComplLLattStr ;
let 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;
funcx *' 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 ComplLLattStr
for x, y being Element of L holds x *' y = ((x `) "\/" (y `)) ` ;

definition
let L be non empty ComplLLattStr ;
attrL is Robbins  means :Def5: :: ROBBINS1:def 5
 for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x;
attrL 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 ComplLLattStr 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 ComplLLattStr 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 ;
attrG 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 )
proofend;
cluster TrivOrtLat  ->  join-commutative join-associative strict Robbins Huntington ;
coherence
 ( TrivOrtLat is join-commutative & TrivOrtLat is join-associative & TrivOrtLat is Huntington & TrivOrtLat is Robbins )
proofend;
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 )
proofend;
end;

registration
cluster non empty join-commutative join-associative strict Robbins Huntington join-idempotent for ComplLLattStr ;
existence
 ex b1 being non empty ComplLLattStr st
( b1 is strict & b1 is join-associative & b1 is join-commutative & b1 is Robbins & b1 is join-idempotent & b1 is Huntington )
proofend;
end;

registration
cluster non empty Lattice-like strict Robbins Huntington for OrthoLattStr ;
existence
 ex b1 being non empty OrthoLattStr st
( b1 is strict & b1 is Lattice-like & b1 is Robbins & b1 is Huntington )
proofend;
end;

definition
let L be non empty join-commutative ComplLLattStr ;
let x, y be Element of L;
:: original:+
redefine funcx + 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 ComplLLattStr
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 ComplLLattStr
for a being Element of L holds a + (a `) = (a `) + ((a `) `)
proofend;

theorem Th3: :: ROBBINS1:3
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for x being Element of L holds (x `) ` = x
proofend;

theorem Th4: :: ROBBINS1:4
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L holds a + (a `) = b + (b `)
proofend;

theorem Th5: :: ROBBINS1:5
for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ex c being Element of L st
for a being Element of L holds
( c + a = c & a + (a `) = c )
proofend;

theorem Th6: :: ROBBINS1:6
for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr holds L is upper-bounded
proofend;

registration
cluster non empty join-commutative join-associative Huntington join-idempotent  ->  non empty upper-bounded for ComplLLattStr ;
coherence
 for b1 being non empty ComplLLattStr st b1 is join-commutative & b1 is join-associative & b1 is join-idempotent & b1 is Huntington holds
b1 is upper-bounded by Th6;
end;

definition
let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ;
redefine func Top L means :Def8: :: ROBBINS1:def 8
 ex a being Element of L st it = a + (a `);
compatibility
 for b1 being M2( the carrier of L) holds
( b1 = Top L iff ex a being Element of L st b1 = a + (a `) )
proofend;
end;

:: deftheorem Def8 defines Top ROBBINS1:def_8_:_
 for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr
for b2 being M2( the carrier of b1) holds
( b2 = Top L iff ex a being Element of L st b2 = a + (a `) );

theorem Th7: :: ROBBINS1:7
for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ex c being Element of L st
for a being Element of L holds
( c *' a = c & (a + (a `)) ` = c )
proofend;

definition
let L be non empty join-commutative join-associative ComplLLattStr ;
let x, y be Element of L;
:: original:*'
redefine funcx *' y ->  Element of L;
commutativity
 for x, y being Element of L holds x *' y = y *' x
proofend;
end;

definition
let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ;
func Bot L ->  Element of L means :Def9: :: ROBBINS1:def 9
 for a being Element of L holds it *' a = it;
existence
 ex b1 being Element of L st
for a being Element of L holds b1 *' a = b1
proofend;
uniqueness
 for b1, b2 being Element of L st ( for a being Element of L holds b1 *' a = b1 ) & ( for a being Element of L holds b2 *' a = b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines Bot ROBBINS1:def_9_:_
 for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr
for b2 being Element of L holds
( b2 = Bot L iff for a being Element of L holds b2 *' a = b2 );

theorem Th8: :: ROBBINS1:8
for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr
for a being Element of L holds Bot L = (a + (a `)) `
proofend;

theorem Th9: :: ROBBINS1:9
for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr holds
( (Top L) ` = Bot L & Top L = (Bot L) ` )
proofend;

theorem Th10: :: ROBBINS1:10
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L st a ` = b ` holds
a = b
proofend;

theorem Th11: :: ROBBINS1:11
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L holds a + ((b + (b `)) `) = a
proofend;

theorem Th12: :: ROBBINS1:12
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a being Element of L holds a + a = a
proofend;

registration
cluster non empty join-commutative join-associative Huntington  ->  non empty join-idempotent for ComplLLattStr ;
coherence
 for b1 being non empty ComplLLattStr st b1 is join-commutative & b1 is join-associative & b1 is Huntington holds
b1 is join-idempotent
proofend;
end;

theorem Th13: :: ROBBINS1:13
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a being Element of L holds a + (Bot L) = a
proofend;

theorem :: ROBBINS1:14
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a being Element of L holds a *' (Top L) = a
proofend;

theorem Th15: :: ROBBINS1:15
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a being Element of L holds a *' (a `) = Bot L
proofend;

theorem Th16: :: ROBBINS1:16
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b, c being Element of L holds a *' (b *' c) = (a *' b) *' c
proofend;

theorem Th17: :: ROBBINS1:17
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L holds a + b = ((a `) *' (b `)) `
proofend;

theorem :: ROBBINS1:18
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a being Element of L holds a *' a = a
proofend;

theorem :: ROBBINS1:19
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a being Element of L holds a + (Top L) = Top L
proofend;

theorem Th20: :: ROBBINS1:20
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L holds a + (a *' b) = a
proofend;

theorem Th21: :: ROBBINS1:21
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L holds a *' (a + b) = a
proofend;

theorem Th22: :: ROBBINS1:22
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L st (a `) + b = Top L & (b `) + a = Top L holds
a = b
proofend;

theorem Th23: :: ROBBINS1:23
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L st a + b = Top L & a *' b = Bot L holds
a ` = b
proofend;

theorem Th24: :: ROBBINS1:24
for L being non empty join-commutative join-associative Huntington ComplLLattStr
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
proofend;

theorem Th25: :: ROBBINS1:25
for L being non empty join-commutative join-associative Huntington ComplLLattStr
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 )
proofend;

theorem Th26: :: ROBBINS1:26
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b, c being Element of L holds (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)
proofend;

theorem Th27: :: ROBBINS1:27
for L being non empty join-commutative join-associative Huntington ComplLLattStr
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 `))
proofend;

theorem Th28: :: ROBBINS1:28
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b, c being Element of L holds ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L
proofend;

theorem Th29: :: ROBBINS1:29
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b, c being Element of L holds ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L
proofend;

theorem Th30: :: ROBBINS1:30
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c)
proofend;

theorem :: ROBBINS1:31
for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c)
proofend;

begin

definition
let L be non empty OrthoLattStr ;
attrL 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 )
proofend;
end;

definition
mode preOrthoLattice is non empty Lattice-like OrthoLattStr ;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean strict well-complemented for OrthoLattStr ;
existence
 ex b1 being preOrthoLattice st
( b1 is strict & b1 is Boolean & b1 is well-complemented )
proofend;
end;

theorem Th32: :: ROBBINS1:32
for L being distributive well-complemented preOrthoLattice
for x being Element of L holds (x `) ` = x
proofend;

theorem Th33: :: ROBBINS1:33
for L being distributive bounded well-complemented preOrthoLattice
for x, y being Element of L holds x "/\" y = ((x `) "\/" (y `)) `
proofend;

begin

:: according to the definition given in \cite{LATTICES.ABS}
definition
let L be non empty ComplLLattStr ;
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 b1 being strict OrthoLattStr st
( the carrier of b1 = the carrier of L & the L_join of b1 = the L_join of L & the Compl of b1 = the Compl of L & ( for a, b being Element of L holds the L_meet of b1 . (a,b) = a *' b ) )
proofend;
uniqueness
 for b1, b2 being strict OrthoLattStr st the carrier of b1 = the carrier of L & the L_join of b1 = the L_join of L & the Compl of b1 = the Compl of L & ( for a, b being Element of L holds the L_meet of b1 . (a,b) = a *' b ) & the carrier of b2 = the carrier of L & the L_join of b2 = the L_join of L & the Compl of b2 = the Compl of L & ( for a, b being Element of L holds the L_meet of b2 . (a,b) = a *' b ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines CLatt ROBBINS1:def_11_:_
 for L being non empty ComplLLattStr
for b2 being strict OrthoLattStr holds
( b2 = CLatt L iff ( the carrier of b2 = the carrier of L & the L_join of b2 = the L_join of L & the Compl of b2 = the Compl of L & ( for a, b being Element of L holds the L_meet of b2 . (a,b) = a *' b ) ) );

registration
let L be non empty ComplLLattStr ;
cluster CLatt L ->  non empty strict ;
coherence
 not CLatt L is empty
proofend;
end;

registration
let L be non empty join-commutative ComplLLattStr ;
cluster CLatt L ->  join-commutative strict ;
coherence
 CLatt L is join-commutative
proofend;
end;

registration
let L be non empty join-associative ComplLLattStr ;
cluster CLatt L ->  join-associative strict ;
coherence
 CLatt L is join-associative
proofend;
end;

registration
let L be non empty join-commutative join-associative ComplLLattStr ;
cluster CLatt L ->  meet-commutative strict ;
coherence
 CLatt L is meet-commutative
proofend;
end;

theorem :: ROBBINS1:34
for L being non empty ComplLLattStr
for a, b being Element of L
for 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 non empty join-commutative join-associative Huntington ComplLLattStr ;
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 )
proofend;
end;

registration
let L be non empty Huntington ComplLLattStr ;
cluster CLatt L ->  strict Huntington ;
coherence
 CLatt L is Huntington
proofend;
end;

registration
let L be non empty join-commutative join-associative Huntington ComplLLattStr ;
cluster CLatt L ->  lower-bounded strict ;
coherence
 CLatt L is lower-bounded
proofend;
end;

theorem Th35: :: ROBBINS1:35
for L being non empty join-commutative join-associative Huntington ComplLLattStr holds Bot L = Bottom (CLatt L)
proofend;

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

begin

notation
let G be non empty ComplLLattStr ;
let x be Element of G;
synonym  - x for x ` ;
end;

definition
let G be non empty join-commutative ComplLLattStr ;
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 )
proofend;
end;

:: deftheorem Def12 defines Huntington ROBBINS1:def_12_:_
 for G being non empty join-commutative ComplLLattStr holds
( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y );

definition
let G be non empty ComplLLattStr ;
attrG 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 ComplLLattStr holds
( G is with_idempotent_element iff ex x being Element of G st x + x = x );

definition
let G be non empty ComplLLattStr ;
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 ComplLLattStr
for x, y being Element of G holds \delta (x,y) = - ((- x) + y);

definition
let G be non empty ComplLLattStr ;
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 ComplLLattStr
for x, y being Element of G holds Expand (x,y) = \delta ((x + y),(\delta (x,y)));

definition
let G be non empty ComplLLattStr ;
let x be Element of G;
funcx _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 ComplLLattStr
for x being Element of G holds x _0 = - ((- x) + x);

:: deftheorem  defines Double ROBBINS1:def_17_:_
 for G being non empty ComplLLattStr
for x being Element of G holds Double x = x + x;

definition
let G be non empty ComplLLattStr ;
let x be Element of G;
funcx _1  ->  Element of G equals :: ROBBINS1:def 18
(x _0) + x;
coherence
 (x _0) + x is Element of G ;
funcx _2  ->  Element of G equals :: ROBBINS1:def 19
(x _0) + (Double x);
coherence
 (x _0) + (Double x) is Element of G ;
funcx _3  ->  Element of G equals :: ROBBINS1:def 20
(x _0) + ((Double x) + x);
coherence
 (x _0) + ((Double x) + x) is Element of G ;
funcx _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 ComplLLattStr
for x being Element of G holds x _1 = (x _0) + x;

:: deftheorem  defines _2 ROBBINS1:def_19_:_
 for G being non empty ComplLLattStr
for x being Element of G holds x _2 = (x _0) + (Double x);

:: deftheorem  defines _3 ROBBINS1:def_20_:_
 for G being non empty ComplLLattStr
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 ComplLLattStr
for x being Element of G holds x _4 = (x _0) + ((Double x) + (Double x));

theorem Th36: :: ROBBINS1:36
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x, y being Element of G holds \delta ((x + y),(\delta (x,y))) = y
proofend;

theorem :: ROBBINS1:37
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x, y being Element of G holds Expand (x,y) = y by Th36;

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

theorem :: ROBBINS1:39
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta (x,x) = x _0 ;

theorem Th40: :: ROBBINS1:40
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta ((Double x),(x _0)) = x
proofend;

theorem Th41: :: ROBBINS1:41
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta ((x _2),x) = x _0
proofend;

theorem Th42: :: ROBBINS1:42
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds (x _4) + (x _0) = (x _3) + (x _1)
proofend;

theorem Th43: :: ROBBINS1:43
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds (x _3) + (x _0) = (x _2) + (x _1)
proofend;

theorem Th44: :: ROBBINS1:44
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds (x _3) + x = x _4
proofend;

theorem Th45: :: ROBBINS1:45
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta ((x _3),(x _0)) = x
proofend;

theorem :: ROBBINS1:46
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x, y, z being Element of G st - x = - y holds
\delta (x,z) = \delta (y,z) ;

theorem Th47: :: ROBBINS1:47
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x, y being Element of G holds \delta (x,(- y)) = \delta (y,(- x))
proofend;

theorem Th48: :: ROBBINS1:48
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta ((x _3),x) = x _0
proofend;

theorem Th49: :: ROBBINS1:49
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta (((x _1) + (x _3)),x) = x _0
proofend;

theorem Th50: :: ROBBINS1:50
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta (((x _1) + (x _2)),x) = x _0
proofend;

theorem Th51: :: ROBBINS1:51
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta (((x _1) + (x _3)),(x _0)) = x
proofend;

definition
let G be non empty join-commutative join-associative Robbins ComplLLattStr ;
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 ComplLLattStr
for x being Element of G holds \beta x = ((- ((x _1) + (x _3))) + x) + (- (x _3));

theorem Th52: :: ROBBINS1:52
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta ((\beta x),x) = - (x _3)
proofend;

theorem Th53: :: ROBBINS1:53
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta ((\beta x),x) = - ((x _1) + (x _3))
proofend;

theorem :: ROBBINS1:54
for G being non empty join-commutative join-associative Robbins ComplLLattStr ex y, z being Element of G st - (y + z) = - z
proofend;

begin

theorem :: ROBBINS1:55
for G being non empty join-commutative join-associative Robbins ComplLLattStr st ( for z being Element of G holds - (- z) = z ) holds
G is Huntington
proofend;

theorem Th56: :: ROBBINS1:56
for G being non empty join-commutative join-associative Robbins ComplLLattStr st G is with_idempotent_element holds
G is Huntington
proofend;

registration
cluster TrivComplLat  ->  strict with_idempotent_element ;
coherence
 TrivComplLat is with_idempotent_element
proofend;
end;

registration
cluster non empty join-commutative join-associative Robbins with_idempotent_element  ->  non empty join-commutative join-associative Robbins Huntington for ComplLLattStr ;
coherence
 for b1 being non empty join-commutative join-associative Robbins ComplLLattStr st b1 is with_idempotent_element holds
b1 is Huntington by Th56;
end;

theorem Th57: :: ROBBINS1:57
for G being non empty join-commutative join-associative Robbins ComplLLattStr st ex c, d being Element of G st c + d = c holds
G is Huntington
proofend;

theorem Th58: :: ROBBINS1:58
for G being non empty join-commutative join-associative Robbins ComplLLattStr ex y, z being Element of G st y + z = z
proofend;

registration
cluster non empty join-commutative join-associative Robbins  ->  non empty join-commutative join-associative Huntington for ComplLLattStr ;
coherence
 for b1 being non empty join-commutative join-associative ComplLLattStr st b1 is Robbins holds
b1 is Huntington
proofend;
end;

definition
let L be non empty OrthoLattStr ;
attrL 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 ComplLLattStr ;
cluster CLatt L ->  strict de_Morgan ;
coherence
 CLatt L is de_Morgan
proofend;
end;

theorem Th59: :: ROBBINS1:59
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 )
proofend;

theorem Th60: :: ROBBINS1:60
for L being distributive bounded well-complemented preOrthoLattice holds (Top L) ` = Bottom L
proofend;

registration
cluster TrivOrtLat  ->  strict de_Morgan ;
coherence
 TrivOrtLat is de_Morgan
proofend;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean strict Robbins Huntington de_Morgan for OrthoLattStr ;
existence
 ex b1 being preOrthoLattice st
( b1 is strict & b1 is de_Morgan & b1 is Boolean & b1 is Robbins & b1 is Huntington )
proofend;
end;

registration
cluster non empty join-commutative join-associative de_Morgan  ->  non empty meet-commutative for OrthoLattStr ;
coherence
 for b1 being non empty OrthoLattStr st b1 is join-associative & b1 is join-commutative & b1 is de_Morgan holds
b1 is meet-commutative
proofend;
end;

theorem Th61: :: ROBBINS1:61
for L being Huntington de_Morgan preOrthoLattice holds Bot L = Bottom L
proofend;

registration
cluster non empty Lattice-like Boolean well-complemented  ->  Huntington well-complemented for OrthoLattStr ;
coherence
 for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
b1 is Huntington
proofend;
end;

registration
cluster non empty Lattice-like Huntington de_Morgan  ->  Boolean de_Morgan for OrthoLattStr ;
coherence
 for b1 being de_Morgan preOrthoLattice st b1 is Huntington holds
b1 is Boolean
proofend;
end;

registration
cluster non empty Lattice-like Robbins de_Morgan  ->  Boolean for OrthoLattStr ;
coherence
 for b1 being preOrthoLattice st b1 is Robbins & b1 is de_Morgan holds
b1 is Boolean ;
cluster non empty Lattice-like Boolean well-complemented  ->  Robbins well-complemented for OrthoLattStr ;
coherence
 for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
b1 is Robbins
proofend;
end;