:: Algebra of Normal Forms
:: by Andrzej Trybulec
::
:: Received October 5, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

let A, B be non empty preBoolean set ;
let x, y be Element of [:A,B:];
pred x c= y means :: NORMFORM:def 1
( x `1 c= y `1 & x `2 c= y `2 );
reflexivity
for x being Element of [:A,B:] holds
( x `1 c= x `1 & x `2 c= x `2 ) ;
func x \/ y -> Element of [:A,B:] equals :: NORMFORM:def 2
[((x `1) \/ (y `1)),((x `2) \/ (y `2))];
correctness
coherence
[((x `1) \/ (y `1)),((x `2) \/ (y `2))] is Element of [:A,B:];
;
commutativity
for b₁, x, y being Element of [:A,B:] st b₁ = [((x `1) \/ (y `1)),((x `2) \/ (y `2))] holds
b₁ = [((y `1) \/ (x `1)),((y `2) \/ (x `2))] ;
idempotence
for x being Element of [:A,B:] holds x = [((x `1) \/ (x `1)),((x `2) \/ (x `2))] by MCART_1:23;
func x /\ y -> Element of [:A,B:] equals :: NORMFORM:def 3
[((x `1) /\ (y `1)),((x `2) /\ (y `2))];
correctness
coherence
[((x `1) /\ (y `1)),((x `2) /\ (y `2))] is Element of [:A,B:];
;
commutativity
for b₁, x, y being Element of [:A,B:] st b₁ = [((x `1) /\ (y `1)),((x `2) /\ (y `2))] holds
b₁ = [((y `1) /\ (x `1)),((y `2) /\ (x `2))] ;
idempotence
for x being Element of [:A,B:] holds x = [((x `1) /\ (x `1)),((x `2) /\ (x `2))] by MCART_1:23;
func x \ y -> Element of [:A,B:] equals :: NORMFORM:def 4
[((x `1) \ (y `1)),((x `2) \ (y `2))];
correctness
coherence
[((x `1) \ (y `1)),((x `2) \ (y `2))] is Element of [:A,B:];
;
func x \+\ y -> Element of [:A,B:] equals :: NORMFORM:def 5
[((x `1) \+\ (y `1)),((x `2) \+\ (y `2))];
correctness
coherence
[((x `1) \+\ (y `1)),((x `2) \+\ (y `2))] is Element of [:A,B:];
;
commutativity
for b₁, x, y being Element of [:A,B:] st b₁ = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))] holds
b₁ = [((y `1) \+\ (x `1)),((y `2) \+\ (x `2))] ;

end;

:: deftheorem defines c= NORMFORM:def 1 :
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds
( x c= y iff ( x `1 c= y `1 & x `2 c= y `2 ) );

:: deftheorem defines \/ NORMFORM:def 2 :
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x \/ y = [((x `1) \/ (y `1)),((x `2) \/ (y `2))];

:: deftheorem defines /\ NORMFORM:def 3 :
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x /\ y = [((x `1) /\ (y `1)),((x `2) /\ (y `2))];

:: deftheorem defines \ NORMFORM:def 4 :
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x \ y = [((x `1) \ (y `1)),((x `2) \ (y `2))];

:: deftheorem defines \+\ NORMFORM:def 5 :
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x \+\ y = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))];

theorem :: NORMFORM:1

canceled;

theorem :: NORMFORM:2

canceled;

theorem :: NORMFORM:3

canceled;

theorem Th4: :: NORMFORM:4

for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] st a c= b & b c= a holds
a = b

proof end;

theorem Th5: :: NORMFORM:5

for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] st a c= b & b c= c holds
a c= c

proof end;

theorem :: NORMFORM:6

canceled;

theorem :: NORMFORM:7

canceled;

theorem :: NORMFORM:8

canceled;

theorem :: NORMFORM:9

canceled;

theorem :: NORMFORM:10

canceled;

theorem :: NORMFORM:11

canceled;

theorem :: NORMFORM:12

canceled;

theorem :: NORMFORM:13

canceled;

theorem :: NORMFORM:14

canceled;

theorem :: NORMFORM:15

canceled;

theorem Th16: :: NORMFORM:16

for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] holds (a \/ b) \/ c = a \/ (b \/ c)

proof end;

theorem :: NORMFORM:17

canceled;

theorem :: NORMFORM:18

canceled;

theorem :: NORMFORM:19

for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] holds (a /\ b) /\ c = a /\ (b /\ c)

proof end;

theorem Th20: :: NORMFORM:20

for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] holds a /\ (b \/ c) = (a /\ b) \/ (a /\ c)

proof end;

theorem Th21: :: NORMFORM:21

for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] holds a \/ (b /\ a) = a

proof end;

theorem Th22: :: NORMFORM:22

for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] holds a /\ (b \/ a) = a

proof end;

theorem :: NORMFORM:23

canceled;

theorem :: NORMFORM:24

for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] holds a \/ (b /\ c) = (a \/ b) /\ (a \/ c)

proof end;

theorem Th25: :: NORMFORM:25

for A, B being non empty preBoolean set
for a, c, b being Element of [:A,B:] st a c= c & b c= c holds
a \/ b c= c

proof end;

theorem Th26: :: NORMFORM:26

for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] holds
( a c= a \/ b & b c= a \/ b )

proof end;

theorem :: NORMFORM:27

for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] st a = a \/ b holds
b c= a by Th26;

theorem Th28: :: NORMFORM:28

for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] st a c= b holds
( c \/ a c= c \/ b & a \/ c c= b \/ c )

proof end;

theorem :: NORMFORM:29

for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] holds (a \ b) \/ b = a \/ b

proof end;

theorem :: NORMFORM:30

for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] st a \ b c= c holds
a c= b \/ c

proof end;

theorem :: NORMFORM:31

for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] st a c= b \/ c holds
a \ c c= b

proof end;

definition

let A be set ;
func FinPairUnion A -> BinOp of [:(Fin A),(Fin A):] means :Def6: :: NORMFORM:def 6
for x, y being Element of [:(Fin A),(Fin A):] holds it . (x,y) = x \/ y;
existence
ex b₁ being BinOp of [:(Fin A),(Fin A):] st
for x, y being Element of [:(Fin A),(Fin A):] holds b₁ . (x,y) = x \/ y

proof end;

uniqueness
for b₁, b₂ being BinOp of [:(Fin A),(Fin A):] st ( for x, y being Element of [:(Fin A),(Fin A):] holds b₁ . (x,y) = x \/ y ) & ( for x, y being Element of [:(Fin A),(Fin A):] holds b₂ . (x,y) = x \/ y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines FinPairUnion NORMFORM:def 6 :
for A being set
for b₂ being BinOp of [:(Fin A),(Fin A):] holds
( b₂ = FinPairUnion A iff for x, y being Element of [:(Fin A),(Fin A):] holds b₂ . (x,y) = x \/ y );

definition

let X be non empty set ;
let A be set ;
let B be Element of Fin X;
let f be Function of X,[:(Fin A),(Fin A):];
func FinPairUnion (B,f) -> Element of [:(Fin A),(Fin A):] equals :: NORMFORM:def 7
(FinPairUnion A) $$ (B,f);
correctness
coherence
(FinPairUnion A) $$ (B,f) is Element of [:(Fin A),(Fin A):];
;

end;

:: deftheorem defines FinPairUnion NORMFORM:def 7 :
for X being non empty set
for A being set
for B being Element of Fin X
for f being Function of X,[:(Fin A),(Fin A):] holds FinPairUnion (B,f) = (FinPairUnion A) $$ (B,f);

Lm1: for A being set holds FinPairUnion A is idempotent

proof end;

Lm2: for A being set holds FinPairUnion A is commutative

proof end;

Lm3: for A being set holds FinPairUnion A is associative

proof end;

registration

let A be set ;
cluster FinPairUnion A -> commutative associative idempotent ;
coherence
( FinPairUnion A is commutative & FinPairUnion A is idempotent & FinPairUnion A is associative ) by Lm1, Lm2, Lm3;

end;

theorem :: NORMFORM:32

canceled;

theorem :: NORMFORM:33

canceled;

theorem :: NORMFORM:34

canceled;

theorem :: NORMFORM:35

for A being set
for X being non empty set
for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)

proof end;

theorem Th36: :: NORMFORM:36

for A being set holds [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A

proof end;

theorem Th37: :: NORMFORM:37

for A being set holds FinPairUnion A is having_a_unity

proof end;

theorem Th38: :: NORMFORM:38

for A being set holds the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)]

proof end;

theorem Th39: :: NORMFORM:39

for A being set
for x being Element of [:(Fin A),(Fin A):] holds the_unity_wrt (FinPairUnion A) c= x

proof end;

theorem :: NORMFORM:40

for A being set
for X being non empty set
for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c

proof end;

theorem :: NORMFORM:41

for A being set
for X being non empty set
for B being Element of Fin X
for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds
FinPairUnion (B,f) = FinPairUnion (B,g)

proof end;

definition

let X be set ;
func DISJOINT_PAIRS X -> Subset of [:(Fin X),(Fin X):] equals :: NORMFORM:def 8
{ a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;
coherence
{ a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } is Subset of [:(Fin X),(Fin X):]

proof end;

end;

:: deftheorem defines DISJOINT_PAIRS NORMFORM:def 8 :
for X being set holds DISJOINT_PAIRS X = { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;

registration

let X be set ;
cluster DISJOINT_PAIRS X -> non empty ;
coherence
not DISJOINT_PAIRS X is empty

proof end;

end;

theorem Th42: :: NORMFORM:42

for X being set
for y being Element of [:(Fin X),(Fin X):] holds
( y in DISJOINT_PAIRS X iff y `1 misses y `2 )

proof end;

theorem :: NORMFORM:43

for X being set
for y, x being Element of [:(Fin X),(Fin X):] st y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X holds
( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} )

proof end;

theorem :: NORMFORM:44

for X being set
for a being Element of DISJOINT_PAIRS X holds a `1 misses a `2 by Th42;

theorem Th45: :: NORMFORM:45

for X being set
for x being Element of [:(Fin X),(Fin X):]
for b being Element of DISJOINT_PAIRS X st x c= b holds
x is Element of DISJOINT_PAIRS X

proof end;

theorem Th46: :: NORMFORM:46

for X being set
for a being Element of DISJOINT_PAIRS X
for x being set holds
( not x in a `1 or not x in a `2 )

proof end;

theorem :: NORMFORM:47

for X being set
for a, b being Element of DISJOINT_PAIRS X st not a \/ b in DISJOINT_PAIRS X holds
ex p being Element of X st
( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )

proof end;

theorem :: NORMFORM:48

canceled;

theorem :: NORMFORM:49

for X being set
for x being Element of [:(Fin X),(Fin X):] st x `1 misses x `2 holds
x is Element of DISJOINT_PAIRS X by Th42;

theorem :: NORMFORM:50

for X being set
for a being Element of DISJOINT_PAIRS X
for V, W being set st V c= a `1 & W c= a `2 holds
[V,W] is Element of DISJOINT_PAIRS X

proof end;

Lm4: for A being set holds {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b }

proof end;

definition

let A be set ;
func Normal_forms_on A -> Subset of (Fin (DISJOINT_PAIRS A)) equals :: NORMFORM:def 9
{ B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } ;
coherence
{ B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } is Subset of (Fin (DISJOINT_PAIRS A))

proof end;

end;

:: deftheorem defines Normal_forms_on NORMFORM:def 9 :
for A being set holds Normal_forms_on A = { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } ;

registration

let A be set ;
cluster Normal_forms_on A -> non empty ;
coherence
not Normal_forms_on A is empty by Lm4;

end;

theorem :: NORMFORM:51

for A being set holds {} in Normal_forms_on A by Lm4;

theorem Th52: :: NORMFORM:52

for A being set
for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds
a = b

proof end;

theorem Th53: :: NORMFORM:53

for A being set
for B being Element of Fin (DISJOINT_PAIRS A) st ( for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b ) holds
B in Normal_forms_on A ;

definition

let A be set ;
let B be Element of Fin (DISJOINT_PAIRS A);
func mi B -> Element of Normal_forms_on A equals :: NORMFORM:def 10
{ t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } ;
coherence
{ t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } is Element of Normal_forms_on A

proof end;

correctness
;
let C be Element of Fin (DISJOINT_PAIRS A);
func B ^ C -> Element of Fin (DISJOINT_PAIRS A) equals :: NORMFORM:def 11
(DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;
coherence
(DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is Element of Fin (DISJOINT_PAIRS A)

proof end;

correctness
;

end;

:: deftheorem defines mi NORMFORM:def 10 :
for A being set
for B being Element of Fin (DISJOINT_PAIRS A) holds mi B = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } ;

:: deftheorem defines ^ NORMFORM:def 11 :
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;

theorem :: NORMFORM:54

canceled;

theorem Th55: :: NORMFORM:55

for A being set
for x being Element of [:(Fin A),(Fin A):]
for B, C being Element of Fin (DISJOINT_PAIRS A) st x in B ^ C holds
ex b, c being Element of DISJOINT_PAIRS A st
( b in B & c in C & x = b \/ c )

proof end;

theorem Th56: :: NORMFORM:56

for A being set
for b, c being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds
b \/ c in B ^ C

proof end;

theorem :: NORMFORM:57

canceled;

theorem Th58: :: NORMFORM:58

for A being set
for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds
( a in B & ( b in B & b c= a implies b = a ) )

proof end;

theorem :: NORMFORM:59

for A being set
for a being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds
a in B by Th58;

theorem :: NORMFORM:60

for A being set
for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B & b in B & b c= a holds
b = a by Th58;

theorem Th61: :: NORMFORM:61

for A being set
for a being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds
b = a ) holds
a in mi B

proof end;

definition

let A be non empty set ;
let B be non empty Subset of A;
let O be BinOp of B;
let a, b be Element of B;
:: original: .
redefine func O . (a,b) -> Element of B;
coherence
O . (a,b) is Element of B

proof end;

end;

Lm5: for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) st ( for a being Element of DISJOINT_PAIRS A st a in B holds
a in C ) holds
B c= C

proof end;

theorem :: NORMFORM:62

canceled;

theorem :: NORMFORM:63

canceled;

theorem Th64: :: NORMFORM:64

for A being set
for B being Element of Fin (DISJOINT_PAIRS A) holds mi B c= B

proof end;

theorem Th65: :: NORMFORM:65

for A being set
for b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st b in B holds
ex c being Element of DISJOINT_PAIRS A st
( c c= b & c in mi B )

proof end;

theorem Th66: :: NORMFORM:66

for A being set
for K being Element of Normal_forms_on A holds mi K = K

proof end;

theorem Th67: :: NORMFORM:67

for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B \/ C) c= (mi B) \/ C

proof end;

theorem Th68: :: NORMFORM:68

for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) \/ C) = mi (B \/ C)

proof end;

theorem :: NORMFORM:69

for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B \/ (mi C)) = mi (B \/ C) by Th68;

theorem Th70: :: NORMFORM:70

for A being set
for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds
B ^ D c= C ^ D

proof end;

Lm6: for A being set
for a being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex b being Element of DISJOINT_PAIRS A st
( b c= a & b in (mi B) ^ C )

proof end;

theorem Th71: :: NORMFORM:71

for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ C) c= (mi B) ^ C

proof end;

theorem Th72: :: NORMFORM:72

for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = C ^ B

proof end;

theorem Th73: :: NORMFORM:73

for A being set
for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds
D ^ B c= D ^ C

proof end;

theorem Th74: :: NORMFORM:74

for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) ^ C) = mi (B ^ C)

proof end;

theorem Th75: :: NORMFORM:75

for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ (mi C)) = mi (B ^ C)

proof end;

theorem Th76: :: NORMFORM:76

for A being set
for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) = (K ^ L) ^ M

proof end;

theorem Th77: :: NORMFORM:77

for A being set
for K, L, M being Element of Normal_forms_on A holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)

proof end;

Lm7: for A being set
for a being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex c being Element of DISJOINT_PAIRS A st
( c in C & c c= a )

proof end;

Lm8: for A being set
for K, L being Element of Normal_forms_on A holds mi ((K ^ L) \/ L) = mi L

proof end;

theorem Th78: :: NORMFORM:78

for A being set
for B being Element of Fin (DISJOINT_PAIRS A) holds B c= B ^ B

proof end;

theorem Th79: :: NORMFORM:79

for A being set
for K being Element of Normal_forms_on A holds mi (K ^ K) = mi K

proof end;

definition

let A be set ;
canceled;
canceled;
func NormForm A -> strict LattStr means :Def14: :: NORMFORM:def 14
( the carrier of it = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of it . (B,C) = mi (B \/ C) & the L_meet of it . (B,C) = mi (B ^ C) ) ) );
existence
ex b₁ being strict LattStr st
( the carrier of b₁ = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b₁ . (B,C) = mi (B \/ C) & the L_meet of b₁ . (B,C) = mi (B ^ C) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict LattStr st the carrier of b₁ = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b₁ . (B,C) = mi (B \/ C) & the L_meet of b₁ . (B,C) = mi (B ^ C) ) ) & the carrier of b₂ = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b₂ . (B,C) = mi (B \/ C) & the L_meet of b₂ . (B,C) = mi (B ^ C) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem NORMFORM:def 12 :
canceled;

:: deftheorem NORMFORM:def 13 :
canceled;

:: deftheorem Def14 defines NormForm NORMFORM:def 14 :
for A being set
for b₂ being strict LattStr holds
( b₂ = NormForm A iff ( the carrier of b₂ = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b₂ . (B,C) = mi (B \/ C) & the L_meet of b₂ . (B,C) = mi (B ^ C) ) ) ) );

registration

let A be set ;
cluster NormForm A -> non empty strict ;
coherence
not NormForm A is empty

proof end;

end;

Lm9: for A being set
for a, b being Element of (NormForm A) holds a "\/" b = b "\/" a

proof end;

Lm10: for A being set
for a, b, c being Element of (NormForm A) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof end;

Lm11: for A being set
for K, L being Element of Normal_forms_on A holds the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = L

proof end;

Lm12: for A being set
for a, b being Element of (NormForm A) holds (a "/\" b) "\/" b = b

proof end;

Lm13: for A being set
for a, b being Element of (NormForm A) holds a "/\" b = b "/\" a

proof end;

Lm14: for A being set
for a, b, c being Element of (NormForm A) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof end;

Lm15: for A being set
for K, L, M being Element of Normal_forms_on A holds the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M)))

proof end;

Lm16: for A being set
for a, b being Element of (NormForm A) holds a "/\" (a "\/" b) = a

proof end;

registration

let A be set ;
cluster NormForm A -> strict Lattice-like ;
coherence
NormForm A is Lattice-like

proof end;

end;

registration

let A be set ;
cluster NormForm A -> strict distributive lower-bounded ;
coherence
( NormForm A is distributive & NormForm A is lower-bounded )

proof end;

end;

theorem :: NORMFORM:80

canceled;

theorem :: NORMFORM:81

canceled;

theorem :: NORMFORM:82

canceled;

theorem :: NORMFORM:83

canceled;

theorem :: NORMFORM:84

canceled;

theorem :: NORMFORM:85

for A being set holds {} is Element of (NormForm A)

proof end;

theorem :: NORMFORM:86

for A being set holds Bottom (NormForm A) = {}

proof end;