:: Lattice of Substitutions :: by Adam Grabowski :: :: Received May 21, 1997 :: Copyright (c) 1997-2016 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 SUBSET_1, FINSUB_1, PARTFUN1, FINSET_1, TARSKI, XBOOLE_0, NORMFORM, FUNCT_1, ORDINAL4, FUNCT_4, STRUCT_0, LATTICES, BINOP_1, EQREL_1, XXREAL_2, SUBSTLAT; notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, FINSUB_1, BINOP_1, STRUCT_0, FUNCT_1, PARTFUN1, LATTICES, FUNCT_4; constructors BINOP_1, FUNCT_4, FINSUB_1, LATTICES, RELSET_1; registrations XBOOLE_0, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1, LATTICES, FUNCT_1; requirements SUBSET, BOOLE; definitions TARSKI, LATTICES, XBOOLE_0; equalities LATTICES; expansions TARSKI, XBOOLE_0; theorems ZFMISC_1, TARSKI, FINSUB_1, FINSET_1, FUNCT_4, PARTFUN1, BINOP_1, LATTICES, LATTICE2, XBOOLE_0, XBOOLE_1, RELSET_1; schemes FRAENKEL, BINOP_1; begin :: Preliminaries reserve V, C for set; definition let V, C; func SubstitutionSet (V, C) -> Subset of Fin PFuncs (V, C) equals { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A & t in A & s c= t implies s = t ) }; coherence proof set IT = { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A & t in A & s c= t implies s = t ) }; IT c= Fin PFuncs (V,C) proof let x be object; assume x in IT; then ex B be Element of Fin PFuncs (V,C) st B = x &( for u being set st u in B holds u is finite)& for s, t being Element of PFuncs (V, C) holds ( s in B & t in B & s c= t implies s = t ); hence thesis; end; hence thesis; end; end; Lm1: for a, b be set st b in SubstitutionSet (V, C) & a in b holds a is finite proof let a, b be set; assume that A1: b in SubstitutionSet (V, C) and A2: a in b; ex A being Element of Fin PFuncs (V,C) st A = b &( for u being set st u in A holds u is finite)& for s, t being Element of PFuncs (V, C ) holds ( s in A & t in A & s c= t implies s = t ) by A1; hence thesis by A2; end; theorem Th1: {} in SubstitutionSet (V, C) proof {} c= PFuncs (V,C); then A1: {} in Fin PFuncs (V,C) by FINSUB_1:def 5; ( for u being set st u in {} holds u is finite)& for s, t being Element of PFuncs (V, C) holds ( s in {} & t in {} & s c= t implies s = t ); hence thesis by A1; end; theorem Th2: { {} } in SubstitutionSet (V, C) proof A1: for s, t being Element of PFuncs (V,C) holds ( s in { {} } & t in { {} } & s c= t implies s = t ) proof let s, t be Element of PFuncs (V,C); assume that A2: s in { {} } and A3: t in { {} } and s c= t; s = {} by A2,TARSKI:def 1; hence thesis by A3,TARSKI:def 1; end; {} is PartFunc of V,C by RELSET_1:12; then {} in PFuncs (V,C) by PARTFUN1:45; then { {} } c= PFuncs (V,C) by ZFMISC_1:31; then A4: { {} } in Fin PFuncs (V,C) by FINSUB_1:def 5; for u being set st u in { {} } holds u is finite; hence thesis by A4,A1; end; registration let V, C; cluster SubstitutionSet (V, C) -> non empty; coherence by Th2; end; definition let V, C; let A, B be Element of SubstitutionSet (V, C); redefine func A \/ B -> Element of Fin PFuncs (V, C); coherence proof A \/ B in Fin PFuncs (V, C); hence thesis; end; end; registration let V, C; cluster non empty for Element of SubstitutionSet (V, C); existence proof { {} } in SubstitutionSet (V, C) by Th2; hence thesis; end; end; registration let V, C; cluster -> finite for Element of SubstitutionSet (V, C); coherence; end; definition let V, C; let A be Element of Fin PFuncs (V, C); func mi A -> Element of SubstitutionSet (V, C) equals { t where t is Element of PFuncs (V, C) : t is finite & for s being Element of PFuncs (V, C) holds ( s in A & s c= t iff s = t ) }; coherence proof set M = { t where t is Element of PFuncs (V, C) : t is finite & for s being Element of PFuncs (V, C) holds ( s in A & s c= t iff s = t ) }; A1: M c= PFuncs (V,C) proof let a be object; assume a in M; then ex t9 being Element of PFuncs (V, C) st a = t9 & t9 is finite & for s being Element of PFuncs (V, C) holds ( s in A & s c= t9 iff s = t9 ); hence thesis; end; A2: now let x be object; assume x in M; then ex t being Element of PFuncs (V, C) st x = t & t is finite & for s being Element of PFuncs (V, C) holds s in A & s c= t iff s = t; hence x in A; end; then A3: M c= A; reconsider M as set; reconsider M9 = M as Element of Fin PFuncs (V,C) by A1,A3,FINSUB_1:def 5; A4: for u being set st u in M9 holds u is finite proof let u be set; assume u in M9; then ex t9 being Element of PFuncs (V, C) st u = t9 & t9 is finite & for s being Element of PFuncs (V, C) holds ( s in A & s c= t9 iff s = t9 ); hence thesis; end; for s, t being Element of PFuncs (V, C) holds ( s in M9 & t in M9 & s c= t implies s = t ) proof let s, t be Element of PFuncs (V, C); assume that A5: s in M9 & t in M9 and A6: s c= t; s in A & ex tt being Element of PFuncs (V, C) st t = tt & tt is finite & for ss being Element of PFuncs (V, C) holds ( ss in A & ss c= tt iff ss = tt ) by A2,A5; hence thesis by A6; end; then M in { A1 where A1 is Element of Fin PFuncs (V,C) : ( for u being set st u in A1 holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A1 & t in A1 & s c= t implies s = t ) } by A4; hence thesis; end; end; registration let V, C; cluster -> functional for Element of SubstitutionSet(V, C); coherence proof let A be Element of SubstitutionSet (V, C); A c= PFuncs (V,C) by FINSUB_1:def 5; hence thesis; end; end; definition let V, C; let A, B be Element of Fin PFuncs (V, C); func A^B -> Element of Fin PFuncs (V, C) equals { s \/ t where s,t is Element of PFuncs (V,C) : s in A & t in B & s tolerates t }; coherence proof deffunc U(Element of PFuncs (V,C),Element of PFuncs (V,C)) = \$1 \/ \$2; set M = { U(s,t) where s,t is Element of PFuncs (V,C) : s in A & t in B & s tolerates t }, N = { U(s,t) where s,t is Element of PFuncs (V,C) : s in A & t in B }; A1: M c= N proof let a be object; assume a in M; then ex s,t being Element of PFuncs (V,C) st a = s \/ t & s in A & t in B & s tolerates t; hence thesis; end; A2: M c= PFuncs (V, C) proof let y be object; assume y in M; then consider s,t being Element of PFuncs (V,C) such that A3: y = s \/ t and s in A and t in B and A4: s tolerates t; reconsider s99 = s, t99 = t as PartFunc of V,C by PARTFUN1:47; reconsider s9 = s, t9 = t as Function; s is PartFunc of V, C & t is PartFunc of V, C by PARTFUN1:47; then s9 +* t9 is PartFunc of V,C by FUNCT_4:40; then s99 \/ t99 is PartFunc of V,C by A4,FUNCT_4:30; hence thesis by A3,PARTFUN1:45; end; A5: B is finite; A6: A is finite; N is finite from FRAENKEL:sch 22(A6,A5); hence thesis by A1,A2,FINSUB_1:def 5; end; end; reserve A, B, D for Element of Fin PFuncs (V, C); theorem Th3: A^B = B^A proof deffunc U(Element of PFuncs (V,C),Element of PFuncs (V,C)) = \$1 \/ \$2; defpred X[Function,Function] means \$1 in A & \$2 in B & \$1 tolerates \$2; defpred Y[Function,Function] means \$2 in B & \$1 in A & \$2 tolerates \$1; set X1 = { U(s,t) where s is Element of PFuncs (V,C), t is Element of PFuncs (V,C) : X[s,t] }; set X2 = { U(t,s) where s is Element of PFuncs (V,C), t is Element of PFuncs (V,C) : Y[s,t] }; A1: now let x be object; x in X2 iff ex s,t being Element of PFuncs (V,C) st x = U(t,s) & Y[s,t ]; then x in X2 iff ex t,s being Element of PFuncs (V,C) st x = t \/ s & t in B & s in A & t tolerates s; hence x in X2 iff x in { t \/ s where t is Element of PFuncs (V,C), s is Element of PFuncs (V,C) : t in B & s in A & t tolerates s }; end; A2: for s, t being Element of PFuncs (V,C) holds U(s,t) = U(t,s); A3: for s, t being Element of PFuncs (V,C) holds X[s,t] iff Y[s,t]; X1 = X2 from FRAENKEL:sch 8(A3,A2); hence thesis by A1,TARSKI:2; end; theorem Th4: B = { {} } implies A ^ B = A proof A1: { s \/ t where s,t is Element of PFuncs (V,C) : s in A & t in { {} } & s tolerates t } c= A proof let a be object; assume a in { s \/ t where s,t is Element of PFuncs (V,C) : s in A & t in { {} } & s tolerates t }; then consider s9, t9 being Element of PFuncs (V,C) such that A2: a = s9 \/ t9 & s9 in A and A3: t9 in { {} } and s9 tolerates t9; t9 = {} by A3,TARSKI:def 1; hence thesis by A2; end; A4: A c= { s \/ t where s,t is Element of PFuncs (V,C) : s in A & t in { {} } & s tolerates t } proof {} is PartFunc of V, C by RELSET_1:12; then reconsider b = {} as Element of PFuncs (V,C) by PARTFUN1:45; let a be object; assume A5: a in A; A c= PFuncs (V,C) by FINSUB_1:def 5; then reconsider a9 = a as Element of PFuncs (V,C) by A5; A6: b in { {} } by TARSKI:def 1; a = a9 \/ b & a9 tolerates b by PARTFUN1:59; hence thesis by A5,A6; end; assume B = { {} }; hence thesis by A1,A4; end; theorem Th5: for a, b be set holds B in SubstitutionSet (V, C) & a in B & b in B & a c= b implies a = b proof let a, b be set; assume B in SubstitutionSet (V, C); then A1: ex A1 be Element of Fin PFuncs (V,C) st A1 = B & ( for u being set st u in A1 holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A1 & t in A1 & s c= t implies s = t ); assume that A2: a in B & b in B and A3: a c= b; B c= PFuncs (V,C) by FINSUB_1:def 5; then reconsider a9 = a, b9 = b as Element of PFuncs (V, C) by A2; a9 = b9 by A1,A2,A3; hence thesis; end; theorem Th6: for a be set holds a in mi B implies a in B & for b be set holds b in B & b c= a implies b = a proof let a be set; assume a in mi B; then A1: ex t being Element of PFuncs (V, C) st a = t & t is finite & for s being Element of PFuncs (V, C) holds s in B & s c= t iff s = t; hence a in B; let b be set; assume that A2: b in B and A3: b c= a; B c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider b9 = b as Element of PFuncs (V, C) by A2; b9 = a by A1,A2,A3; hence thesis; end; reserve s for Element of PFuncs (V,C); registration let V, C; cluster finite for Element of PFuncs (V,C); existence proof {} is PartFunc of V,C by RELSET_1:12; then reconsider e = {} as Element of PFuncs (V,C) by PARTFUN1:45; take e; thus thesis; end; end; theorem Th7: for a be finite set holds a in B & (for b be finite set st b in B & b c= a holds b = a) implies a in mi B proof let a be finite set; assume that A1: a in B and A2: for s be finite set st s in B & s c= a holds s = a; B c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider a9 = a as Element of PFuncs (V, C) by A1; s in B & s c= a iff s = a by A1,A2; then a9 in { t where t is Element of PFuncs (V,C) : t is finite & for s being Element of PFuncs (V, C) holds s in B & s c= t iff s = t }; hence thesis; end; theorem Th8: mi A c= A by Th6; theorem A = {} implies mi A = {} by Th8,XBOOLE_1:3; theorem Th10: for b be finite set holds b in B implies ex c be set st c c= b & c in mi B proof defpred X[set,set] means \$1 c= \$2; let b be finite set; assume A1: b in B; A2: B c= PFuncs (V,C) by FINSUB_1:def 5; then reconsider b9 = b as Element of PFuncs (V, C) by A1; A3: for a,b,c be Element of PFuncs (V, C) st X[a,b] & X[b,c] holds X[a,c] by XBOOLE_1:1; A4: for a be Element of PFuncs (V, C) holds X[a,a]; for a be Element of PFuncs (V, C) st a in B ex b be Element of PFuncs (V , C) st b in B & X[b,a] & for c be Element of PFuncs (V, C) st c in B & X[c,b] holds X[b,c] from FRAENKEL:sch 23(A4,A3); then consider c be Element of PFuncs (V, C) such that A5: c in B and A6: c c= b9 and A7: for a be Element of PFuncs (V, C) st a in B & a c= c holds c c= a by A1; take c; thus c c= b by A6; for b be finite set st b in B & b c= c holds b = c by A2,A7; hence thesis by A5,A6,Th7; end; theorem Th11: for K be Element of SubstitutionSet (V, C) holds mi K = K proof let K be Element of SubstitutionSet (V, C); thus mi K c= K by Th8; now let a be set; assume A1: a in K; then a is finite & for b be finite set st b in K & b c= a holds b = a by Lm1,Th5; hence a in mi K by A1,Th7; end; hence thesis; end; theorem Th12: mi (A \/ B) c= mi A \/ B proof now let a be set; assume A1: a in mi (A \/ B); then reconsider a9 = a as finite set by Lm1; A2: a in A \/ B by A1,Th6; now per cases by A2,XBOOLE_0:def 3; suppose A3: a in A; now let b be finite set; assume b in A; then b in A \/ B by XBOOLE_0:def 3; hence b c= a implies b = a by A1,Th6; end; then a9 in mi A by A3,Th7; hence a in mi A \/ B by XBOOLE_0:def 3; end; suppose a in B; hence a in mi A \/ B by XBOOLE_0:def 3; end; end; hence a in mi A \/ B; end; hence thesis; end; theorem Th13: mi(mi A \/ B) = mi (A \/ B) proof A1: mi A \/ B c= A \/ B by Th8,XBOOLE_1:9; now let a be set; assume A2: a in mi(mi A \/ B); then reconsider a9 = a as finite set by Lm1; A3: now let b be finite set; assume that A4: b in A \/ B and A5: b c= a; now per cases by A4,XBOOLE_0:def 3; suppose b in A; then consider c be set such that A6: c c= b and A7: c in mi A by Th10; c in mi A \/ B & c c= a by A5,A6,A7,XBOOLE_0:def 3; then c = a by A2,Th6; hence b = a by A5,A6; end; suppose b in B; then b in mi A \/ B by XBOOLE_0:def 3; hence b = a by A2,A5,Th6; end; end; hence b = a; end; a in mi A \/ B by A2,Th6; then a9 in mi (A \/ B) by A1,A3,Th7; hence a in mi (A \/ B); end; hence mi(mi A \/ B) c= mi (A \/ B); A8: mi(A \/ B) c= mi A \/ B by Th12; now let a be set; assume A9: a in mi (A \/ B); then reconsider a9 = a as finite set by Lm1; for b be finite set st b in mi A \/ B holds b c= a implies b = a by A1,A9 ,Th6; then a9 in mi(mi A \/ B) by A8,A9,Th7; hence a in mi(mi A \/ B); end; hence thesis; end; theorem Th14: A c= B implies A ^ D c= B ^ D proof deffunc U(Element of PFuncs (V,C),Element of PFuncs (V,C)) = \$1 \/ \$2; defpred X[Function,Function] means \$1 in A & \$2 in D & \$1 tolerates \$2; defpred Y[Function,Function] means \$1 in B & \$2 in D & \$1 tolerates \$2; set X1 = { U(s,t) where s, t is Element of PFuncs (V,C) : X[s,t]}, X2 = { U( s,t) where s, t is Element of PFuncs (V,C) : Y[s,t]}; assume A c= B; then A1: for s, t being Element of PFuncs (V,C) holds X[s,t] implies Y[s,t]; X1 c= X2 from FRAENKEL:sch 2(A1); hence thesis; end; theorem Th15: for a be set holds a in A^B implies ex b,c be set st b in A & c in B & a = b \/ c proof let a be set; assume a in A^B; then ex s,t be Element of PFuncs (V,C) st a = s \/ t & s in A & t in B & s tolerates t; hence thesis; end; theorem for b, c be Element of PFuncs (V, C) holds b in A & c in B & b tolerates c implies b \/ c in A^B; Lm2: for a be finite set holds a in A ^ B implies ex b be finite set st b c= a & b in mi A ^ B proof let a be finite set; assume a in A ^ B; then consider b, c be Element of PFuncs (V,C) such that A1: a = b \/ c and A2: b in A and A3: c in B and A4: b tolerates c; b is finite by A1,FINSET_1:1,XBOOLE_1:7; then consider d be set such that A5: d c= b and A6: d in mi A by A2,Th10; A7: mi A c= PFuncs (V,C) by FINSUB_1:def 5; then reconsider d9 = d, c9 = c as Element of PFuncs (V, C) by A6; reconsider d1 = d, b1 = b, c1 = c as PartFunc of V, C by A6,A7,PARTFUN1:46; d1 c= b1 by A5; then A8: d9 tolerates c9 by A4,PARTFUN1:58; then d9 \/ c9 = d9 +* c9 by FUNCT_4:30; then reconsider e = d1 \/ c1 as Element of PFuncs (V, C) by PARTFUN1:45; reconsider e as finite set by A1,A5,FINSET_1:1,XBOOLE_1:9; take e; thus e c= a by A1,A5,XBOOLE_1:9; thus thesis by A3,A6,A8; end; theorem Th17: mi(A ^ B) c= mi A ^ B proof A1: mi A ^ B c= A ^ B by Th8,Th14; now let a be set; assume A2: a in mi (A ^ B); then a in A ^ B & a is finite by Lm1,Th6; then ex b be finite set st b c= a & b in mi A ^ B by Lm2; hence a in mi A ^ B by A1,A2,Th6; end; hence thesis; end; theorem Th18: A c= B implies D ^ A c= D ^ B proof D ^ A = A ^ D & D ^ B = B ^ D by Th3; hence thesis by Th14; end; theorem Th19: mi(mi A ^ B) = mi (A ^ B) proof A1: mi A ^ B c= A ^ B by Th8,Th14; now let a be set; assume A2: a in mi (mi A ^ B); A3: now let b be finite set; assume b in A ^ B; then consider c be finite set such that A4: c c= b and A5: c in mi A ^ B by Lm2; assume A6: b c= a; then c c= a by A4; then c = a by A2,A5,Th6; hence b = a by A4,A6; end; a in mi A ^ B & a is finite by A2,Lm1,Th6; hence a in mi (A ^ B) by A1,A3,Th7; end; hence mi(mi A ^ B) c= mi(A ^ B); A7: mi(A ^ B) c= mi A ^ B by Th17; now let a be set; assume A8: a in mi(A ^ B); then a is finite & for b be finite set st b in mi A ^ B holds b c= a implies b = a by A1,Lm1,Th6; hence a in mi(mi A ^ B) by A7,A8,Th7; end; hence thesis; end; theorem Th20: mi(A ^ mi B) = mi (A ^ B) proof A ^ mi B = mi B ^ A & A ^ B = B ^ A by Th3; hence thesis by Th19; end; theorem Th21: for K, L, M being Element of Fin PFuncs (V, C) holds K^(L^M) = K ^L^M proof let K, L, M be Element of Fin PFuncs (V, C); A1: L^M = M^L & K^L = L^K by Th3; A2: now let K, L, M be Element of Fin PFuncs (V, C); A3: K c= PFuncs (V,C) & L c= PFuncs (V,C) by FINSUB_1:def 5; A4: M c= PFuncs (V,C) by FINSUB_1:def 5; now let a be set; A5: K^(L^M) c= PFuncs (V,C) by FINSUB_1:def 5; assume A6: a in K^(L^M); then consider b,c be set such that A7: b in K and A8: c in L^M and A9: a = b \/ c by Th15; A10: c c= b \/ c by XBOOLE_1:7; consider b1, c1 being set such that A11: b1 in L and A12: c1 in M and A13: c = b1 \/ c1 by A8,Th15; reconsider b2 = b, b12 = b1 as PartFunc of V, C by A3,A7,A11,PARTFUN1:46; reconsider b9 = b, b19 = b1, c19 = c1 as Element of PFuncs (V,C) by A3,A4 ,A7,A11,A12; b1 c= c by A13,XBOOLE_1:7; then A14: b c= b \/ c & b1 c= b \/ c by A10,XBOOLE_1:7; then A15: b9 tolerates b19 by A6,A9,A5,PARTFUN1:57; then b9 \/ b19 = b9 +* b19 by FUNCT_4:30; then b2 \/ b12 is PartFunc of V, C; then reconsider c2 = b9 \/ b19 as Element of PFuncs (V,C) by PARTFUN1:45; A16: b \/ (b1 \/ c1) = b \/ b1 \/ c1 & c2 in K^L by A7,A11,A15,XBOOLE_1:4; c1 c= c by A13,XBOOLE_1:7; then A17: c1 c= b \/ c by A10; c2 c= b \/ c by A14,XBOOLE_1:8; then c2 tolerates c19 by A6,A9,A5,A17,PARTFUN1:57; hence a in K^L^M by A9,A12,A13,A16; end; hence K^(L^M) c= K^L^M; end; then A18: K^(L^M) c= K^L^M; K^L^M = M^(K^L) & K^(L^M) = L^M^K by Th3; then K^L^M c= K^(L^M) by A1,A2; hence thesis by A18; end; theorem Th22: for K, L, M being Element of Fin PFuncs (V, C) holds K^(L \/ M) = K^L \/ K^M proof let K, L, M be Element of Fin PFuncs (V, C); now let a be set; assume A1: a in K^(L \/ M); then consider b,c being set such that A2: b in K and A3: c in L \/ M and A4: a = b \/ c by Th15; K^(L \/ M) c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider a9 = a as Element of PFuncs (V,C) by A1; K c= PFuncs (V, C) & L \/ M c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider b9 = b, c9 = c as Element of PFuncs (V,C) by A2,A3; b9 c= a9 & c9 c= a9 by A4,XBOOLE_1:7; then A5: b9 tolerates c9 by PARTFUN1:57; c9 in L or c9 in M by A3,XBOOLE_0:def 3; then a in K^L or a in K^M by A2,A4,A5; hence a in K^L \/ K^M by XBOOLE_0:def 3; end; hence K^(L \/ M) c= K^L \/ K^M; K^L c= K^(L \/ M) & K^M c= K^(L \/ M) by Th18,XBOOLE_1:7; hence thesis by XBOOLE_1:8; end; Lm3: for a be set holds a in A ^ B implies ex c be set st c in B & c c= a proof let a be set; assume a in A ^ B; then consider b,c be set such that b in A and A1: c in B and A2: a = b \/ c by Th15; take c; thus c in B by A1; thus thesis by A2,XBOOLE_1:7; end; Lm4: for K, L being Element of Fin PFuncs (V, C) holds mi(K ^ L \/ L) = mi L proof let K, L be Element of Fin PFuncs (V, C); now let a be set; assume A1: a in mi(K ^ L \/ L); then a in K ^ L \/ L by Th6; then A2: a in K ^ L or a in L by XBOOLE_0:def 3; A3: now let b be finite set; assume b in L; then b in K ^ L \/ L by XBOOLE_0:def 3; hence b c= a implies b = a by A1,Th6; end; A4: now assume a in K ^ L; then consider b be set such that A5: b in L and A6: b c= a by Lm3; b in K ^ L \/ L by A5,XBOOLE_0:def 3; hence a in L by A1,A5,A6,Th6; end; a is finite by A1,Lm1; hence a in mi L by A2,A4,A3,Th7; end; hence mi(K ^ L \/ L) c= mi L; now let a be set; assume A7: a in mi L; then A8: a in L by Th6; then A9: a in K ^ L \/ L by XBOOLE_0:def 3; A10: now let b be finite set; assume b in K ^ L \/ L; then A11: b in K ^ L or b in L by XBOOLE_0:def 3; assume A12: b c= a; now assume b in K ^ L; then consider c be set such that A13: c in L and A14: c c= b by Lm3; c c= a by A12,A14; then c = a by A7,A13,Th6; hence b in L by A8,A12,A14,XBOOLE_0:def 10; end; hence b = a by A7,A11,A12,Th6; end; a is finite by A7,Lm1; hence a in mi(K ^ L \/ L) by A9,A10,Th7; end; hence thesis; end; theorem Th23: B c= B ^ B proof now let a be set; assume A1: a in B; B c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider a9 = a as Element of PFuncs (V,C) by A1; a = a \/ a & a9 tolerates a9; hence a in B ^ B by A1; end; hence thesis; end; theorem Th24: mi (A ^ A) = mi A proof thus mi (A ^ A) = mi (A ^ A \/ A) by Th23,XBOOLE_1:12 .= mi A by Lm4; end; theorem for K be Element of SubstitutionSet (V, C) holds mi (K^K) = K proof let K be Element of SubstitutionSet (V, C); thus mi (K^K) = mi K by Th24 .= K by Th11; end; begin :: Definition of the lattice definition let V, C; func SubstLatt (V, C) -> strict LattStr means :Def4: the carrier of it = SubstitutionSet (V, C) & for A, B being Element of SubstitutionSet (V, C) holds (the L_join of it).(A,B) = mi (A \/ B) & (the L_meet of it).(A,B) = mi (A^B); existence proof deffunc U(Element of SubstitutionSet (V, C), Element of SubstitutionSet (V , C)) = mi (\$1 \/ \$2); consider j being BinOp of SubstitutionSet (V, C) such that A1: for x,y being Element of SubstitutionSet (V, C) holds j.(x,y) = U( x,y) from BINOP_1:sch 4; deffunc U(Element of SubstitutionSet (V, C), Element of SubstitutionSet (V , C)) = mi (\$1 ^ \$2); consider m being BinOp of SubstitutionSet (V, C) such that A2: for x,y being Element of SubstitutionSet (V, C) holds m.(x,y) = U( x,y) from BINOP_1:sch 4; take LattStr (# SubstitutionSet (V, C), j, m #); thus thesis by A1,A2; end; uniqueness proof let A1, A2 be strict LattStr such that A3: the carrier of A1 = SubstitutionSet (V, C) and A4: for A, B being Element of SubstitutionSet (V, C) 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 = SubstitutionSet (V, C) and A6: for A, B being Element of SubstitutionSet (V, C) 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 SubstitutionSet (V, C) by A3,A5; now let x,y be Element of SubstitutionSet (V, C); thus a1.(x,y) = mi (x \/ y) by A4 .= a2.(x,y) by A6; end; then A7: a1 = a2 by BINOP_1:2; now let x,y be Element of SubstitutionSet (V, C); 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 V, C; cluster SubstLatt (V, C) -> non empty; coherence proof the carrier of SubstLatt (V, C) = SubstitutionSet (V, C) by Def4; hence thesis; end; end; Lm5: for a,b being Element of SubstLatt (V, C) holds a"\/"b = b"\/"a proof set G = SubstLatt (V, C); let a,b be Element of G; reconsider a9 = a, b9 = b as Element of SubstitutionSet (V, C) by Def4; a"\/"b = mi (b9 \/ a9) by Def4 .= b"\/"a by Def4; hence thesis; end; Lm6: for a,b,c being Element of SubstLatt (V, C) holds a"\/"(b"\/"c) = (a"\/"b )"\/"c proof let a, b, c be Element of SubstLatt (V, C); reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V, C) by Def4; set G = SubstLatt (V, C); a"\/"(b"\/"c) = (the L_join of G).(a, mi (b9 \/ c9)) by Def4 .= mi (mi (b9 \/ c9) \/ a9) by Def4 .= mi ( a9 \/ ( b9 \/ c9 ) ) by Th13 .= mi ( a9 \/ b9 \/ c9 ) by XBOOLE_1:4 .= mi ( mi ( a9 \/ b9 ) \/ c9 ) by Th13 .= (the L_join of G).(mi (a9 \/ b9), c9 ) by Def4 .= (a"\/"b)"\/"c by Def4; hence thesis; end; reserve K, L, M for Element of SubstitutionSet (V,C); Lm7: (the L_join of SubstLatt (V, C)). ((the L_meet of SubstLatt (V, C)).(K,L) , L) = L proof thus (the L_join of SubstLatt (V, C)). ((the L_meet of SubstLatt (V, C)).(K, L), L) = (the L_join of SubstLatt (V, C)).(mi (K^L), L) by Def4 .= mi(mi(K ^ L) \/ L) by Def4 .= mi(K ^ L \/ L) by Th13 .= mi L by Lm4 .= L by Th11; end; Lm8: for a,b being Element of SubstLatt (V, C) holds (a"/\"b)"\/"b = b proof let a,b be Element of SubstLatt (V, C); reconsider a9 = a, b9 = b as Element of SubstitutionSet (V, C) by Def4; set G = SubstLatt (V, C); thus (a"/\"b)"\/"b = (the L_join of G).((the L_meet of G).(a9,b9), b9) .= b by Lm7; end; Lm9: for a,b being Element of SubstLatt (V, C) holds a"/\"b = b"/\"a proof let a, b be Element of SubstLatt (V, C); reconsider a9 = a, b9 = b as Element of SubstitutionSet (V, C) by Def4; a"/\"b = mi (a9 ^ b9) by Def4 .= mi (b9 ^ a9) by Th3 .= b"/\"a by Def4; hence thesis; end; Lm10: for a,b,c being Element of SubstLatt (V, C) holds a"/\"(b"/\"c) = (a"/\" b)"/\"c proof let a, b, c be Element of SubstLatt (V, C); reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V, C) by Def4; set G = SubstLatt (V, C); a"/\"(b"/\"c) = (the L_meet of G).(a, mi (b9 ^ c9)) by Def4 .= mi (a9 ^ mi (b9 ^ c9)) by Def4 .= mi ( a9 ^ ( b9 ^ c9 ) ) by Th20 .= mi ( a9 ^ b9 ^ c9 ) by Th21 .= mi ( mi ( a9 ^ b9 ) ^ c9 ) by Th19 .= (the L_meet of G).(mi (a9 ^ b9), c9 ) by Def4 .= (a"/\"b)"/\"c by Def4; hence thesis; end; Lm11: (the L_meet of SubstLatt (V, C)).(K,(the L_join of SubstLatt (V, C)). (L ,M)) = (the L_join of SubstLatt (V, C)).((the L_meet of SubstLatt (V, C)).(K,L) , (the L_meet of SubstLatt (V, C)).(K,M)) proof A1: (the L_meet of SubstLatt (V, C)).(K,M) = mi (K ^ M) by Def4; (the L_join of SubstLatt (V, C)).(L, M) = mi (L \/ M) & (the L_meet of SubstLatt (V, C)).(K,L) = mi (K ^ L) by Def4; then reconsider La = (the L_join of SubstLatt (V, C)).(L, M), Lb = (the L_meet of SubstLatt (V, C)).(K,L), Lc = (the L_meet of SubstLatt (V, C)).(K,M) as Element of SubstitutionSet (V,C) by A1; (the L_meet of SubstLatt (V, C)). (K,(the L_join of SubstLatt (V, C)).(L ,M)) = mi (K^La) by Def4 .= mi (K^mi(L \/ M)) by Def4 .= mi (K^(L \/ M)) by Th20 .= mi (K^L \/ K^M) by Th22 .= mi (mi(K^L) \/ K^M) by Th13 .= mi (mi(K^L) \/ mi (K^M)) by Th13 .= mi (Lb \/ mi(K^M)) by Def4 .= mi (Lb \/ Lc) by Def4; hence thesis by Def4; end; Lm12: for a,b being Element of SubstLatt (V, C) holds a"/\"(a"\/"b)=a proof let a,b be Element of SubstLatt (V, C); reconsider a9 = a, b9 = b as Element of SubstitutionSet (V, C) by Def4; thus a"/\"(a"\/"b) = (the L_join of SubstLatt (V, C)).((the L_meet of SubstLatt (V, C)).(a9,a9), (the L_meet of SubstLatt (V, C)).(a9,b9)) by Lm11 .= (the L_join of SubstLatt (V, C)).(mi (a9 ^ a9), (the L_meet of SubstLatt (V, C)).(a9,b9)) by Def4 .= (the L_join of SubstLatt (V, C)).(mi a9, (the L_meet of SubstLatt (V, C)).(a9,b9)) by Th24 .= a"\/"(a"/\"b) by Th11 .= (a"/\"b)"\/"a by Lm5 .= (b"/\"a)"\/"a by Lm9 .= a by Lm8; end; registration let V, C; cluster SubstLatt (V, C) -> Lattice-like; coherence proof set G = SubstLatt (V, C); thus for u,v being Element of G holds u"\/"v = v"\/"u by Lm5; thus for u,v,w being Element of G holds u"\/"(v"\/"w) = (u"\/"v)"\/"w by Lm6; thus for u,v being Element of G holds (u"/\"v)"\/" v = v by Lm8; 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; let u,v be Element of G; thus thesis by Lm12; end; end; registration let V, C; cluster SubstLatt (V, C) -> distributive bounded; coherence proof thus SubstLatt (V, C) is distributive proof let u,v,w be Element of SubstLatt (V, C); reconsider K = u, L = v, M = w as Element of SubstitutionSet (V,C) by Def4; thus u "/\" (v "\/" w) = (the L_meet of SubstLatt (V, C)).(K,(the L_join of SubstLatt (V, C)). (L,M)) .= (u "/\" v) "\/" (u "/\" w) by Lm11; end; A1: SubstLatt (V, C) is lower-bounded proof reconsider E = {} as Element of SubstitutionSet (V,C) by Th1; set L = SubstLatt (V, C); reconsider e = E as Element of L by Def4; take e; let u be Element of L; reconsider K = u as Element of SubstitutionSet (V,C) by Def4; A2: e "\/" u = mi (E \/ K) by Def4 .= u by Th11; then u "/\" e = e by LATTICES:def 9; hence thesis by A2,LATTICES:def 9; end; SubstLatt (V, C) is upper-bounded proof reconsider E = { {} } as Element of SubstitutionSet (V,C) by Th2; set L = SubstLatt (V, C); reconsider e = E as Element of L by Def4; take e; let u be Element of L; reconsider K = u as Element of SubstitutionSet (V,C) by Def4; A3: e "/\" u = mi (E ^ K) by Def4 .= mi (K ^ E) by Th3 .= mi K by Th4 .= u by Th11; then e "\/" u = e by LATTICES:def 8; hence thesis by A3,LATTICES:def 8; end; hence SubstLatt (V, C) is bounded by A1; end; end; theorem Bottom SubstLatt (V,C) = {} proof {} in SubstitutionSet (V,C) by Th1; then reconsider Z = {} as Element of SubstLatt (V,C) by Def4; now let u be Element of SubstLatt (V,C); reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4; thus Z "\/" u = mi (z \/ u9) by Def4 .= u by Th11; end; hence thesis by LATTICE2:14; end; theorem Top SubstLatt (V,C) = { {} } proof { {} } in SubstitutionSet (V,C) by Th2; then reconsider Z = { {} } as Element of SubstLatt (V,C) by Def4; now let u be Element of SubstLatt (V,C); reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4; thus Z "/\" u = mi (z ^ u9) by Def4 .= mi (u9 ^ z) by Th3 .= mi u9 by Th4 .= u by Th11; end; hence thesis by LATTICE2:16; end;