:: Algebra of Normal Forms :: by Andrzej Trybulec :: :: Received October 5, 1990 :: Copyright (c) 1990-2018 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; definitions TARSKI, BINOP_1, LATTICES, XBOOLE_0; equalities LATTICES, XBOOLE_0; expansions TARSKI, BINOP_1, XBOOLE_0; theorems BINOP_1, FINSUB_1, DOMAIN_1, MCART_1, ZFMISC_1, SETWISEO, LATTICE2, TARSKI, FINSET_1, LATTICES, XBOOLE_0, XBOOLE_1, RELAT_1; schemes BINOP_1, SETWISEO, FRAENKEL; 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 x`1 c= y`1 & x`2 c= y`2; reflexivity; func x \/ y -> Element of [:A, B:] equals [x`1 \/ y`1, x`2 \/ y`2]; correctness; commutativity; idempotence by MCART_1:21; func x /\ y -> Element of [:A, B:] equals [x`1 /\ y`1, x`2 /\ y`2]; correctness; commutativity; idempotence by MCART_1:21; func x \ y -> Element of [:A, B:] equals [x`1 \ y`1, x`2 \ y`2]; correctness; func x \+\ y -> Element of [:A, B:] equals [x`1 \+\ y`1, x`2 \+\ y`2]; correctness; commutativity; end; reserve X for set, a,b,c for Element of [:A,B:]; theorem Th1: a c= b & b c= a implies a = b proof assume a`1 c= b`1 & a`2 c= b`2 & b`1 c= a`1 & b`2 c= a`2; then a`1 = b`1 & a`2 = b`2; hence thesis by DOMAIN_1:2; end; theorem Th2: a c= b & b c= c implies a c= c proof assume a`1 c= b`1 & a`2 c= b`2 & b`1 c= c`1 & b`2 c= c`2; hence a`1 c= c`1 & a`2 c= c`2; end; theorem Th3: (a \/ b) \/ c = a \/ (b \/ c) proof A1: ((a \/ b) \/ c)`2 = (a \/ b)`2 \/ c`2 .= a`2 \/ b`2 \/ c`2 .= a`2 \/ (b`2 \/ c`2) by XBOOLE_1:4 .= a`2 \/ (b \/ c)`2 .= (a \/ (b \/ c))`2; ((a \/ b) \/ c)`1 = (a \/ b)`1 \/ c`1 .= a`1 \/ b`1 \/ c`1 .= a`1 \/ (b`1 \/ c`1) by XBOOLE_1:4 .= a`1 \/ (b \/ c)`1 .= (a \/ (b \/ c))`1; hence thesis by A1,DOMAIN_1:2; end; theorem (a /\ b) /\ c = a /\ (b /\ c) proof A1: ((a /\ b) /\ c)`2 = (a /\ b)`2 /\ c`2 .= a`2 /\ b`2 /\ c`2 .= a`2 /\ (b`2 /\ c`2) by XBOOLE_1:16 .= a`2 /\ (b /\ c)`2 .= (a /\ (b /\ c))`2; ((a /\ b) /\ c)`1 = (a /\ b)`1 /\ c`1 .= a`1 /\ b`1 /\ c`1 .= a`1 /\ (b`1 /\ c`1) by XBOOLE_1:16 .= a`1 /\ (b /\ c)`1 .= (a /\ (b /\ c))`1; hence thesis by A1,DOMAIN_1:2; end; theorem Th5: a /\ (b \/ c) = a /\ b \/ a /\ c proof A1: (a /\ (b \/ c))`2 = a`2 /\ (b \/ c)`2 .= a`2 /\ (b`2 \/ c`2) .= a`2 /\ b`2 \/ a`2 /\ c`2 by XBOOLE_1:23 .= a`2 /\ b`2 \/ (a /\ c)`2 .= (a /\ b)`2 \/ (a /\ c)`2 .= (a /\ b \/ a /\ c)`2; (a /\ (b \/ c))`1 = a`1 /\ (b \/ c)`1 .= a`1 /\ (b`1 \/ c`1) .= a`1 /\ b`1 \/ a`1 /\ c`1 by XBOOLE_1:23 .= a`1 /\ b`1 \/ (a /\ c)`1 .= (a /\ b)`1 \/ (a /\ c)`1 .= (a /\ b \/ a /\ c)`1; hence thesis by A1,DOMAIN_1:2; end; theorem Th6: a \/ (b /\ a) = a proof A1: (a \/ (b /\ a))`2 = a`2 \/ (b /\ a)`2 .= a`2 \/ b`2 /\ a`2 .= a`2 by XBOOLE_1:22; (a \/ (b /\ a))`1 = a`1 \/ (b /\ a)`1 .= a`1 \/ b`1 /\ a`1 .= a`1 by XBOOLE_1:22; hence thesis by A1,DOMAIN_1:2; end; theorem Th7: a /\ (b \/ a) = a proof thus a /\ (b \/ a) = a /\ b \/ a /\ a by Th5 .= a by Th6; end; theorem a \/ (b /\ c) = (a \/ b) /\ (a \/ c) proof thus a \/ (b /\ c) = a \/ c /\ a \/ c /\ b by Th6 .= a \/ (c /\ a \/ c /\ b) by Th3 .= a \/ c /\ (a \/ b) by Th5 .= (a \/ b) /\ a \/ (a \/ b) /\ c by Th7 .= (a \/ b) /\ (a \/ c) by Th5; end; theorem Th9: a c= c & b c= c implies a \/ b c= c by XBOOLE_1:8; theorem Th10: a c= a \/ b & b c= a \/ b by XBOOLE_1:7; theorem a = a \/ b implies b c= a by Th10; theorem Th12: a c= b implies c \/ a c= c \/ b & a \/ c c= b \/ c by XBOOLE_1:9; theorem a\b \/ b = a \/ b proof a`1 \ b`1 \/ b`1 = a`1 \/ b`1 & a`2 \ b`2 \/ b`2 = a`2 \/ b`2 by XBOOLE_1:39; hence thesis; end; theorem a \ b c= c implies a c= b \/ c by XBOOLE_1:44; theorem a c= b \/ c implies a \ c c= b by XBOOLE_1:43; reserve a for Element of [:Fin X, Fin X:]; definition let A be set; func FinPairUnion A -> BinOp of [:Fin A, Fin A:] means :Def6: for x,y being Element of [:Fin A, Fin A:] holds it.(x,y) = x \/ y; existence proof deffunc O(Element of [:Fin A, Fin A:],Element of [:Fin A, Fin A:]) = \$1 \/ \$2; ex IT being BinOp of [:Fin A, Fin A:] st for x,y being Element of [: Fin A, Fin A:] holds IT.(x,y) = O(x,y) from BINOP_1:sch 4; hence thesis; end; uniqueness proof let IT, IT9 be BinOp of [:Fin A, Fin A:] such that A1: for x,y being Element of [:Fin A, Fin A:] holds IT.(x,y) = x \/ y and A2: for x,y being Element of [:Fin A, Fin A:] holds IT9.(x,y) = x \/ y; now let x,y be Element of [:Fin A, Fin A:]; thus IT.(x,y) = x \/ y by A1 .= IT9.(x,y) by A2; end; hence IT = IT9; end; 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 FinPairUnion A \$\$(B,f); correctness; end; Lm1: FinPairUnion A is idempotent proof let a be Element of [:Fin A, Fin A:]; thus FinPairUnion A.(a, a) = a \/ a by Def6 .= a; end; Lm2: FinPairUnion A is commutative proof let a,b be Element of [:Fin A, Fin A:]; thus FinPairUnion A.(a,b) = b \/ a by Def6 .= FinPairUnion A.(b,a) by Def6; end; Lm3: FinPairUnion A is associative proof let a,b,c be Element of [:Fin A, Fin A:]; thus FinPairUnion A.(a, FinPairUnion A.(b,c)) = a \/ FinPairUnion A.(b,c) by Def6 .= a \/ (b \/ c) by Def6 .= a \/ b \/ c by Th3 .= FinPairUnion A.(a,b) \/ c by Def6 .= FinPairUnion A.(FinPairUnion A.(a,b), c) by Def6; end; registration let A be set; cluster FinPairUnion A -> commutative idempotent associative; coherence by Lm1,Lm2,Lm3; end; theorem 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 let X be non empty set, f be Function of X, [:Fin A,Fin A:]; let B be (Element of Fin X), x be Element of X; assume A1: x in B; then FinPairUnion A \$\$(B, f) = FinPairUnion A \$\$(B \/ {.x.}, f) by ZFMISC_1:40 .= FinPairUnion A.(FinPairUnion A \$\$(B,f),f.x) by A1,SETWISEO:20 .= FinPairUnion A \$\$(B,f) \/ f.x by Def6; hence thesis by Th10; end; theorem Th17: [{}.A, {}.A] is_a_unity_wrt FinPairUnion A proof now let x be Element of [:Fin A, Fin A:]; thus FinPairUnion A.([{}.A, {}.A], x) = [{}.A, {}.A] \/ x by Def6 .= x by MCART_1:21; end; hence thesis by BINOP_1:4; end; theorem Th18: FinPairUnion A is having_a_unity proof [{}.A, {}.A] is_a_unity_wrt FinPairUnion A by Th17; hence thesis by SETWISEO:def 2; end; theorem Th19: the_unity_wrt FinPairUnion A = [{}.A, {}.A] proof [{}.A, {}.A] is_a_unity_wrt FinPairUnion A by Th17; hence thesis by BINOP_1:def 8; end; theorem Th20: for x being Element of [:Fin A, Fin A:] holds the_unity_wrt FinPairUnion A c= x proof let x be Element of [:Fin A, Fin A:]; [{}.A, {}.A] is_a_unity_wrt FinPairUnion A by Th17; then the_unity_wrt FinPairUnion A = [{}, {}] by BINOP_1:def 8; then (the_unity_wrt FinPairUnion A)`1 = {} & (the_unity_wrt FinPairUnion A)`2 = {}; hence (the_unity_wrt FinPairUnion A)`1 c= x`1 & (the_unity_wrt FinPairUnion A )`2 c= x`2; end; theorem 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 proof let X be non empty set, f be Function of X,[:Fin A,Fin A:]; let B be (Element of Fin X), c be Element of [:Fin A, Fin A:]; defpred P[Element of Fin X] means \$1 c= B implies FinPairUnion A \$\$(\$1,f) c= c; assume A1: for x being Element of X st x in B holds f.x c= c; A2: now let C be (Element of Fin X), b be Element of X; assume A3: P[C]; now assume A4: C \/ {b} c= B; then {b} c= B by XBOOLE_1:11; then b in B by ZFMISC_1:31; then A5: f.b c= c by A1; FinPairUnion A \$\$(C \/ {.b.},f) = FinPairUnion A.(FinPairUnion A \$\$ (C,f),f.b) by Th18,SETWISEO:32 .= FinPairUnion A \$\$(C,f) \/ f.b by Def6; hence FinPairUnion A \$\$(C \/ {.b.},f) c= c by A3,A4,A5,Th9,XBOOLE_1:11; end; hence P[C \/ {.b.}]; end; A6: P[{}.X] proof assume {}.X c= B; FinPairUnion A \$\$({}.X,f) = the_unity_wrt FinPairUnion A by Th18, SETWISEO:31; hence thesis by Th20; end; for C being Element of Fin X holds P[C] from SETWISEO:sch 4(A6,A2); hence thesis; end; theorem 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) proof let X be non empty set, B be Element of Fin X; let f,g be Function of X,[:Fin A,Fin A:]; set J = FinPairUnion A; A1: [{}.A, {}.A] = the_unity_wrt J by Th19; assume A2: f|B = g|B; now per cases; suppose A3: B = {}; hence FinPairUnion(B,f) = J\$\$({}.X,f) .= [{}.A, {}.A] by A1,Th18,SETWISEO:31 .= J\$\$({}.X,g) by A1,Th18,SETWISEO:31 .= FinPairUnion(B,g) by A3; end; suppose A4: B <> {}; f.:B = g.:B by A2,RELAT_1:166; hence thesis by A4,SETWISEO:26; end; end; hence thesis; end; :: Part 2. Disjoint pairs of finite sets definition let X; func DISJOINT_PAIRS(X) -> Subset of [:Fin X, Fin X:] equals { a : a`1 misses a`2 }; coherence proof set D = { a : a`1 misses a`2 }; D c= [:Fin X, Fin X:] proof let x be object; assume x in D; then ex a st x = a & a`1 misses a`2; hence thesis; end; hence thesis; end; end; registration let X; cluster DISJOINT_PAIRS(X) -> non empty; coherence proof {} is Element of Fin X by FINSUB_1:7; then reconsider b = [{},{}] as Element of [:Fin X, Fin X:] by ZFMISC_1:def 2; b`1 misses b`2; then b in { a : a`1 misses a`2 }; hence thesis; end; end; theorem Th23: for y being Element of [:Fin X, Fin X:] holds y in DISJOINT_PAIRS X iff y`1 misses y`2 proof let y be Element of [:Fin X, Fin X:]; y in DISJOINT_PAIRS X iff ex a st y = a & a`1 misses a`2; hence thesis; end; reserve x,y for Element of [:Fin X, Fin X:], a,b for Element of DISJOINT_PAIRS X; theorem 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 = {}) proof assume that A1: y in DISJOINT_PAIRS X and A2: x in DISJOINT_PAIRS X; A3: (y`1 \/ x`1) /\ (y`2 \/ x`2) = (y`1 \/ x`1) /\ y`2 \/ (y`1 \/ x`1) /\ x `2 & (y`1 \/ x`1) /\ y`2 = y`1 /\ y`2 \/ x`1 /\ y`2 by XBOOLE_1:23; x`1 misses x`2 by A2,Th23; then A4: x`1 /\ x`2 = {}; y`1 misses y`2 by A1,Th23; then A5: y`1 /\ y`2 = {}; A6: (y`1 \/ x`1) /\ x`2 = y`1 /\ x`2 \/ x`1 /\ x`2 by XBOOLE_1:23; A7: (y \/ x)`1 = y`1 \/ x`1 & (y \/ x)`2 = y`2 \/ x`2; thus y \/ x in DISJOINT_PAIRS X implies y`1 /\ x`2 \/ x`1 /\y`2 = {} by A5,A4,A7,A3,A6,XBOOLE_0:def 7,Th23; assume y`1 /\ x`2 \/ x`1 /\ y`2 = {}; then (y \/ x)`1 misses (y \/ x)`2 by A5,A4,A3,A6; hence thesis; end; theorem a`1 misses a`2 by Th23; theorem Th26: x c= b implies x is Element of DISJOINT_PAIRS X proof assume A1: x`1 c= b`1 & x`2 c= b`2; b`1 misses b`2 by Th23; then x`1 misses x`2 by A1,XBOOLE_1:64; hence thesis by Th23; end; theorem Th27: not (ex x being set st x in a`1 & x in a`2) by Th23,XBOOLE_0:3; theorem 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 proof set p = the Element of (a \/ b)`1 /\ (a \/ b)`2; assume not a \/ b in DISJOINT_PAIRS X; then (a \/ b)`1 meets (a \/ b)`2; then A1: (a \/ b)`1 /\ (a \/ b)`2 <> {}; (a \/ b)`1 /\ (a \/ b)`2 is Subset of X by FINSUB_1:16; then reconsider p as Element of X by A1,TARSKI:def 3; p in (a \/ b)`2 by A1,XBOOLE_0:def 4; then p in a`2 \/ b`2; then A2: p in b`2 or p in a`2 by XBOOLE_0:def 3; take p; p in (a \/ b)`1 by A1,XBOOLE_0:def 4; then p in a`1 \/ b`1; then p in a`1 or p in b`1 by XBOOLE_0:def 3; hence thesis by A2,Th27; end; theorem x`1 misses x`2 implies x is Element of DISJOINT_PAIRS X by Th23; theorem for V,W being set st V c= a`1 & W c= a`2 holds [V,W] is Element of DISJOINT_PAIRS X proof let V,W be set; assume A1: V c= a`1 & W c= a`2; then V is Element of Fin X & W is Element of Fin X by SETWISEO:11; then reconsider x = [V,W] as Element of [:Fin X, Fin X:] by ZFMISC_1:def 2; a`1 misses a`2 & [V,W]`1 = V by Th23; then x`1 misses x`2 by A1,XBOOLE_1:64; hence thesis by Th23; end; 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; Lm4: for A holds {} in { B : a in B & b in B & a c= b implies a = b} proof let A; {} is Element of Fin DISJOINT_PAIRS A & for a,b holds a in {} & b in {} & a c= b implies a = b by FINSUB_1:7; hence thesis; end; definition let A; func Normal_forms_on A -> Subset of Fin DISJOINT_PAIRS A equals { B : a in B & b in B & a c= b implies a = b}; coherence proof set IT = { B : a in B & b in B & a c= b implies a = b}; IT c= Fin DISJOINT_PAIRS A proof let x be object; assume x in IT; then ex B st x = B & for a,b holds a in B & b in B & a c= b implies a = b; hence thesis; end; hence thesis; end; end; registration let A; cluster Normal_forms_on A -> non empty; coherence by Lm4; end; reserve K,L,M for Element of Normal_forms_on A; theorem {} in Normal_forms_on A by Lm4; theorem Th32: B in Normal_forms_on A & a in B & b in B & a c= b implies a = b proof assume B in Normal_forms_on A; then ex C st B = C & for a,b holds a in C & b in C & a c= b implies a = b; hence thesis; end; theorem Th33: (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 { t : s in B & s c= t iff s = t }; coherence proof set M = { t : s in B & s c= t iff s = t }; now let x be object; assume x in M; then ex t st x = t & for s holds s in B & s c= t iff s = t; hence x in B; end; then A1: M c= B; then A2: M is finite by FINSET_1:1; B c= DISJOINT_PAIRS A by FINSUB_1:def 5; then M c= DISJOINT_PAIRS A by A1; then reconsider M9 = M as Element of Fin DISJOINT_PAIRS A by A2, FINSUB_1:def 5; now let c,d be Element of DISJOINT_PAIRS A; assume c in M; then ex t st c = t & for s holds s in B & s c= t iff s = t; then A3: c in B; assume d in M; then ex t st d = t & for s holds s in B & s c= t iff s = t; hence c c= d implies c = d by A3; end; then M9 is Element of Normal_forms_on A by Th33; hence thesis; end; correctness; let C; func B^C -> Element of Fin DISJOINT_PAIRS A equals DISJOINT_PAIRS A /\ { s \/ t: s in B & t in C }; coherence proof deffunc F(Element of DISJOINT_PAIRS A,Element of DISJOINT_PAIRS A) = \$1 \/ \$2; set M = DISJOINT_PAIRS A /\ { F(s,t): s in B & t in C }; A4: C is finite; A5: B is finite; { F(s, t) : s in B & t in C } is finite from FRAENKEL:sch 22(A5, A4 ); then M c= DISJOINT_PAIRS A & M is finite by FINSET_1:1,XBOOLE_1:17; hence thesis by FINSUB_1:def 5; end; correctness; end; theorem Th34: x in B^C implies ex b,c st b in B & c in C & x = b \/ c proof assume x in B^C; then x in { s \/ t: s in B & t in C } by XBOOLE_0:def 4; then ex s,t st x = s \/ t & s in B & t in C; hence thesis; end; theorem Th35: b in B & c in C & b \/ c in DISJOINT_PAIRS A implies b \/ c in B ^C proof assume b in B & c in C; then A1: b \/ c in { s \/ t: s in B & t in C }; assume b \/ c in DISJOINT_PAIRS A; hence thesis by A1,XBOOLE_0:def 4; end; theorem Th36: a in mi B implies a in B & (b in B & b c= a implies b = a) proof assume a in mi B; then ex t st a = t & for s holds s in B & s c= t iff s = t; hence thesis; end; theorem a in mi B implies a in B by Th36; theorem a in mi B & b in B & b c= a implies b = a by Th36; theorem Th39: a in B & (for b st b in B & b c= a holds b = a) implies a in mi B proof assume a in B & for s st s in B & s c= a holds s = a; then s in B & s c= a iff s = a; hence thesis; end; Lm5: (for a holds a in B implies a in C) implies B c= C proof assume A1: for a holds a in B implies a in C; let x be object; assume A2: x in B; then x is Element of DISJOINT_PAIRS A by SETWISEO:9; hence thesis by A1,A2; end; theorem Th40: mi B c= B proof for a holds a in mi B implies a in B by Th36; hence thesis by Lm5; end; theorem Th41: b in B implies ex c st c c= b & c in mi B proof assume A1: b in B; defpred P[Element of DISJOINT_PAIRS A,Element of DISJOINT_PAIRS A] means \$1 c= \$2; A2: for a holds P[a,a]; A3: for a,b,c st P[a,b] & P[b,c] holds P[a,c] by Th2; for a st a in B ex b st b in B & P[b,a] & for c st c in B & P[c,b] holds P[b,c] from FRAENKEL:sch 23(A2,A3); then consider c such that A4: c in B and A5: c c= b and A6: for a st a in B & a c= c holds c c= a by A1; take c; thus c c= b by A5; now let b; assume that A7: b in B and A8: b c= c; c c= b by A6,A7,A8; hence b = c by A8,Th1; end; hence thesis by A4,Th39; end; theorem Th42: mi K = K proof thus mi K c= K by Th40; now let a; assume A1: a in K; then for b st b in K & b c= a holds b = a by Th32; hence a in mi K by A1,Th39; end; hence thesis by Lm5; end; theorem Th43: mi (B \/ C) c= mi B \/ C proof now let a; assume A1: a in mi(B \/ C); then A2: a in B \/ C by Th36; now per cases by A2,XBOOLE_0:def 3; suppose A3: a in B; now let b; assume b in B; then b in B \/ C by XBOOLE_0:def 3; hence b c= a implies b = a by A1,Th36; end; then a in mi B by A3,Th39; hence a in mi B \/ C by XBOOLE_0:def 3; end; suppose a in C; hence a in mi B \/ C by XBOOLE_0:def 3; end; end; hence a in mi B \/ C; end; hence thesis by Lm5; end; theorem Th44: mi(mi B \/ C) = mi (B \/ C) proof A1: mi B \/ C c= B \/ C by Th40,XBOOLE_1:9; now let a; assume A2: a in mi(mi B \/ C); A3: now let b; assume that A4: b in B \/ C and A5: b c= a; now per cases by A4,XBOOLE_0:def 3; suppose b in B; then consider c such that A6: c c= b and A7: c in mi B by Th41; c in mi B \/ C & c c= a by A5,A6,A7,Th2,XBOOLE_0:def 3; then c = a by A2,Th36; hence b = a by A5,A6,Th1; end; suppose b in C; then b in mi B \/ C by XBOOLE_0:def 3; hence b = a by A2,A5,Th36; end; end; hence b = a; end; a in mi B \/ C by A2,Th36; hence a in mi (B \/ C) by A1,A3,Th39; end; hence mi(mi B \/ C) c= mi (B \/ C) by Lm5; A8: mi(B \/ C) c= mi B \/ C by Th43; now let a; assume A9: a in mi (B \/ C); then for b st b in mi B \/ C holds b c= a implies b = a by A1,Th36; hence a in mi(mi B \/ C) by A8,A9,Th39; end; hence thesis by Lm5; end; theorem mi(B \/ mi C) = mi (B \/ C) by Th44; theorem Th46: B c= C implies B ^ D c= C ^ D proof deffunc F(Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) = \$1 \/ \$2; defpred P[set,set] means \$1 in B & \$2 in D; defpred Q[set,set] means \$1 in C & \$2 in D; set X1 = { F(s,t): P[s,t] }; set X2 = { F(s,t): Q[s,t] }; assume B c= C; then A1: P[s, t] implies Q[s, t]; X1 c= X2 from FRAENKEL:sch 2(A1); hence thesis by XBOOLE_1:26; end; Lm6: a in B ^ C implies ex b st b c= a & b in mi B ^ C proof assume a in B ^ C; then consider b,c such that A1: b in B and A2: c in C and A3: a = b \/ c by Th34; consider d such that A4: d c= b and A5: d in mi B by A1,Th41; d \/ c c= a by A3,A4,Th12; then reconsider e = d \/ c as Element of DISJOINT_PAIRS A by Th26; take e; thus e c= a by A3,A4,Th12; thus thesis by A2,A5,Th35; end; theorem Th47: mi(B ^ C) c= mi B ^ C proof A1: mi B ^ C c= B ^ C by Th40,Th46; now let a; assume A2: a in mi(B ^ C); then a in B ^ C by Th36; then ex b st b c= a & b in mi B ^ C by Lm6; hence a in mi B ^ C by A1,A2,Th36; end; hence thesis by Lm5; end; theorem Th48: B^C = C^B proof deffunc F(Element of DISJOINT_PAIRS A,Element of DISJOINT_PAIRS A) = \$1 \/ \$2; defpred P[set,set] means \$1 in B & \$2 in C; defpred Q[set,set] means \$2 in C & \$1 in B; set X1 = { F(s,t) where s,t is Element of DISJOINT_PAIRS A: P[s,t] }; set X2 = { F(t,s) where s,t is Element of DISJOINT_PAIRS A: Q[s,t] }; A1: F(s,t) = F(t,s); A2: now let x be object; x in X2 iff ex s,t st x = t \/ s & t in C & s in B; then x in X2 iff ex t,s st x = t \/ s & t in C & s in B; hence x in X2 iff x in{ t \/ s where t,s: t in C & s in B }; end; A3: P[s,t] iff Q[s,t]; X1 = X2 from FRAENKEL:sch 8(A3,A1); hence thesis by A2,TARSKI:2; end; theorem Th49: B c= C implies D ^ B c= D ^ C proof D ^ C = C ^ D & D ^ B = B ^ D by Th48; hence thesis by Th46; end; theorem Th50: mi(mi B ^ C) = mi (B ^ C) proof A1: mi B ^ C c= B ^ C by Th40,Th46; now let a; assume A2: a in mi(mi B ^ C); A3: now let b; assume b in B ^ C; then consider c such that A4: c c= b and A5: c in mi B ^ C by Lm6; assume A6: b c= a; then c c= a by A4,Th2; then c = a by A2,A5,Th36; hence b = a by A4,A6,Th1; end; a in mi B ^ C by A2,Th36; hence a in mi(B ^ C) by A1,A3,Th39; end; hence mi(mi B ^ C) c= mi(B ^ C) by Lm5; A7: mi(B ^ C) c= mi B ^ C by Th47; now let a; assume A8: a in mi(B ^ C); then for b st b in mi B ^ C holds b c= a implies b = a by A1,Th36; hence a in mi(mi B ^ C) by A7,A8,Th39; end; hence thesis by Lm5; end; theorem Th51: mi(B ^ mi C) = mi (B ^ C) proof B ^ mi C = mi C ^ B & B ^ C = C ^ B by Th48; hence thesis by Th50; end; theorem Th52: K^(L^M) = K^L^M proof A1: L^M = M^L & K^L = L^K by Th48; A2: now let K,L,M; now let a; assume a in K^(L^M); then consider b,c such that A3: b in K and A4: c in L^M and A5: a = b \/ c by Th34; consider b1,c1 being Element of DISJOINT_PAIRS A such that A6: b1 in L and A7: c1 in M and A8: c = b1 \/ c1 by A4,Th34; reconsider d = b \/ (b1 \/ c1) as Element of DISJOINT_PAIRS A by A5,A8; A9: b \/(b1 \/ c1) = b \/ b1 \/ c1 by Th3; then b \/ b1 c= d by Th10; then reconsider c2 = b \/ b1 as Element of DISJOINT_PAIRS A by Th26; c2 in K^L by A3,A6,Th35; hence a in K^L^M by A5,A7,A8,A9,Th35; end; hence K^(L^M) c= K^L^M by Lm5; end; then A10: K^(L^M) c= K^L^M; K^L^M = M^(K^L) & K^(L^M) = L^M^K by Th48; then K^L^M c= K^(L^M) by A1,A2; hence thesis by A10; end; theorem Th53: K^(L \/ M) = K^L \/ K^M proof now let a; assume a in K^(L \/ M); then consider b,c such that A1: b in K and A2: c in L \/ M and A3: a = b \/ c by Th34; c in L or c in M by A2,XBOOLE_0:def 3; then a in K^L or a in K^M by A1,A3,Th35; hence a in K^L \/ K^M by XBOOLE_0:def 3; end; hence K^(L \/ M) c= K^L \/ K^M by Lm5; K^L c= K^(L \/ M) & K^M c= K^(L \/ M) by Th49,XBOOLE_1:7; hence thesis by XBOOLE_1:8; end; Lm7: a in B ^ C implies ex c st c in C & c c= a proof assume a in B ^ C; then consider b,c such that b in B and A1: c in C and A2: a = b \/ c by Th34; take c; thus c in C by A1; thus thesis by A2,Th10; end; Lm8: mi(K ^ L \/ L) = mi L proof now let a; assume A1: a in mi(K ^ L \/ L); A2: now let b; assume b in L; then b in K ^ L \/ L by XBOOLE_0:def 3; hence b c= a implies b = a by A1,Th36; end; A3: now assume a in K ^ L; then consider b such that A4: b in L and A5: b c= a by Lm7; b in K ^ L \/ L by A4,XBOOLE_0:def 3; hence a in L by A1,A4,A5,Th36; end; a in K ^ L \/ L by A1,Th36; then a in K ^ L or a in L by XBOOLE_0:def 3; hence a in mi L by A3,A2,Th39; end; hence mi(K ^ L \/ L) c= mi L by Lm5; now let a; assume A6: a in mi L; then A7: a in L by Th36; A8: now let b; assume b in K ^ L \/ L; then A9: b in K ^ L or b in L by XBOOLE_0:def 3; assume A10: b c= a; now assume b in K ^ L; then consider c such that A11: c in L and A12: c c= b by Lm7; c c= a by A10,A12,Th2; then c = a by A6,A11,Th36; hence b in L by A7,A10,A12,Th1; end; hence b = a by A6,A9,A10,Th36; end; a in K ^ L \/ L by A7,XBOOLE_0:def 3; hence a in mi(K ^ L \/ L) by A8,Th39; end; hence thesis by Lm5; end; theorem Th54: B c= B ^ B proof now let a; a = a \/ a; hence a in B implies a in B ^ B by Th35; end; hence thesis by Lm5; end; theorem Th55: mi(K ^ K) = mi K proof thus mi (K ^ K) = mi (K ^ K \/ K) by Th54,XBOOLE_1:12 .= mi K by Lm8; end; definition let A; func NormForm A -> strict LattStr means :Def12: 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 proof set L = Normal_forms_on A; deffunc O(Element of L,Element of L) = mi (\$1 \/ \$2); consider j being BinOp of L such that A1: for x,y being Element of L holds j.(x,y) = O(x,y) from BINOP_1:sch 4; deffunc O1(Element of L,Element of L) = mi (\$1 ^ \$2); consider m being BinOp of L such that A2: for x,y being Element of L holds m.(x,y) = O1(x,y) from BINOP_1: sch 4; take LattStr (# L, j, m #); thus thesis by A1,A2; end; uniqueness proof set L = Normal_forms_on A; let A1, A2 be strict LattStr such that A3: the carrier of A1 = L and A4: for A, B being Element of L holds (the L_join of A1).(A,B) = mi (A \/ B) & (the L_meet of A1).(A,B) = mi (A^B) and A5: the carrier of A2 = L and A6: for A, B being Element of L holds (the L_join of A2).(A,B) = mi (A \/ B) & (the L_meet of A2).(A,B) = mi (A^B); reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of L by A3,A5; now let x,y be Element of L; thus a1.(x,y) = mi (x \/ y) by A4 .= a2.(x,y) by A6; end; then A7: a1 = a2; now let x,y be Element of L; thus a3.(x,y) = mi (x^y) by A4 .= a4.(x,y) by A6; end; hence thesis by A3,A5,A7,BINOP_1:2; end; end; registration let A; cluster NormForm A -> non empty; coherence proof the carrier of NormForm A = Normal_forms_on A by Def12; hence thesis; end; end; Lm9: for a,b being Element of NormForm A holds a"\/"b = b"\/"a proof set G = NormForm A; let a,b be Element of G; reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12; a"\/"b = mi (b9 \/ a9) by Def12 .= b"\/"a by Def12; hence thesis; end; Lm10: for a,b,c being Element of NormForm A holds a"\/"(b"\/"c) = (a"\/"b)"\/" c proof set G = NormForm A; let a, b, c be Element of G; reconsider a9 = a, b9 = b, c9 = c as Element of Normal_forms_on A by Def12; a"\/"(b"\/"c) = (the L_join of G).(a, mi (b9 \/ c9)) by Def12 .= mi (mi (b9 \/ c9) \/ a9) by Def12 .= mi ( a9 \/ ( b9 \/ c9 ) ) by Th44 .= mi ( a9 \/ b9 \/ c9 ) by XBOOLE_1:4 .= mi ( mi ( a9 \/ b9 ) \/ c9 ) by Th44 .= (the L_join of G).(mi (a9 \/ b9), c9 ) by Def12 .= (a"\/"b)"\/"c by Def12; hence thesis; end; reserve K, L, M for Element of Normal_forms_on A; Lm11: (the L_join of NormForm A).((the L_meet of NormForm A).(K,L), L) = L proof thus (the L_join of NormForm A). ((the L_meet of NormForm A).(K,L), L) = ( the L_join of NormForm A).(mi (K^L), L) by Def12 .= mi(mi(K ^ L) \/ L) by Def12 .= mi(K ^ L \/ L) by Th44 .= mi L by Lm8 .= L by Th42; end; Lm12: for a,b being Element of NormForm A holds (a"/\"b)"\/" b = b proof let a,b be Element of NormForm A; reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12; set G = NormForm A; thus (a"/\"b)"\/"b = (the L_join of G).((the L_meet of G).(a9,b9), b9) .= b by Lm11; end; Lm13: for a,b being Element of NormForm A holds a"/\"b = b"/\"a proof set G = NormForm A; let a, b be Element of G; reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12; a"/\"b = mi (a9 ^ b9) by Def12 .= mi (b9 ^ a9) by Th48 .= b"/\"a by Def12; hence thesis; end; Lm14: for a,b,c being Element of NormForm A holds a"/\"(b"/\"c) = (a"/\"b)"/\" c proof set G = NormForm A; let a, b, c be Element of G; reconsider a9 = a, b9 = b, c9 = c as Element of Normal_forms_on A by Def12; a"/\"(b"/\"c) = (the L_meet of G).(a, mi (b9 ^ c9)) by Def12 .= mi (a9 ^ mi (b9 ^ c9)) by Def12 .= mi ( a9 ^ ( b9 ^ c9 ) ) by Th51 .= mi ( a9 ^ b9 ^ c9 ) by Th52 .= mi ( mi ( a9 ^ b9 ) ^ c9 ) by Th50 .= (the L_meet of G).(mi (a9 ^ b9), c9 ) by Def12 .= (a"/\"b)"/\"c by Def12; hence thesis; end; Lm15: (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 A1: (the L_meet of NormForm A).(K,M) = mi (K ^ M) by Def12; (the L_join of NormForm A).(L, M) = mi (L \/ M) & (the L_meet of NormForm A) .(K,L) = mi (K ^ L) by Def12; then reconsider La = (the L_join of NormForm A).(L, M), Lb = (the L_meet of NormForm A).(K,L), Lc = (the L_meet of NormForm A).(K,M) as Element of Normal_forms_on A by A1; (the L_meet of NormForm A). (K,(the L_join of NormForm A).(L,M)) = mi (K ^La) by Def12 .= mi (K^mi(L \/ M)) by Def12 .= mi (K^(L \/ M)) by Th51 .= mi (K^L \/ K^M) by Th53 .= mi (mi(K^L) \/ K^M) by Th44 .= mi (mi(K^L) \/ mi (K^M)) by Th44 .= mi (Lb \/ mi(K^M)) by Def12 .= mi (Lb \/ Lc) by Def12; hence thesis by Def12; end; Lm16: for a,b being Element of NormForm A holds a"/\"(a"\/"b)=a proof set G = NormForm A; let a,b be Element of G; reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12; thus a"/\"(a"\/"b) = (the L_join of G).((the L_meet of G).(a9,a9), (the L_meet of G).(a9,b9)) by Lm15 .= (the L_join of G).(mi (a9 ^ a9), (the L_meet of G).(a9,b9)) by Def12 .= (the L_join of G).(mi a9, (the L_meet of G).(a9,b9)) by Th55 .= a"\/"(a"/\"b) by Th42 .= (a"/\"b)"\/"a by Lm9 .= (b"/\"a)"\/"a by Lm13 .= a by Lm12; end; registration let A; cluster NormForm A -> Lattice-like; coherence proof set G = NormForm A; thus for u,v being Element of G holds u"\/"v = v"\/" u by Lm9; thus for u,v,w being Element of G holds u"\/"(v"\/"w) = (u"\/"v)"\/"w by Lm10; thus for u,v being Element of G holds (u"/\"v)"\/" v = v by Lm12; thus for u,v being Element of G holds u"/\"v = v"/\" u by Lm13; thus for u,v,w being Element of G holds u"/\"(v"/\"w) = (u"/\"v)"/\"w by Lm14; let u,v be Element of G; thus thesis by Lm16; end; end; registration let A; cluster NormForm A -> distributive lower-bounded; coherence proof set G = NormForm A; thus G is distributive proof let u,v,w be Element of G; reconsider K = u, L = v, M = w as Element of Normal_forms_on A by Def12; thus u "/\" (v "\/" w) = (the L_meet of G).(K,(the L_join of G). (L,M)) .= (u "/\" v) "\/" (u "/\" w) by Lm15; end; thus G is lower-bounded proof reconsider E = {} as Element of Normal_forms_on A by Lm4; reconsider e = E as Element of G by Def12; take e; let u be Element of G; reconsider K = u as Element of Normal_forms_on A by Def12; A1: e "\/" u = mi (E \/ K) by Def12 .= u by Th42; then u "/\" e = e by LATTICES:def 9; hence thesis by A1,LATTICES:def 9; end; end; end; theorem {} is Element of NormForm A proof the carrier of NormForm A = Normal_forms_on A by Def12; hence thesis by Lm4; end; theorem Bottom NormForm A = {} proof {} in Normal_forms_on A by Lm4; then reconsider Z = {} as Element of NormForm A by Def12; now let u be Element of NormForm A; reconsider z = Z, u9 = u as Element of Normal_forms_on A by Def12; thus Z "\/" u = mi (z \/ u9) by Def12 .= u by Th42; end; hence thesis by LATTICE2:14; end;