Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Algebra of Normal Forms

**by****Andrzej Trybulec**- Received October 5, 1990
- 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 = {};

Back to top