Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Algebra of Normal Forms

by
Andrzej Trybulec

MML identifier: NORMFORM
[ Mizar article, MML identifier index ]

```environ

vocabulary BOOLE, FINSUB_1, MCART_1, BINOP_1, FUNCT_1, SETWISEO, RELAT_1,
FINSET_1, FINSEQ_1, LATTICES, NORMFORM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_2,
FINSET_1, BINOP_1, DOMAIN_1, FINSUB_1, SETWISEO, STRUCT_0, LATTICES;
constructors FINSET_1, BINOP_1, DOMAIN_1, SETWISEO, LATTICES, PARTFUN1,
MEMBERED, XBOOLE_0;
clusters FINSUB_1, LATTICES, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

:: A u x i l i a r y   t h e o r e m s

:: Part 1. BOOLEan operations on pairs & relations between pairs

reserve A, B for non empty preBoolean set,
x, y for Element of [:A,B:];

definition let A,B,x,y;
pred x c= y means
:: NORMFORM:def 1
x`1 c= y`1 & x`2 c= y`2;
reflexivity;
func x \/ y -> Element of [:A, B:] equals
:: NORMFORM:def 2
[x`1 \/ y`1, x`2 \/ y`2];
commutativity;
idempotence;
func x /\ y -> Element of [:A, B:] equals
:: NORMFORM:def 3
[x`1 /\ y`1, x`2 /\ y`2];
commutativity;
idempotence;
func x \ y -> Element of [:A, B:] equals
:: NORMFORM:def 4
[x`1 \ y`1, x`2 \ y`2];
func x \+\ y -> Element of [:A, B:] equals
:: NORMFORM:def 5
[x`1 \+\ y`1, x`2 \+\ y`2];
commutativity;
end;

reserve X for set,
a,b,c for Element of [:A,B:];

canceled 3;

theorem :: NORMFORM:4
a c= b & b c= a implies a = b;

theorem :: NORMFORM:5
a c= b & b c= c implies a c= c;

canceled 4;

theorem :: NORMFORM:10
(a \/ b)`1 = a`1 \/ b`1 & (a \/ b)`2 = a`2 \/ b`2;

theorem :: NORMFORM:11
(a /\ b)`1 = a`1 /\ b`1 & (a /\ b)`2 = a`2 /\ b`2;

theorem :: NORMFORM:12
(a \ b)`1 = a`1 \ b`1 & (a \ b)`2 = a`2 \ b`2;

theorem :: NORMFORM:13
(a \+\ b)`1 = a`1 \+\ b`1 & (a \+\ b)`2 = a`2 \+\ b`2;

canceled 2;

theorem :: NORMFORM:16
(a \/ b) \/ c = a \/ (b \/ c);

canceled 2;

theorem :: NORMFORM:19
(a /\ b) /\ c = a /\ (b /\ c);

theorem :: NORMFORM:20
a /\ (b \/ c) = a /\ b \/ a /\ c;

theorem :: NORMFORM:21
a \/ (b /\ a) = a;

theorem :: NORMFORM:22
a /\ (b \/ a) = a;

canceled;

theorem :: NORMFORM:24
a \/ (b /\ c) = (a \/ b) /\ (a \/ c);

theorem :: NORMFORM:25
a c= c & b c= c implies a \/ b c= c;

theorem :: NORMFORM:26
a c= a \/ b & b c= a \/ b;

theorem :: NORMFORM:27
a = a \/ b implies b c= a;

theorem :: NORMFORM:28
a c= b implies c \/ a c= c \/ b & a \/ c c= b \/ c;

theorem :: NORMFORM:29
a\b \/ b = a \/ b;

theorem :: NORMFORM:30
a \ b c= c implies a c= b \/ c;

theorem :: NORMFORM:31
a c= b \/ c implies a \ c c= b;

reserve a for Element of [:Fin X, Fin X:];

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

reserve A for set;

definition let X be non empty set, 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);
end;

definition let A be set;
cluster FinPairUnion A -> commutative idempotent associative;
end;

canceled 3;

theorem :: NORMFORM:35
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);

theorem :: NORMFORM:36
[{}.A, {}.A] is_a_unity_wrt FinPairUnion A;

theorem :: NORMFORM:37
FinPairUnion A has_a_unity;

theorem :: NORMFORM:38
the_unity_wrt FinPairUnion A = [{}.A, {}.A];

theorem :: NORMFORM:39
for x being Element of [:Fin A, Fin A:] holds
the_unity_wrt FinPairUnion A c= x;

theorem :: NORMFORM:40
for X being non empty set
for f being (Function of X,[:Fin A,Fin A:]), 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;

theorem :: NORMFORM:41
for X being non empty set, 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);

:: Part 2. Disjoint pairs of finite sets

definition let X;
func DISJOINT_PAIRS(X) -> Subset of [:Fin X, Fin X:] equals
:: NORMFORM:def 8
{ a : a`1 misses a`2 };
end;

definition let X;
cluster DISJOINT_PAIRS(X) -> non empty;
end;

theorem :: NORMFORM:42
for y being Element of [:Fin X, Fin X:]
holds y in DISJOINT_PAIRS X iff y`1 misses y`2;

reserve x,y for Element of [:Fin X, Fin X:],
a,b for Element of DISJOINT_PAIRS X;

theorem :: NORMFORM:43
y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X implies
(y \/ x in DISJOINT_PAIRS X iff y`1 /\ x`2 \/ x`1 /\ y`2 = {});

theorem :: NORMFORM:44
a`1 misses a`2;

theorem :: NORMFORM:45
x c= b implies x is Element of DISJOINT_PAIRS X;

theorem :: NORMFORM:46
not (ex x being set st x in a`1 & x in a`2);

theorem :: NORMFORM:47
not a \/ b in DISJOINT_PAIRS X implies
ex p being Element of X st
p in a`1 & p in b`2 or p in b`1 & p in a`2;

canceled;

theorem :: NORMFORM:49
x`1 misses x`2 implies x is Element of DISJOINT_PAIRS X;

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

reserve A for set,
x for Element of [:Fin A, Fin A:],
a,b,c,d,s,t for Element of DISJOINT_PAIRS A,
B,C,D for Element of Fin DISJOINT_PAIRS A;

definition let A;
func Normal_forms_on A -> Subset of Fin DISJOINT_PAIRS A equals
:: NORMFORM:def 9
{ B : a in B & b in B & a c= b implies a = b};
end;

definition let A;
cluster Normal_forms_on A -> non empty;
end;

reserve K,L,M for Element of Normal_forms_on A;

theorem :: NORMFORM:51
{} in Normal_forms_on A;

theorem :: NORMFORM:52
B in Normal_forms_on A & a in B & b in B & a c= b implies a = b;

theorem :: NORMFORM:53
(for a,b st a in B & b in B & a c= b holds a = b)
implies B in Normal_forms_on A;

definition let A,B;
func mi B -> Element of Normal_forms_on A equals
:: NORMFORM:def 10
{ t : s in B & s c= t iff s = t };
let C;
func B^C -> Element of Fin DISJOINT_PAIRS A equals
:: NORMFORM:def 11
DISJOINT_PAIRS A /\ { s \/ t: s in B & t in C };
end;

canceled;

theorem :: NORMFORM:55
x in B^C implies ex b,c st b in B & c in C & x = b \/ c;

theorem :: NORMFORM:56
b in B & c in C & b \/ c in DISJOINT_PAIRS A implies b \/ c in B^C;

canceled;

theorem :: NORMFORM:58
a in mi B implies a in B & (b in B & b c= a implies b = a);

theorem :: NORMFORM:59
a in mi B implies a in B;

theorem :: NORMFORM:60
a in mi B & b in B & b c= a implies b = a;

theorem :: NORMFORM:61
a in B & (for b st b in B & b c= a holds b = a) implies a in mi B;

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;
redefine func O.(a,b) -> Element of B;
end;

canceled 2;

theorem :: NORMFORM:64
mi B c= B;

theorem :: NORMFORM:65
b in B implies ex c st c c= b & c in mi B;

theorem :: NORMFORM:66
mi K = K;

theorem :: NORMFORM:67
mi (B \/ C) c= mi B \/ C;

theorem :: NORMFORM:68
mi(mi B \/ C) = mi (B \/ C);

theorem :: NORMFORM:69
mi(B \/ mi C) = mi (B \/ C);

theorem :: NORMFORM:70
B c= C implies B ^ D c= C ^ D;

theorem :: NORMFORM:71
mi(B ^ C) c= mi B ^ C;

theorem :: NORMFORM:72
B^C = C^B;

theorem :: NORMFORM:73
B c= C implies D ^ B c= D ^ C;

theorem :: NORMFORM:74
mi(mi B ^ C) = mi (B ^ C);

theorem :: NORMFORM:75
mi(B ^ mi C) = mi (B ^ C);

theorem :: NORMFORM:76
K^(L^M) = K^L^M;

theorem :: NORMFORM:77
K^(L \/ M) = K^L \/ K^M;

theorem :: NORMFORM:78
B c= B ^ B;

theorem :: NORMFORM:79
mi(K ^ K) = mi K;

definition let A;
canceled 2;

func NormForm A -> strict LattStr means
:: 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);
end;

definition let A;
cluster NormForm A -> non empty;
end;

reserve K, L, M for Element of Normal_forms_on A;

definition let A;
cluster NormForm A -> Lattice-like;
end;

definition let A;
cluster NormForm A -> distributive lower-bounded;
end;

canceled 5;

theorem :: NORMFORM:85
{} is Element of NormForm A;

theorem :: NORMFORM:86
Bottom NormForm A = {};

```