:: Robbins Algebras vs. Boolean Algebras
:: by Adam Grabowski
::
:: Received June 12, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users
begin
definition
attr
c
1
is
strict
;
struct
ComplStr
->
1-sorted
;
aggr
ComplStr
(#
carrier
,
Compl
#)
->
ComplStr
;
sel
Compl
c
1
->
UnOp
of the
carrier
of
c
1
;
end;
definition
attr
c
1
is
strict
;
struct
ComplLLattStr
->
\/-SemiLattStr
,
ComplStr
;
aggr
ComplLLattStr
(#
carrier
,
L_join
,
Compl
#)
->
ComplLLattStr
;
end;
definition
attr
c
1
is
strict
;
struct
ComplULattStr
->
/\-SemiLattStr
,
ComplStr
;
aggr
ComplULattStr
(#
carrier
,
L_meet
,
Compl
#)
->
ComplULattStr
;
end;
definition
attr
c
1
is
strict
;
struct
OrthoLattStr
->
ComplLLattStr
,
LattStr
;
aggr
OrthoLattStr
(#
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
proof
end;
cluster
TrivOrtLat
->
1
-element
strict
;
coherence
TrivOrtLat
is 1
-element
proof
end;
end;
registration
cluster
1
-element
strict
for
OrthoLattStr
;
existence
ex
b
1
being
OrthoLattStr
st
(
b
1
is
strict
&
b
1
is 1
-element
)
proof
end;
cluster
1
-element
strict
for
ComplLLattStr
;
existence
ex
b
1
being
ComplLLattStr
st
(
b
1
is
strict
&
b
1
is 1
-element
)
proof
end;
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
proof
end;
end;
registration
cluster
1
-element
strict
for
ComplStr
;
existence
ex
b
1
being
ComplStr
st
(
b
1
is
strict
&
b
1
is 1
-element
)
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
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
;
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
ComplLLattStr
for
x
,
y
being
Element
of
L
holds
x
*'
y
=
(
(
x
`
)
"\/"
(
y
`
)
)
`
;
definition
let
L
be non
empty
ComplLLattStr
;
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
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
;
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
for
ComplLLattStr
;
existence
ex
b
1
being non
empty
ComplLLattStr
st
(
b
1
is
strict
&
b
1
is
join-associative
&
b
1
is
join-commutative
&
b
1
is
Robbins
&
b
1
is
join-idempotent
&
b
1
is
Huntington
)
proof
end;
end;
registration
cluster
non
empty
Lattice-like
strict
Robbins
Huntington
for
OrthoLattStr
;
existence
ex
b
1
being non
empty
OrthoLattStr
st
(
b
1
is
strict
&
b
1
is
Lattice-like
&
b
1
is
Robbins
&
b
1
is
Huntington
)
proof
end;
end;
definition
let
L
be non
empty
join-commutative
ComplLLattStr
;
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
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
`
)
`
)
proof
end;
theorem
Th3
:
:: ROBBINS1:3
for
L
being non
empty
join-commutative
join-associative
Huntington
ComplLLattStr
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
ComplLLattStr
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
ComplLLattStr
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
ComplLLattStr
holds
L
is
upper-bounded
proof
end;
registration
cluster
non
empty
join-commutative
join-associative
Huntington
join-idempotent
->
non
empty
upper-bounded
for
ComplLLattStr
;
coherence
for
b
1
being non
empty
ComplLLattStr
st
b
1
is
join-commutative
&
b
1
is
join-associative
&
b
1
is
join-idempotent
&
b
1
is
Huntington
holds
b
1
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
b
1
being
M2
( the
carrier
of
L
) holds
(
b
1
=
Top
L
iff ex
a
being
Element
of
L
st
b
1
=
a
+
(
a
`
)
)
proof
end;
end;
::
deftheorem
Def8
defines
Top
ROBBINS1:def 8 :
for
L
being non
empty
join-commutative
join-associative
Huntington
join-idempotent
ComplLLattStr
for
b
2
being
M2
( the
carrier
of
b
1
) holds
(
b
2
=
Top
L
iff ex
a
being
Element
of
L
st
b
2
=
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
)
proof
end;
definition
let
L
be non
empty
join-commutative
join-associative
ComplLLattStr
;
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
proof
end;
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
b
1
being
Element
of
L
st
for
a
being
Element
of
L
holds
b
1
*'
a
=
b
1
proof
end;
uniqueness
for
b
1
,
b
2
being
Element
of
L
st ( for
a
being
Element
of
L
holds
b
1
*'
a
=
b
1
) & ( for
a
being
Element
of
L
holds
b
2
*'
a
=
b
2
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def9
defines
Bot
ROBBINS1:def 9 :
for
L
being non
empty
join-commutative
join-associative
Huntington
join-idempotent
ComplLLattStr
for
b
2
being
Element
of
L
holds
(
b
2
=
Bot
L
iff for
a
being
Element
of
L
holds
b
2
*'
a
=
b
2
);
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
`
)
)
`
proof
end;
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
)
`
)
proof
end;
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
proof
end;
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
proof
end;
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
proof
end;
registration
cluster
non
empty
join-commutative
join-associative
Huntington
->
non
empty
join-idempotent
for
ComplLLattStr
;
coherence
for
b
1
being non
empty
ComplLLattStr
st
b
1
is
join-commutative
&
b
1
is
join-associative
&
b
1
is
Huntington
holds
b
1
is
join-idempotent
proof
end;
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
proof
end;
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
proof
end;
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
proof
end;
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
proof
end;
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
`
)
)
`
proof
end;
theorem
:: ROBBINS1:18
for
L
being non
empty
join-commutative
join-associative
Huntington
ComplLLattStr
for
a
being
Element
of
L
holds
a
*'
a
=
a
proof
end;
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
proof
end;
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
proof
end;
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
proof
end;
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
proof
end;
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
proof
end;
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
proof
end;
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
)
proof
end;
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
)
proof
end;
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
`
)
)
proof
end;
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
proof
end;
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
proof
end;
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
)
proof
end;
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
)
proof
end;
begin
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
non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
Boolean
strict
well-complemented
for
OrthoLattStr
;
existence
ex
b
1
being
preOrthoLattice
st
(
b
1
is
strict
&
b
1
is
Boolean
&
b
1
is
well-complemented
)
proof
end;
end;
theorem
Th32
:
:: ROBBINS1:32
for
L
being
distributive
well-complemented
preOrthoLattice
for
x
being
Element
of
L
holds
(
x
`
)
`
=
x
proof
end;
theorem
Th33
:
:: ROBBINS1:33
for
L
being
distributive
bounded
well-complemented
preOrthoLattice
for
x
,
y
being
Element
of
L
holds
x
"/\"
y
=
(
(
x
`
)
"\/"
(
y
`
)
)
`
proof
end;
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
b
1
being
strict
OrthoLattStr
st
( the
carrier
of
b
1
=
the
carrier
of
L
& the
L_join
of
b
1
=
the
L_join
of
L
& the
Compl
of
b
1
=
the
Compl
of
L
& ( for
a
,
b
being
Element
of
L
holds the
L_meet
of
b
1
.
(
a
,
b
)
=
a
*'
b
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
strict
OrthoLattStr
st the
carrier
of
b
1
=
the
carrier
of
L
& the
L_join
of
b
1
=
the
L_join
of
L
& the
Compl
of
b
1
=
the
Compl
of
L
& ( for
a
,
b
being
Element
of
L
holds the
L_meet
of
b
1
.
(
a
,
b
)
=
a
*'
b
) & the
carrier
of
b
2
=
the
carrier
of
L
& the
L_join
of
b
2
=
the
L_join
of
L
& the
Compl
of
b
2
=
the
Compl
of
L
& ( for
a
,
b
being
Element
of
L
holds the
L_meet
of
b
2
.
(
a
,
b
)
=
a
*'
b
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def11
defines
CLatt
ROBBINS1:def 11 :
for
L
being non
empty
ComplLLattStr
for
b
2
being
strict
OrthoLattStr
holds
(
b
2
=
CLatt
L
iff ( the
carrier
of
b
2
=
the
carrier
of
L
& the
L_join
of
b
2
=
the
L_join
of
L
& the
Compl
of
b
2
=
the
Compl
of
L
& ( for
a
,
b
being
Element
of
L
holds the
L_meet
of
b
2
.
(
a
,
b
)
=
a
*'
b
) ) );
registration
let
L
be non
empty
ComplLLattStr
;
cluster
CLatt
L
->
non
empty
strict
;
coherence
not
CLatt
L
is
empty
proof
end;
end;
registration
let
L
be non
empty
join-commutative
ComplLLattStr
;
cluster
CLatt
L
->
join-commutative
strict
;
coherence
CLatt
L
is
join-commutative
proof
end;
end;
registration
let
L
be non
empty
join-associative
ComplLLattStr
;
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
ComplLLattStr
;
cluster
CLatt
L
->
meet-commutative
strict
;
coherence
CLatt
L
is
meet-commutative
proof
end;
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
)
proof
end;
end;
registration
let
L
be non
empty
Huntington
ComplLLattStr
;
cluster
CLatt
L
->
strict
Huntington
;
coherence
CLatt
L
is
Huntington
proof
end;
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
proof
end;
end;
theorem
Th35
:
:: ROBBINS1:35
for
L
being non
empty
join-commutative
join-associative
Huntington
ComplLLattStr
holds
Bot
L
=
Bottom
(
CLatt
L
)
proof
end;
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
)
proof
end;
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
)
proof
end;
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
;
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
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
;
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
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
;
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
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
proof
end;
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
proof
end;
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
proof
end;
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
)
proof
end;
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
)
proof
end;
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
proof
end;
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
proof
end;
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
)
)
proof
end;
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
proof
end;
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
proof
end;
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
proof
end;
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
proof
end;
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
)
proof
end;
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
)
)
proof
end;
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
proof
end;
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
proof
end;
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
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
for
ComplLLattStr
;
coherence
for
b
1
being non
empty
join-commutative
join-associative
Robbins
ComplLLattStr
st
b
1
is
with_idempotent_element
holds
b
1
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
proof
end;
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
proof
end;
registration
cluster
non
empty
join-commutative
join-associative
Robbins
->
non
empty
join-commutative
join-associative
Huntington
for
ComplLLattStr
;
coherence
for
b
1
being non
empty
join-commutative
join-associative
ComplLLattStr
st
b
1
is
Robbins
holds
b
1
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
ComplLLattStr
;
cluster
CLatt
L
->
strict
de_Morgan
;
coherence
CLatt
L
is
de_Morgan
proof
end;
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
)
proof
end;
theorem
Th60
:
:: ROBBINS1:60
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
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
b
1
being
preOrthoLattice
st
(
b
1
is
strict
&
b
1
is
de_Morgan
&
b
1
is
Boolean
&
b
1
is
Robbins
&
b
1
is
Huntington
)
proof
end;
end;
registration
cluster
non
empty
join-commutative
join-associative
de_Morgan
->
non
empty
meet-commutative
for
OrthoLattStr
;
coherence
for
b
1
being non
empty
OrthoLattStr
st
b
1
is
join-associative
&
b
1
is
join-commutative
&
b
1
is
de_Morgan
holds
b
1
is
meet-commutative
proof
end;
end;
theorem
Th61
:
:: ROBBINS1:61
for
L
being
Huntington
de_Morgan
preOrthoLattice
holds
Bot
L
=
Bottom
L
proof
end;
registration
cluster
non
empty
Lattice-like
Boolean
well-complemented
->
Huntington
well-complemented
for
OrthoLattStr
;
coherence
for
b
1
being
well-complemented
preOrthoLattice
st
b
1
is
Boolean
holds
b
1
is
Huntington
proof
end;
end;
registration
cluster
non
empty
Lattice-like
Huntington
de_Morgan
->
Boolean
de_Morgan
for
OrthoLattStr
;
coherence
for
b
1
being
de_Morgan
preOrthoLattice
st
b
1
is
Huntington
holds
b
1
is
Boolean
proof
end;
end;
registration
cluster
non
empty
Lattice-like
Robbins
de_Morgan
->
Boolean
for
OrthoLattStr
;
coherence
for
b
1
being
preOrthoLattice
st
b
1
is
Robbins
&
b
1
is
de_Morgan
holds
b
1
is
Boolean
;
cluster
non
empty
Lattice-like
Boolean
well-complemented
->
Robbins
well-complemented
for
OrthoLattStr
;
coherence
for
b
1
being
well-complemented
preOrthoLattice
st
b
1
is
Boolean
holds
b
1
is
Robbins
proof
end;
end;