:: Algebra of Normal Forms :: by Andrzej Trybulec :: :: Received October 5, 1990 :: Copyright (c) 1990-2021 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 XBOOLE_0, FINSUB_1, SUBSET_1, ZFMISC_1, TARSKI, MCART_1, BINOP_1, FUNCT_1, SETWISEO, RELAT_1, FINSET_1, ORDINAL4, STRUCT_0, LATTICES, EQREL_1, NORMFORM; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1, FUNCT_2, FINSET_1, BINOP_1, DOMAIN_1, FINSUB_1, SETWISEO, STRUCT_0, LATTICES; constructors PARTFUN1, BINOP_1, DOMAIN_1, FINSET_1, SETWISEO, LATTICES, RELSET_1, XTUPLE_0; registrations SUBSET_1, FINSUB_1, LATTICES, RELAT_1, XTUPLE_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:]; theorem :: NORMFORM:1 a c= b & b c= a implies a = b; theorem :: NORMFORM:2 a c= b & b c= c implies a c= c; theorem :: NORMFORM:3 (a \/ b) \/ c = a \/ (b \/ c); theorem :: NORMFORM:4 (a /\ b) /\ c = a /\ (b /\ c); theorem :: NORMFORM:5 a /\ (b \/ c) = a /\ b \/ a /\ c; theorem :: NORMFORM:6 a \/ (b /\ a) = a; theorem :: NORMFORM:7 a /\ (b \/ a) = a; theorem :: NORMFORM:8 a \/ (b /\ c) = (a \/ b) /\ (a \/ c); theorem :: NORMFORM:9 a c= c & b c= c implies a \/ b c= c; theorem :: NORMFORM:10 a c= a \/ b & b c= a \/ b; theorem :: NORMFORM:11 a = a \/ b implies b c= a; theorem :: NORMFORM:12 a c= b implies c \/ a c= c \/ b & a \/ c c= b \/ c; theorem :: NORMFORM:13 a\b \/ b = a \/ b; theorem :: NORMFORM:14 a \ b c= c implies a c= b \/ c; theorem :: NORMFORM:15 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; registration let A be set; cluster FinPairUnion A -> commutative idempotent associative; end; theorem :: NORMFORM:16 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:17 [{}.A, {}.A] is_a_unity_wrt FinPairUnion A; theorem :: NORMFORM:18 FinPairUnion A is having_a_unity; theorem :: NORMFORM:19 the_unity_wrt FinPairUnion A = [{}.A, {}.A]; theorem :: NORMFORM:20 for x being Element of [:Fin A, Fin A:] holds the_unity_wrt FinPairUnion A c= x; theorem :: NORMFORM:21 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:22 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; registration let X; cluster DISJOINT_PAIRS(X) -> non empty; end; theorem :: NORMFORM:23 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:24 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:25 a`1 misses a`2; theorem :: NORMFORM:26 x c= b implies x is Element of DISJOINT_PAIRS X; theorem :: NORMFORM:27 not (ex x being set st x in a`1 & x in a`2); theorem :: NORMFORM:28 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; theorem :: NORMFORM:29 x`1 misses x`2 implies x is Element of DISJOINT_PAIRS X; theorem :: NORMFORM:30 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; registration let A; cluster Normal_forms_on A -> non empty; end; reserve K,L,M for Element of Normal_forms_on A; theorem :: NORMFORM:31 {} in Normal_forms_on A; theorem :: NORMFORM:32 B in Normal_forms_on A & a in B & b in B & a c= b implies a = b; theorem :: NORMFORM:33 (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; theorem :: NORMFORM:34 x in B^C implies ex b,c st b in B & c in C & x = b \/ c; theorem :: NORMFORM:35 b in B & c in C & b \/ c in DISJOINT_PAIRS A implies b \/ c in B ^C; theorem :: NORMFORM:36 a in mi B implies a in B & (b in B & b c= a implies b = a); theorem :: NORMFORM:37 a in mi B implies a in B; theorem :: NORMFORM:38 a in mi B & b in B & b c= a implies b = a; theorem :: NORMFORM:39 a in B & (for b st b in B & b c= a holds b = a) implies a in mi B; theorem :: NORMFORM:40 mi B c= B; theorem :: NORMFORM:41 b in B implies ex c st c c= b & c in mi B; theorem :: NORMFORM:42 mi K = K; theorem :: NORMFORM:43 mi (B \/ C) c= mi B \/ C; theorem :: NORMFORM:44 mi(mi B \/ C) = mi (B \/ C); theorem :: NORMFORM:45 mi(B \/ mi C) = mi (B \/ C); theorem :: NORMFORM:46 B c= C implies B ^ D c= C ^ D; theorem :: NORMFORM:47 mi(B ^ C) c= mi B ^ C; theorem :: NORMFORM:48 B^C = C^B; theorem :: NORMFORM:49 B c= C implies D ^ B c= D ^ C; theorem :: NORMFORM:50 mi(mi B ^ C) = mi (B ^ C); theorem :: NORMFORM:51 mi(B ^ mi C) = mi (B ^ C); theorem :: NORMFORM:52 K^(L^M) = K^L^M; theorem :: NORMFORM:53 K^(L \/ M) = K^L \/ K^M; theorem :: NORMFORM:54 B c= B ^ B; theorem :: NORMFORM:55 mi(K ^ K) = mi K; definition let A; func NormForm A -> strict LattStr means :: NORMFORM:def 12 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; registration let A; cluster NormForm A -> non empty; end; reserve K, L, M for Element of Normal_forms_on A; registration let A; cluster NormForm A -> Lattice-like; end; registration let A; cluster NormForm A -> distributive lower-bounded; end; theorem :: NORMFORM:56 {} is Element of NormForm A; theorem :: NORMFORM:57 Bottom NormForm A = {};