:: Robbins Algebras vs. Boolean Algebras
:: by Adam Grabowski
::
:: Received June 12, 2001
:: Copyright (c) 2001-2026 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;
definitions LATTICES;
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; :: redefines + (ROBBINS1, synonym) → "\/" (LATTICES, definition)
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 :: redefines Top (LATTICES, definition)
: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; :: redefines *' (ROBBINS1, definition)
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 :: redefines Huntington (ROBBINS1, definition)
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;