:: MMLQUERY semantic presentation begin definition let X be set ; mode List of X is Subset of X; mode Operation of X is Relation of X; end; definition let x, y, R be set ; predx,y in R means :Def1: :: MMLQUERY:def 1 [x,y] in R; end; :: deftheorem Def1 defines in MMLQUERY:def_1_:_ for x, y, R being set holds ( x,y in R iff [x,y] in R ); notation let x, y, R be set ; antonym x,y nin R for x,y in R; end; theorem Th9: :: MMLQUERY:1 for R1, R2 being Relation holds ( R1 c= R2 iff for z being set holds Im (R1,z) c= Im (R2,z) ) proof let R1, R2 be Relation; ::_thesis: ( R1 c= R2 iff for z being set holds Im (R1,z) c= Im (R2,z) ) hereby ::_thesis: ( ( for z being set holds Im (R1,z) c= Im (R2,z) ) implies R1 c= R2 ) assume Z1: R1 c= R2 ; ::_thesis: for z being set holds Im (R1,z) c= Im (R2,z) let z be set ; ::_thesis: Im (R1,z) c= Im (R2,z) thus Im (R1,z) c= Im (R2,z) ::_thesis: verum proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Im (R1,z) or s in Im (R2,z) ) assume s in Im (R1,z) ; ::_thesis: s in Im (R2,z) then consider v being set such that A1: ( [v,s] in R1 & v in {z} ) by RELAT_1:def_13; thus s in Im (R2,z) by Z1, A1, RELAT_1:def_13; ::_thesis: verum end; end; assume Z2: for z being set holds Im (R1,z) c= Im (R2,z) ; ::_thesis: R1 c= R2 let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in R1 or [a,b] in R2 ) assume [a,b] in R1 ; ::_thesis: [a,b] in R2 then ( b in Im (R1,a) & Im (R1,a) c= Im (R2,a) ) by Z2, RELAT_1:169; hence [a,b] in R2 by RELAT_1:169; ::_thesis: verum end; notation let X be set ; let O be Operation of X; let x be Element of X; synonym x . O for Im (X,O); end; definition let X be set ; let O be Operation of X; let x be Element of X; :: original: . redefine funcx . O -> List of X; coherence . x is List of X proof . x = O .: {x} ; hence . x is Subset of X ; ::_thesis: verum end; end; theorem Th0: :: MMLQUERY:2 for X being set for x being Element of X for O being Operation of X for y being Element of X holds ( x,y in O iff y in x . O ) proof let X be set ; ::_thesis: for x being Element of X for O being Operation of X for y being Element of X holds ( x,y in O iff y in x . O ) let x be Element of X; ::_thesis: for O being Operation of X for y being Element of X holds ( x,y in O iff y in x . O ) let O be Operation of X; ::_thesis: for y being Element of X holds ( x,y in O iff y in x . O ) let y be Element of X; ::_thesis: ( x,y in O iff y in x . O ) ( x,y in O iff [x,y] in O ) by Def1; hence ( x,y in O iff y in x . O ) by RELAT_1:169; ::_thesis: verum end; notation let X be set ; let O be Operation of X; let L be List of X; synonym L | O for X .: O; end; definition let X be set ; let O be Operation of X; let L be List of X; :: original: | redefine funcL | O -> List of X equals :: MMLQUERY:def 2 union { (x . O) where x is Element of X : x in L } ; coherence | L is List of X proof thus O .: L is Subset of X ; ::_thesis: verum end; compatibility for b1 being List of X holds ( b1 = | L iff b1 = union { (x . O) where x is Element of X : x in L } ) proof union { (x . O) where x is Element of X : x in L } = | L proof thus union { (x . O) where x is Element of X : x in L } c= | L :: according to XBOOLE_0:def_10 ::_thesis: | L c= union { (x . O) where x is Element of X : x in L } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { (x . O) where x is Element of X : x in L } or z in | L ) assume z in union { (x . O) where x is Element of X : x in L } ; ::_thesis: z in | L then consider Y being set such that A1: ( z in Y & Y in { (x . O) where x is Element of X : x in L } ) by TARSKI:def_4; consider x being Element of X such that A2: ( Y = x . O & x in L ) by A1; [x,z] in O by A1, A2, RELAT_1:169; hence z in | L by A2, RELAT_1:def_13; ::_thesis: verum end; thus | L c= union { (x . O) where x is Element of X : x in L } ::_thesis: verum proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in | L or z in union { (x . O) where x is Element of X : x in L } ) assume z in | L ; ::_thesis: z in union { (x . O) where x is Element of X : x in L } then consider y being set such that A3: ( [y,z] in O & y in L ) by RELAT_1:def_13; reconsider y = y as Element of X by A3; ( z in y . O & y . O in { (x . O) where x is Element of X : x in L } ) by A3, RELAT_1:169; hence z in union { (x . O) where x is Element of X : x in L } by TARSKI:def_4; ::_thesis: verum end; end; hence for b1 being List of X holds ( b1 = | L iff b1 = union { (x . O) where x is Element of X : x in L } ) ; ::_thesis: verum end; funcL \& O -> List of X equals :: MMLQUERY:def 3 meet { (x . O) where x is Element of X : x in L } ; coherence meet { (x . O) where x is Element of X : x in L } is List of X proof meet { (x . O) where x is Element of X : x in L } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet { (x . O) where x is Element of X : x in L } or z in X ) assume A1: z in meet { (x . O) where x is Element of X : x in L } ; ::_thesis: z in X then { (x . O) where x is Element of X : x in L } <> {} by SETFAM_1:def_1; then consider Y being set such that A2: Y in { (x . O) where x is Element of X : x in L } by XBOOLE_0:def_1; consider x being Element of X such that A3: ( Y = x . O & x in L ) by A2; z in x . O by A1, A2, A3, SETFAM_1:def_1; hence z in X ; ::_thesis: verum end; hence meet { (x . O) where x is Element of X : x in L } is List of X ; ::_thesis: verum end; funcL WHERE O -> List of X equals :: MMLQUERY:def 4 { x where x is Element of X : ex y being Element of X st ( x,y in O & x in L ) } ; coherence { x where x is Element of X : ex y being Element of X st ( x,y in O & x in L ) } is List of X proof { x where x is Element of X : ex y being Element of X st ( x,y in O & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ex y being Element of X st ( x,y in O & x in L ) } or z in X ) assume z in { x where x is Element of X : ex y being Element of X st ( x,y in O & x in L ) } ; ::_thesis: z in X then consider x being Element of X such that A1: ( z = x & ex y being Element of X st ( x,y in O & x in L ) ) ; thus z in X by A1; ::_thesis: verum end; hence { x where x is Element of X : ex y being Element of X st ( x,y in O & x in L ) } is List of X ; ::_thesis: verum end; let O2 be Operation of X; funcL WHEREeq (O,O2) -> List of X equals :: MMLQUERY:def 5 { x where x is Element of X : ( card (x . O) = card (x . O2) & x in L ) } ; coherence { x where x is Element of X : ( card (x . O) = card (x . O2) & x in L ) } is List of X proof { x where x is Element of X : ( card (x . O) = card (x . O2) & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( card (x . O) = card (x . O2) & x in L ) } or z in X ) assume z in { x where x is Element of X : ( card (x . O) = card (x . O2) & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & card (x . O) = card (x . O2) & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( card (x . O) = card (x . O2) & x in L ) } is List of X ; ::_thesis: verum end; funcL WHEREle (O,O2) -> List of X equals :: MMLQUERY:def 6 { x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L ) } ; coherence { x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L ) } is List of X proof { x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L ) } or z in X ) assume z in { x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & card (x . O) c= card (x . O2) & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L ) } is List of X ; ::_thesis: verum end; funcL WHEREge (O,O2) -> List of X equals :: MMLQUERY:def 7 { x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L ) } ; coherence { x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L ) } is List of X proof { x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L ) } or z in X ) assume z in { x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & card (x . O2) c= card (x . O) & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L ) } is List of X ; ::_thesis: verum end; funcL WHERElt (O,O2) -> List of X equals :: MMLQUERY:def 8 { x where x is Element of X : ( card (x . O) in card (x . O2) & x in L ) } ; coherence { x where x is Element of X : ( card (x . O) in card (x . O2) & x in L ) } is List of X proof { x where x is Element of X : ( card (x . O) in card (x . O2) & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( card (x . O) in card (x . O2) & x in L ) } or z in X ) assume z in { x where x is Element of X : ( card (x . O) in card (x . O2) & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & card (x . O) in card (x . O2) & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( card (x . O) in card (x . O2) & x in L ) } is List of X ; ::_thesis: verum end; funcL WHEREgt (O,O2) -> List of X equals :: MMLQUERY:def 9 { x where x is Element of X : ( card (x . O2) in card (x . O) & x in L ) } ; coherence { x where x is Element of X : ( card (x . O2) in card (x . O) & x in L ) } is List of X proof { x where x is Element of X : ( card (x . O2) in card (x . O) & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( card (x . O2) in card (x . O) & x in L ) } or z in X ) assume z in { x where x is Element of X : ( card (x . O2) in card (x . O) & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & card (x . O2) in card (x . O) & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( card (x . O2) in card (x . O) & x in L ) } is List of X ; ::_thesis: verum end; end; :: deftheorem defines | MMLQUERY:def_2_:_ for X being set for O being Operation of X for L being List of X holds L | O = union { (x . O) where x is Element of X : x in L } ; :: deftheorem defines \& MMLQUERY:def_3_:_ for X being set for O being Operation of X for L being List of X holds L \& O = meet { (x . O) where x is Element of X : x in L } ; :: deftheorem defines WHERE MMLQUERY:def_4_:_ for X being set for O being Operation of X for L being List of X holds L WHERE O = { x where x is Element of X : ex y being Element of X st ( x,y in O & x in L ) } ; :: deftheorem defines WHEREeq MMLQUERY:def_5_:_ for X being set for O being Operation of X for L being List of X for O2 being Operation of X holds L WHEREeq (O,O2) = { x where x is Element of X : ( card (x . O) = card (x . O2) & x in L ) } ; :: deftheorem defines WHEREle MMLQUERY:def_6_:_ for X being set for O being Operation of X for L being List of X for O2 being Operation of X holds L WHEREle (O,O2) = { x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L ) } ; :: deftheorem defines WHEREge MMLQUERY:def_7_:_ for X being set for O being Operation of X for L being List of X for O2 being Operation of X holds L WHEREge (O,O2) = { x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L ) } ; :: deftheorem defines WHERElt MMLQUERY:def_8_:_ for X being set for O being Operation of X for L being List of X for O2 being Operation of X holds L WHERElt (O,O2) = { x where x is Element of X : ( card (x . O) in card (x . O2) & x in L ) } ; :: deftheorem defines WHEREgt MMLQUERY:def_9_:_ for X being set for O being Operation of X for L being List of X for O2 being Operation of X holds L WHEREgt (O,O2) = { x where x is Element of X : ( card (x . O2) in card (x . O) & x in L ) } ; definition let X be set ; let L be List of X; let O be Operation of X; let n be Nat; funcL WHEREeq (O,n) -> List of X equals :: MMLQUERY:def 10 { x where x is Element of X : ( card (x . O) = n & x in L ) } ; coherence { x where x is Element of X : ( card (x . O) = n & x in L ) } is List of X proof { x where x is Element of X : ( card (x . O) = n & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( card (x . O) = n & x in L ) } or z in X ) assume z in { x where x is Element of X : ( card (x . O) = n & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & card (x . O) = n & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( card (x . O) = n & x in L ) } is List of X ; ::_thesis: verum end; funcL WHEREle (O,n) -> List of X equals :: MMLQUERY:def 11 { x where x is Element of X : ( card (x . O) c= n & x in L ) } ; coherence { x where x is Element of X : ( card (x . O) c= n & x in L ) } is List of X proof { x where x is Element of X : ( card (x . O) c= n & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( card (x . O) c= n & x in L ) } or z in X ) assume z in { x where x is Element of X : ( card (x . O) c= n & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & card (x . O) c= n & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( card (x . O) c= n & x in L ) } is List of X ; ::_thesis: verum end; funcL WHEREge (O,n) -> List of X equals :: MMLQUERY:def 12 { x where x is Element of X : ( n c= card (x . O) & x in L ) } ; coherence { x where x is Element of X : ( n c= card (x . O) & x in L ) } is List of X proof { x where x is Element of X : ( n c= card (x . O) & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( n c= card (x . O) & x in L ) } or z in X ) assume z in { x where x is Element of X : ( n c= card (x . O) & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & n c= card (x . O) & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( n c= card (x . O) & x in L ) } is List of X ; ::_thesis: verum end; funcL WHERElt (O,n) -> List of X equals :: MMLQUERY:def 13 { x where x is Element of X : ( card (x . O) in n & x in L ) } ; coherence { x where x is Element of X : ( card (x . O) in n & x in L ) } is List of X proof { x where x is Element of X : ( card (x . O) in n & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( card (x . O) in n & x in L ) } or z in X ) assume z in { x where x is Element of X : ( card (x . O) in n & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & card (x . O) in n & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( card (x . O) in n & x in L ) } is List of X ; ::_thesis: verum end; funcL WHEREgt (O,n) -> List of X equals :: MMLQUERY:def 14 { x where x is Element of X : ( n in card (x . O) & x in L ) } ; coherence { x where x is Element of X : ( n in card (x . O) & x in L ) } is List of X proof { x where x is Element of X : ( n in card (x . O) & x in L ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( n in card (x . O) & x in L ) } or z in X ) assume z in { x where x is Element of X : ( n in card (x . O) & x in L ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & n in card (x . O) & x in L ) ; hence z in X ; ::_thesis: verum end; hence { x where x is Element of X : ( n in card (x . O) & x in L ) } is List of X ; ::_thesis: verum end; end; :: deftheorem defines WHEREeq MMLQUERY:def_10_:_ for X being set for L being List of X for O being Operation of X for n being Nat holds L WHEREeq (O,n) = { x where x is Element of X : ( card (x . O) = n & x in L ) } ; :: deftheorem defines WHEREle MMLQUERY:def_11_:_ for X being set for L being List of X for O being Operation of X for n being Nat holds L WHEREle (O,n) = { x where x is Element of X : ( card (x . O) c= n & x in L ) } ; :: deftheorem defines WHEREge MMLQUERY:def_12_:_ for X being set for L being List of X for O being Operation of X for n being Nat holds L WHEREge (O,n) = { x where x is Element of X : ( n c= card (x . O) & x in L ) } ; :: deftheorem defines WHERElt MMLQUERY:def_13_:_ for X being set for L being List of X for O being Operation of X for n being Nat holds L WHERElt (O,n) = { x where x is Element of X : ( card (x . O) in n & x in L ) } ; :: deftheorem defines WHEREgt MMLQUERY:def_14_:_ for X being set for L being List of X for O being Operation of X for n being Nat holds L WHEREgt (O,n) = { x where x is Element of X : ( n in card (x . O) & x in L ) } ; theorem ThW: :: MMLQUERY:3 for X being set for L being List of X for x being Element of X for O being Operation of X holds ( x in L WHERE O iff ( x in L & x . O <> {} ) ) proof let X be set ; ::_thesis: for L being List of X for x being Element of X for O being Operation of X holds ( x in L WHERE O iff ( x in L & x . O <> {} ) ) let L be List of X; ::_thesis: for x being Element of X for O being Operation of X holds ( x in L WHERE O iff ( x in L & x . O <> {} ) ) let x be Element of X; ::_thesis: for O being Operation of X holds ( x in L WHERE O iff ( x in L & x . O <> {} ) ) let O be Operation of X; ::_thesis: ( x in L WHERE O iff ( x in L & x . O <> {} ) ) hereby ::_thesis: ( x in L & x . O <> {} implies x in L WHERE O ) assume x in L WHERE O ; ::_thesis: ( x in L & x . O <> {} ) then consider y being Element of X such that A1: ( x = y & ex a being Element of X st ( y,a in O & y in L ) ) ; thus ( x in L & x . O <> {} ) by A1, Th0; ::_thesis: verum end; assume A3: ( x in L & x . O <> {} ) ; ::_thesis: x in L WHERE O set y = the Element of x . O; the Element of x . O in x . O by A3; then reconsider y = the Element of x . O as Element of X ; x,y in O by A3, Th0; hence x in L WHERE O by A3; ::_thesis: verum end; theorem Th56: :: MMLQUERY:4 for X being set for L being List of X for O being Operation of X holds L WHERE O c= L proof let X be set ; ::_thesis: for L being List of X for O being Operation of X holds L WHERE O c= L let L be List of X; ::_thesis: for O being Operation of X holds L WHERE O c= L let O be Operation of X; ::_thesis: L WHERE O c= L let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE O or z in L ) thus ( not z in L WHERE O or z in L ) by ThW; ::_thesis: verum end; theorem :: MMLQUERY:5 for X being set for L being List of X for O being Operation of X st L c= dom O holds L WHERE O = L proof let X be set ; ::_thesis: for L being List of X for O being Operation of X st L c= dom O holds L WHERE O = L let L be List of X; ::_thesis: for O being Operation of X st L c= dom O holds L WHERE O = L let O be Operation of X; ::_thesis: ( L c= dom O implies L WHERE O = L ) assume A1: L c= dom O ; ::_thesis: L WHERE O = L thus L WHERE O c= L by Th56; :: according to XBOOLE_0:def_10 ::_thesis: L c= L WHERE O let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L or z in L WHERE O ) assume A2: z in L ; ::_thesis: z in L WHERE O then reconsider z = z as Element of X ; z . O <> {} by A1, A2, RELAT_1:170; hence z in L WHERE O by A2, ThW; ::_thesis: verum end; theorem Th26: :: MMLQUERY:6 for X being set for L1, L2 being List of X for O being Operation of X for n being Nat st n <> 0 & L1 c= L2 holds L1 WHEREge (O,n) c= L2 WHERE O proof let X be set ; ::_thesis: for L1, L2 being List of X for O being Operation of X for n being Nat st n <> 0 & L1 c= L2 holds L1 WHEREge (O,n) c= L2 WHERE O let L1, L2 be List of X; ::_thesis: for O being Operation of X for n being Nat st n <> 0 & L1 c= L2 holds L1 WHEREge (O,n) c= L2 WHERE O let O be Operation of X; ::_thesis: for n being Nat st n <> 0 & L1 c= L2 holds L1 WHEREge (O,n) c= L2 WHERE O let n be Nat; ::_thesis: ( n <> 0 & L1 c= L2 implies L1 WHEREge (O,n) c= L2 WHERE O ) assume A1: ( n <> 0 & L1 c= L2 ) ; ::_thesis: L1 WHEREge (O,n) c= L2 WHERE O let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREge (O,n) or z in L2 WHERE O ) assume z in L1 WHEREge (O,n) ; ::_thesis: z in L2 WHERE O then consider x being Element of X such that A2: ( z = x & n c= card (x . O) & x in L1 ) ; x . O <> {} by A1, A2; hence z in L2 WHERE O by A1, A2, ThW; ::_thesis: verum end; theorem :: MMLQUERY:7 for X being set for L being List of X for O being Operation of X holds L WHEREge (O,1) = L WHERE O proof let X be set ; ::_thesis: for L being List of X for O being Operation of X holds L WHEREge (O,1) = L WHERE O let L be List of X; ::_thesis: for O being Operation of X holds L WHEREge (O,1) = L WHERE O let O be Operation of X; ::_thesis: L WHEREge (O,1) = L WHERE O thus L WHEREge (O,1) c= L WHERE O by Th26; :: according to XBOOLE_0:def_10 ::_thesis: L WHERE O c= L WHEREge (O,1) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE O or z in L WHEREge (O,1) ) assume A1: z in L WHERE O ; ::_thesis: z in L WHEREge (O,1) then reconsider z = z as Element of X ; A2: ( z . O <> {} & z in L ) by A1, ThW; then succ 0 c= card (z . O) by ORDINAL1:21, ORDINAL3:8; hence z in L WHEREge (O,1) by A2; ::_thesis: verum end; theorem Th27: :: MMLQUERY:8 for X being set for L1, L2 being List of X for O being Operation of X for n being Nat st L1 c= L2 holds L1 WHEREgt (O,n) c= L2 WHERE O proof let X be set ; ::_thesis: for L1, L2 being List of X for O being Operation of X for n being Nat st L1 c= L2 holds L1 WHEREgt (O,n) c= L2 WHERE O let L1, L2 be List of X; ::_thesis: for O being Operation of X for n being Nat st L1 c= L2 holds L1 WHEREgt (O,n) c= L2 WHERE O let O be Operation of X; ::_thesis: for n being Nat st L1 c= L2 holds L1 WHEREgt (O,n) c= L2 WHERE O let n be Nat; ::_thesis: ( L1 c= L2 implies L1 WHEREgt (O,n) c= L2 WHERE O ) assume A1: L1 c= L2 ; ::_thesis: L1 WHEREgt (O,n) c= L2 WHERE O let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREgt (O,n) or z in L2 WHERE O ) assume z in L1 WHEREgt (O,n) ; ::_thesis: z in L2 WHERE O then consider x being Element of X such that A2: ( z = x & n in card (x . O) & x in L1 ) ; x . O <> {} by A2; hence z in L2 WHERE O by A1, A2, ThW; ::_thesis: verum end; theorem :: MMLQUERY:9 for X being set for L being List of X for O being Operation of X holds L WHEREgt (O,0) = L WHERE O proof let X be set ; ::_thesis: for L being List of X for O being Operation of X holds L WHEREgt (O,0) = L WHERE O let L be List of X; ::_thesis: for O being Operation of X holds L WHEREgt (O,0) = L WHERE O let O be Operation of X; ::_thesis: L WHEREgt (O,0) = L WHERE O thus L WHEREgt (O,0) c= L WHERE O by Th27; :: according to XBOOLE_0:def_10 ::_thesis: L WHERE O c= L WHEREgt (O,0) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE O or z in L WHEREgt (O,0) ) assume A1: z in L WHERE O ; ::_thesis: z in L WHEREgt (O,0) then reconsider z = z as Element of X ; A2: ( z . O <> {} & z in L ) by A1, ThW; then 0 in card (z . O) by ORDINAL3:8; hence z in L WHEREgt (O,0) by A2; ::_thesis: verum end; theorem :: MMLQUERY:10 for X being set for L1, L2 being List of X for O being Operation of X for n being Nat st n <> 0 & L1 c= L2 holds L1 WHEREeq (O,n) c= L2 WHERE O proof let X be set ; ::_thesis: for L1, L2 being List of X for O being Operation of X for n being Nat st n <> 0 & L1 c= L2 holds L1 WHEREeq (O,n) c= L2 WHERE O let L1, L2 be List of X; ::_thesis: for O being Operation of X for n being Nat st n <> 0 & L1 c= L2 holds L1 WHEREeq (O,n) c= L2 WHERE O let O be Operation of X; ::_thesis: for n being Nat st n <> 0 & L1 c= L2 holds L1 WHEREeq (O,n) c= L2 WHERE O let n be Nat; ::_thesis: ( n <> 0 & L1 c= L2 implies L1 WHEREeq (O,n) c= L2 WHERE O ) assume A1: ( n <> 0 & L1 c= L2 ) ; ::_thesis: L1 WHEREeq (O,n) c= L2 WHERE O let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREeq (O,n) or z in L2 WHERE O ) assume z in L1 WHEREeq (O,n) ; ::_thesis: z in L2 WHERE O then consider x being Element of X such that A2: ( z = x & card (x . O) = n & x in L1 ) ; x . O <> {} by A1, A2; hence z in L2 WHERE O by A1, A2, ThW; ::_thesis: verum end; theorem :: MMLQUERY:11 for X being set for L being List of X for O being Operation of X for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n) proof let X be set ; ::_thesis: for L being List of X for O being Operation of X for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n) let L be List of X; ::_thesis: for O being Operation of X for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n) let O be Operation of X; ::_thesis: for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n) let n be Nat; ::_thesis: L WHEREge (O,(n + 1)) = L WHEREgt (O,n) thus L WHEREge (O,(n + 1)) c= L WHEREgt (O,n) :: according to XBOOLE_0:def_10 ::_thesis: L WHEREgt (O,n) c= L WHEREge (O,(n + 1)) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREge (O,(n + 1)) or z in L WHEREgt (O,n) ) assume z in L WHEREge (O,(n + 1)) ; ::_thesis: z in L WHEREgt (O,n) then consider x being Element of X such that A2: ( z = x & n + 1 c= card (x . O) & x in L ) ; n + 1 = succ n by NAT_1:38; then n in card (x . O) by A2, ORDINAL1:21; hence z in L WHEREgt (O,n) by A2; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREgt (O,n) or z in L WHEREge (O,(n + 1)) ) assume z in L WHEREgt (O,n) ; ::_thesis: z in L WHEREge (O,(n + 1)) then consider x being Element of X such that A2: ( z = x & n in card (x . O) & x in L ) ; n + 1 = succ n by NAT_1:38; then n + 1 c= card (x . O) by A2, ORDINAL1:21; hence z in L WHEREge (O,(n + 1)) by A2; ::_thesis: verum end; theorem :: MMLQUERY:12 for X being set for L being List of X for O being Operation of X for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1)) proof let X be set ; ::_thesis: for L being List of X for O being Operation of X for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1)) let L be List of X; ::_thesis: for O being Operation of X for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1)) let O be Operation of X; ::_thesis: for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1)) let n be Nat; ::_thesis: L WHEREle (O,n) = L WHERElt (O,(n + 1)) thus L WHEREle (O,n) c= L WHERElt (O,(n + 1)) :: according to XBOOLE_0:def_10 ::_thesis: L WHERElt (O,(n + 1)) c= L WHEREle (O,n) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREle (O,n) or z in L WHERElt (O,(n + 1)) ) assume z in L WHEREle (O,n) ; ::_thesis: z in L WHERElt (O,(n + 1)) then consider x being Element of X such that A2: ( z = x & card (x . O) c= n & x in L ) ; n + 1 = succ n by NAT_1:38; then card (x . O) in n + 1 by A2, ORDINAL1:22; hence z in L WHERElt (O,(n + 1)) by A2; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERElt (O,(n + 1)) or z in L WHEREle (O,n) ) assume z in L WHERElt (O,(n + 1)) ; ::_thesis: z in L WHEREle (O,n) then consider x being Element of X such that A2: ( z = x & card (x . O) in n + 1 & x in L ) ; n + 1 = succ n by NAT_1:38; then card (x . O) c= n by A2, ORDINAL1:22; hence z in L WHEREle (O,n) by A2; ::_thesis: verum end; theorem :: MMLQUERY:13 for X being set for L1, L2 being List of X for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREge (O1,m) c= L2 WHEREge (O2,n) proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREge (O1,m) c= L2 WHEREge (O2,n) let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREge (O1,m) c= L2 WHEREge (O2,n) let O1, O2 be Operation of X; ::_thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREge (O1,m) c= L2 WHEREge (O2,n) let n, m be Nat; ::_thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREge (O1,m) c= L2 WHEREge (O2,n) ) assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 WHEREge (O1,m) c= L2 WHEREge (O2,n) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREge (O1,m) or z in L2 WHEREge (O2,n) ) assume z in L1 WHEREge (O1,m) ; ::_thesis: z in L2 WHEREge (O2,n) then consider x being Element of X such that A2: ( z = x & m c= card (x . O1) & x in L1 ) ; ( n c= m & x . O1 c= x . O2 ) by A1, Th9, NAT_1:39; then ( n c= card (x . O1) & card (x . O1) c= card (x . O2) ) by A2, CARD_1:11, XBOOLE_1:1; then n c= card (x . O2) by XBOOLE_1:1; hence z in L2 WHEREge (O2,n) by A1, A2; ::_thesis: verum end; theorem :: MMLQUERY:14 for X being set for L1, L2 being List of X for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n) proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n) let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n) let O1, O2 be Operation of X; ::_thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n) let n, m be Nat; ::_thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n) ) assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREgt (O1,m) or z in L2 WHEREgt (O2,n) ) assume z in L1 WHEREgt (O1,m) ; ::_thesis: z in L2 WHEREgt (O2,n) then consider x being Element of X such that A2: ( z = x & m in card (x . O1) & x in L1 ) ; ( n c= m & card (x . O1) c= card (x . O2) ) by A1, CARD_1:11, NAT_1:39, Th9; then n in card (x . O2) by A2, ORDINAL1:12; hence z in L2 WHEREgt (O2,n) by A1, A2; ::_thesis: verum end; theorem :: MMLQUERY:15 for X being set for L1, L2 being List of X for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREle (O2,n) c= L2 WHEREle (O1,m) proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREle (O2,n) c= L2 WHEREle (O1,m) let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREle (O2,n) c= L2 WHEREle (O1,m) let O1, O2 be Operation of X; ::_thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHEREle (O2,n) c= L2 WHEREle (O1,m) let n, m be Nat; ::_thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREle (O2,n) c= L2 WHEREle (O1,m) ) assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 WHEREle (O2,n) c= L2 WHEREle (O1,m) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREle (O2,n) or z in L2 WHEREle (O1,m) ) assume z in L1 WHEREle (O2,n) ; ::_thesis: z in L2 WHEREle (O1,m) then consider x being Element of X such that A2: ( z = x & card (x . O2) c= n & x in L1 ) ; ( n c= m & x . O1 c= x . O2 ) by A1, Th9, NAT_1:39; then ( card (x . O1) c= card (x . O2) & card (x . O2) c= m ) by A2, CARD_1:11, XBOOLE_1:1; then card (x . O1) c= m by XBOOLE_1:1; hence z in L2 WHEREle (O1,m) by A1, A2; ::_thesis: verum end; theorem :: MMLQUERY:16 for X being set for L1, L2 being List of X for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHERElt (O2,n) c= L2 WHERElt (O1,m) proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHERElt (O2,n) c= L2 WHERElt (O1,m) let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHERElt (O2,n) c= L2 WHERElt (O1,m) let O1, O2 be Operation of X; ::_thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds L1 WHERElt (O2,n) c= L2 WHERElt (O1,m) let n, m be Nat; ::_thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHERElt (O2,n) c= L2 WHERElt (O1,m) ) assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 WHERElt (O2,n) c= L2 WHERElt (O1,m) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHERElt (O2,n) or z in L2 WHERElt (O1,m) ) assume z in L1 WHERElt (O2,n) ; ::_thesis: z in L2 WHERElt (O1,m) then consider x being Element of X such that A2: ( z = x & card (x . O2) in n & x in L1 ) ; ( n c= m & card (x . O1) c= card (x . O2) ) by A1, CARD_1:11, NAT_1:39, Th9; then card (x . O1) in m by A2, ORDINAL1:12; hence z in L2 WHERElt (O1,m) by A1, A2; ::_thesis: verum end; theorem :: MMLQUERY:17 for X being set for L1, L2 being List of X for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1) proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1) let L1, L2 be List of X; ::_thesis: for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1) let O1, O2, O, O3 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1) ) assume Z0: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; ::_thesis: L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREge (O,O2) or z in L2 WHEREge (O3,O1) ) assume z in L1 WHEREge (O,O2) ; ::_thesis: z in L2 WHEREge (O3,O1) then consider x being Element of X such that A1: ( z = x & card (x . O2) c= card (x . O) & x in L1 ) ; A2: ( card (x . O1) c= card (x . O2) & card (x . O) c= card (x . O3) ) by Z0, Th9, CARD_1:11; then card (x . O1) c= card (x . O) by A1, XBOOLE_1:1; then card (x . O1) c= card (x . O3) by A2, XBOOLE_1:1; hence z in L2 WHEREge (O3,O1) by A1, Z0; ::_thesis: verum end; theorem :: MMLQUERY:18 for X being set for L1, L2 being List of X for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1) proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1) let L1, L2 be List of X; ::_thesis: for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1) let O1, O2, O, O3 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1) ) assume Z0: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; ::_thesis: L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREgt (O,O2) or z in L2 WHEREgt (O3,O1) ) assume z in L1 WHEREgt (O,O2) ; ::_thesis: z in L2 WHEREgt (O3,O1) then consider x being Element of X such that A1: ( z = x & card (x . O2) in card (x . O) & x in L1 ) ; ( x . O1 c= x . O2 & x . O c= x . O3 ) by Z0, Th9; then ( card (x . O1) in card (x . O) & card (x . O) c= card (x . O3) ) by A1, CARD_1:11, ORDINAL1:12; hence z in L2 WHEREgt (O3,O1) by A1, Z0; ::_thesis: verum end; theorem :: MMLQUERY:19 for X being set for L1, L2 being List of X for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2) proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2) let L1, L2 be List of X; ::_thesis: for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2) let O1, O2, O, O3 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2) ) assume Z0: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; ::_thesis: L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREle (O3,O1) or z in L2 WHEREle (O,O2) ) assume z in L1 WHEREle (O3,O1) ; ::_thesis: z in L2 WHEREle (O,O2) then consider x being Element of X such that A1: ( z = x & card (x . O3) c= card (x . O1) & x in L1 ) ; A2: ( card (x . O1) c= card (x . O2) & card (x . O) c= card (x . O3) ) by Z0, Th9, CARD_1:11; then card (x . O3) c= card (x . O2) by A1, XBOOLE_1:1; then card (x . O) c= card (x . O2) by A2, XBOOLE_1:1; hence z in L2 WHEREle (O,O2) by A1, Z0; ::_thesis: verum end; theorem :: MMLQUERY:20 for X being set for L1, L2 being List of X for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2) proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2) let L1, L2 be List of X; ::_thesis: for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2) let O1, O2, O, O3 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2) ) assume Z0: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; ::_thesis: L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHERElt (O3,O1) or z in L2 WHERElt (O,O2) ) assume z in L1 WHERElt (O3,O1) ; ::_thesis: z in L2 WHERElt (O,O2) then consider x being Element of X such that A1: ( z = x & card (x . O3) in card (x . O1) & x in L1 ) ; ( card (x . O1) c= card (x . O2) & card (x . O) c= card (x . O3) ) by Z0, Th9, CARD_1:11; then card (x . O) in card (x . O2) by A1, ORDINAL1:12; hence z in L2 WHERElt (O,O2) by A1, Z0; ::_thesis: verum end; theorem :: MMLQUERY:21 for X being set for L being List of X for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O proof let X be set ; ::_thesis: for L being List of X for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O let L be List of X; ::_thesis: for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O let O, O1 be Operation of X; ::_thesis: L WHEREgt (O,O1) c= L WHERE O let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREgt (O,O1) or z in L WHERE O ) assume z in L WHEREgt (O,O1) ; ::_thesis: z in L WHERE O then consider x being Element of X such that A2: ( z = x & card (x . O1) in card (x . O) & x in L ) ; x . O <> {} by A2; hence z in L WHERE O by A2, ThW; ::_thesis: verum end; theorem :: MMLQUERY:22 for X being set for L1, L2 being List of X for O1, O2 being Operation of X st O1 c= O2 & L1 c= L2 holds L1 WHERE O1 c= L2 WHERE O2 proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2 being Operation of X st O1 c= O2 & L1 c= L2 holds L1 WHERE O1 c= L2 WHERE O2 let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X st O1 c= O2 & L1 c= L2 holds L1 WHERE O1 c= L2 WHERE O2 let O1, O2 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 implies L1 WHERE O1 c= L2 WHERE O2 ) assume A1: ( O1 c= O2 & L1 c= L2 ) ; ::_thesis: L1 WHERE O1 c= L2 WHERE O2 let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHERE O1 or z in L2 WHERE O2 ) assume A2: z in L1 WHERE O1 ; ::_thesis: z in L2 WHERE O2 then reconsider z = z as Element of X ; A3: ( z . O1 <> {} & z in L1 ) by A2, ThW; z . O1 c= z . O2 by A1, Th9; then z . O2 <> {} by A3; hence z in L2 WHERE O2 by A1, A3, ThW; ::_thesis: verum end; theorem Th1: :: MMLQUERY:23 for X being set for L being List of X for O being Operation of X for a being Element of X holds ( a in L | O iff ex b being Element of X st ( a in b . O & b in L ) ) proof let X be set ; ::_thesis: for L being List of X for O being Operation of X for a being Element of X holds ( a in L | O iff ex b being Element of X st ( a in b . O & b in L ) ) let L be List of X; ::_thesis: for O being Operation of X for a being Element of X holds ( a in L | O iff ex b being Element of X st ( a in b . O & b in L ) ) let O be Operation of X; ::_thesis: for a being Element of X holds ( a in L | O iff ex b being Element of X st ( a in b . O & b in L ) ) let a be Element of X; ::_thesis: ( a in L | O iff ex b being Element of X st ( a in b . O & b in L ) ) hereby ::_thesis: ( ex b being Element of X st ( a in b . O & b in L ) implies a in L | O ) assume a in L | O ; ::_thesis: ex b being Element of X st ( a in b . O & b in L ) then consider b being set such that A1: ( [b,a] in O & b in L ) by RELAT_1:def_13; reconsider b = b as Element of X by A1; take b = b; ::_thesis: ( a in b . O & b in L ) thus a in b . O by A1, RELAT_1:169; ::_thesis: b in L thus b in L by A1; ::_thesis: verum end; given b being Element of X such that A2: ( a in b . O & b in L ) ; ::_thesis: a in L | O [b,a] in O by A2, RELAT_1:169; hence a in L | O by A2, RELAT_1:def_13; ::_thesis: verum end; notation let X be set ; let A, B be List of X; synonym A AND B for X /\ A; synonym A OR B for X \/ A; synonym A BUTNOT B for X \ A; end; definition let X be set ; let A, B be List of X; :: original: AND redefine funcA AND B -> List of X; coherence B AND is List of X proof A /\ B is Subset of X ; hence B AND is List of X ; ::_thesis: verum end; :: original: OR redefine funcA OR B -> List of X; coherence B OR is List of X proof A \/ B is Subset of X ; hence B OR is List of X ; ::_thesis: verum end; :: original: BUTNOT redefine funcA BUTNOT B -> List of X; coherence B BUTNOT is List of X proof A \ B is Subset of X ; hence B BUTNOT is List of X ; ::_thesis: verum end; end; theorem Th17: :: MMLQUERY:24 for X being set for L1, L2 being List of X for O being Operation of X st L1 <> {} & L2 <> {} holds (L1 OR L2) \& O = (L1 \& O) AND (L2 \& O) proof let X be set ; ::_thesis: for L1, L2 being List of X for O being Operation of X st L1 <> {} & L2 <> {} holds (L1 OR L2) \& O = (L1 \& O) AND (L2 \& O) let L1, L2 be List of X; ::_thesis: for O being Operation of X st L1 <> {} & L2 <> {} holds (L1 OR L2) \& O = (L1 \& O) AND (L2 \& O) let O be Operation of X; ::_thesis: ( L1 <> {} & L2 <> {} implies (L1 OR L2) \& O = (L1 \& O) AND (L2 \& O) ) assume A0: ( L1 <> {} & L2 <> {} ) ; ::_thesis: (L1 OR L2) \& O = (L1 \& O) AND (L2 \& O) thus (L1 OR L2) \& O c= (L1 \& O) AND (L2 \& O) :: according to XBOOLE_0:def_10 ::_thesis: (L1 \& O) AND (L2 \& O) c= (L1 OR L2) \& O proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (L1 OR L2) \& O or z in (L1 \& O) AND (L2 \& O) ) assume A1: z in (L1 OR L2) \& O ; ::_thesis: z in (L1 \& O) AND (L2 \& O) now__::_thesis:_(__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1__}__holds_ z_in_Y_)_) set c = the Element of L1; the Element of L1 in L1 by A0; then reconsider c = the Element of L1 as Element of X ; c . O in { (x . O) where x is Element of X : x in L1 } by A0; hence { (x . O) where x is Element of X : x in L1 } <> {} ; ::_thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L1 } holds z in Y let Y be set ; ::_thesis: ( Y in { (x . O) where x is Element of X : x in L1 } implies z in Y ) assume Y in { (x . O) where x is Element of X : x in L1 } ; ::_thesis: z in Y then consider x being Element of X such that A3: ( Y = x . O & x in L1 ) ; x in L1 OR L2 by A3, XBOOLE_0:def_3; then Y in { (a . O) where a is Element of X : a in L1 OR L2 } by A3; hence z in Y by A1, SETFAM_1:def_1; ::_thesis: verum end; then A4: z in L1 \& O by SETFAM_1:def_1; now__::_thesis:_(__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L2__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L2__}__holds_ z_in_Y_)_) set c = the Element of L2; the Element of L2 in L2 by A0; then reconsider c = the Element of L2 as Element of X ; c . O in { (x . O) where x is Element of X : x in L2 } by A0; hence { (x . O) where x is Element of X : x in L2 } <> {} ; ::_thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L2 } holds z in Y let Y be set ; ::_thesis: ( Y in { (x . O) where x is Element of X : x in L2 } implies z in Y ) assume Y in { (x . O) where x is Element of X : x in L2 } ; ::_thesis: z in Y then consider x being Element of X such that A3: ( Y = x . O & x in L2 ) ; x in L1 OR L2 by A3, XBOOLE_0:def_3; then Y in { (a . O) where a is Element of X : a in L1 OR L2 } by A3; hence z in Y by A1, SETFAM_1:def_1; ::_thesis: verum end; then z in L2 \& O by SETFAM_1:def_1; hence z in (L1 \& O) AND (L2 \& O) by A4, XBOOLE_0:def_4; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (L1 \& O) AND (L2 \& O) or z in (L1 OR L2) \& O ) assume z in (L1 \& O) AND (L2 \& O) ; ::_thesis: z in (L1 OR L2) \& O then A5: ( z in L1 \& O & z in L2 \& O ) by XBOOLE_0:def_4; now__::_thesis:_(__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1_OR_L2__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1_OR_L2__}__holds_ z_in_Y_)_) set c = the Element of L2; the Element of L2 in L2 by A0; then reconsider c = the Element of L2 as Element of X ; c in L1 OR L2 by A0, XBOOLE_0:def_3; then c . O in { (x . O) where x is Element of X : x in L1 OR L2 } ; hence { (x . O) where x is Element of X : x in L1 OR L2 } <> {} ; ::_thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L1 OR L2 } holds z in Y let Y be set ; ::_thesis: ( Y in { (x . O) where x is Element of X : x in L1 OR L2 } implies z in Y ) assume Y in { (x . O) where x is Element of X : x in L1 OR L2 } ; ::_thesis: z in Y then consider x being Element of X such that A3: ( Y = x . O & x in L1 OR L2 ) ; ( x in L1 or x in L2 ) by A3, XBOOLE_0:def_3; then ( Y in { (a . O) where a is Element of X : a in L1 } or Y in { (b . O) where b is Element of X : b in L2 } ) by A3; hence z in Y by A5, SETFAM_1:def_1; ::_thesis: verum end; hence z in (L1 OR L2) \& O by SETFAM_1:def_1; ::_thesis: verum end; theorem :: MMLQUERY:25 for X being set for L1, L2 being List of X for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds L1 | O1 c= L2 | O2 proof let X be set ; ::_thesis: for L1, L2 being List of X for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds L1 | O1 c= L2 | O2 let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds L1 | O1 c= L2 | O2 let O1, O2 be Operation of X; ::_thesis: ( L1 c= L2 & O1 c= O2 implies L1 | O1 c= L2 | O2 ) assume ( L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 | O1 c= L2 | O2 then ( L1 | O1 c= L2 | O1 & L2 | O1 c= L2 | O2 ) by RELAT_1:123, RELAT_1:124; hence L1 | O1 c= L2 | O2 by XBOOLE_1:1; ::_thesis: verum end; theorem Th81: :: MMLQUERY:26 for X being set for L being List of X for O1, O2 being Operation of X st O1 c= O2 holds L \& O1 c= L \& O2 proof let X be set ; ::_thesis: for L being List of X for O1, O2 being Operation of X st O1 c= O2 holds L \& O1 c= L \& O2 let L be List of X; ::_thesis: for O1, O2 being Operation of X st O1 c= O2 holds L \& O1 c= L \& O2 let O1, O2 be Operation of X; ::_thesis: ( O1 c= O2 implies L \& O1 c= L \& O2 ) assume A1: O1 c= O2 ; ::_thesis: L \& O1 c= L \& O2 let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L \& O1 or z in L \& O2 ) assume A2: z in L \& O1 ; ::_thesis: z in L \& O2 then { (x . O1) where x is Element of X : x in L } <> {} by SETFAM_1:def_1; then consider Y being set such that A3: Y in { (x . O1) where x is Element of X : x in L } by XBOOLE_0:def_1; consider y being Element of X such that A4: ( Y = y . O1 & y in L ) by A3; A5: y . O2 in { (x . O2) where x is Element of X : x in L } by A4; now__::_thesis:_for_Y_being_set_st_Y_in__{__(x_._O2)_where_x_is_Element_of_X_:_x_in_L__}__holds_ z_in_Y let Y be set ; ::_thesis: ( Y in { (x . O2) where x is Element of X : x in L } implies z in Y ) assume Y in { (x . O2) where x is Element of X : x in L } ; ::_thesis: z in Y then consider a being Element of X such that A6: ( Y = a . O2 & a in L ) ; a . O1 in { (x . O1) where x is Element of X : x in L } by A6; then ( z in a . O1 & a . O1 c= Y ) by A1, A2, A6, Th9, SETFAM_1:def_1; hence z in Y ; ::_thesis: verum end; hence z in L \& O2 by A5, SETFAM_1:def_1; ::_thesis: verum end; theorem :: MMLQUERY:27 for X being set for L being List of X for O1, O2 being Operation of X holds L \& (O1 AND O2) = (L \& O1) AND (L \& O2) proof let X be set ; ::_thesis: for L being List of X for O1, O2 being Operation of X holds L \& (O1 AND O2) = (L \& O1) AND (L \& O2) let L be List of X; ::_thesis: for O1, O2 being Operation of X holds L \& (O1 AND O2) = (L \& O1) AND (L \& O2) let O1, O2 be Operation of X; ::_thesis: L \& (O1 AND O2) = (L \& O1) AND (L \& O2) ( L \& (O1 AND O2) c= L \& O1 & L \& (O1 AND O2) c= L \& O2 ) by XBOOLE_1:17, Th81; hence L \& (O1 AND O2) c= (L \& O1) AND (L \& O2) by XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: (L \& O1) AND (L \& O2) c= L \& (O1 AND O2) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (L \& O1) AND (L \& O2) or z in L \& (O1 AND O2) ) assume z in (L \& O1) AND (L \& O2) ; ::_thesis: z in L \& (O1 AND O2) then A5: ( z in L \& O1 & z in L \& O2 ) by XBOOLE_0:def_4; now__::_thesis:_(__{__(x_._(O1_AND_O2))_where_x_is_Element_of_X_:_x_in_L__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._(O1_AND_O2))_where_x_is_Element_of_X_:_x_in_L__}__holds_ z_in_Y_)_) set O = O1 AND O2; set c = the Element of L; { (x . O1) where x is Element of X : x in L } <> {} by A5, SETFAM_1:def_1; then consider c being set such that A1: c in { (x . O1) where x is Element of X : x in L } by XBOOLE_0:def_1; consider a being Element of X such that A2: ( c = a . O1 & a in L ) by A1; a . (O1 AND O2) in { (x . (O1 AND O2)) where x is Element of X : x in L } by A2; hence { (x . (O1 AND O2)) where x is Element of X : x in L } <> {} ; ::_thesis: for Y being set st Y in { (x . (O1 AND O2)) where x is Element of X : x in L } holds z in Y let Y be set ; ::_thesis: ( Y in { (x . (O1 AND O2)) where x is Element of X : x in L } implies z in Y ) assume Y in { (x . (O1 AND O2)) where x is Element of X : x in L } ; ::_thesis: z in Y then consider x being Element of X such that A3: ( Y = x . (O1 AND O2) & x in L ) ; A4: Y = (x . O1) AND (x . O2) by A3, RELSET_2:11; x . O1 in { (y . O1) where y is Element of X : y in L } by A3; then A6: z in x . O1 by A5, SETFAM_1:def_1; x . O2 in { (y . O2) where y is Element of X : y in L } by A3; then z in x . O2 by A5, SETFAM_1:def_1; hence z in Y by A4, A6, XBOOLE_0:def_4; ::_thesis: verum end; hence z in L \& (O1 AND O2) by SETFAM_1:def_1; ::_thesis: verum end; theorem :: MMLQUERY:28 for X being set for L1, L2 being List of X for O being Operation of X st L1 <> {} & L1 c= L2 holds L2 \& O c= L1 \& O proof let X be set ; ::_thesis: for L1, L2 being List of X for O being Operation of X st L1 <> {} & L1 c= L2 holds L2 \& O c= L1 \& O let L1, L2 be List of X; ::_thesis: for O being Operation of X st L1 <> {} & L1 c= L2 holds L2 \& O c= L1 \& O let O be Operation of X; ::_thesis: ( L1 <> {} & L1 c= L2 implies L2 \& O c= L1 \& O ) assume Z0: L1 <> {} ; ::_thesis: ( not L1 c= L2 or L2 \& O c= L1 \& O ) assume Z1: L1 c= L2 ; ::_thesis: L2 \& O c= L1 \& O let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L2 \& O or z in L1 \& O ) assume A0: z in L2 \& O ; ::_thesis: z in L1 \& O now__::_thesis:_(__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1__}__holds_ z_in_Y_)_) set c = the Element of L1; the Element of L1 in L1 by Z0; then reconsider c = the Element of L1 as Element of X ; c . O in { (x . O) where x is Element of X : x in L1 } by Z0; hence { (x . O) where x is Element of X : x in L1 } <> {} ; ::_thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L1 } holds z in Y let Y be set ; ::_thesis: ( Y in { (x . O) where x is Element of X : x in L1 } implies z in Y ) assume Y in { (x . O) where x is Element of X : x in L1 } ; ::_thesis: z in Y then consider x being Element of X such that A3: ( Y = x . O & x in L1 ) ; Y in { (a . O) where a is Element of X : a in L2 } by A3, Z1; hence z in Y by A0, SETFAM_1:def_1; ::_thesis: verum end; hence z in L1 \& O by SETFAM_1:def_1; ::_thesis: verum end; begin theorem Th3a: :: MMLQUERY:29 for X being set for O1, O2 being Operation of X st ( for x being Element of X holds x . O1 = x . O2 ) holds O1 = O2 proof let X be set ; ::_thesis: for O1, O2 being Operation of X st ( for x being Element of X holds x . O1 = x . O2 ) holds O1 = O2 let O1, O2 be Operation of X; ::_thesis: ( ( for x being Element of X holds x . O1 = x . O2 ) implies O1 = O2 ) assume Z0: for x being Element of X holds x . O1 = x . O2 ; ::_thesis: O1 = O2 let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in O1 or [a,b] in O2 ) & ( not [a,b] in O2 or [a,b] in O1 ) ) thus ( [a,b] in O1 implies [a,b] in O2 ) ::_thesis: ( not [a,b] in O2 or [a,b] in O1 ) proof assume A1: [a,b] in O1 ; ::_thesis: [a,b] in O2 reconsider a = a, b = b as Element of X by A1, ZFMISC_1:87; b in a . O1 by A1, RELAT_1:169; then b in a . O2 by Z0; hence [a,b] in O2 by RELAT_1:169; ::_thesis: verum end; assume A1: [a,b] in O2 ; ::_thesis: [a,b] in O1 then A2: ( a in X & b in X ) by ZFMISC_1:87; reconsider a = a, b = b as Element of X by A1, ZFMISC_1:87; reconsider L = {a} as Subset of X by A2, ZFMISC_1:31; b in a . O2 by A1, RELAT_1:169; then b in a . O1 by Z0; hence [a,b] in O1 by RELAT_1:169; ::_thesis: verum end; theorem Th3: :: MMLQUERY:30 for X being set for O1, O2 being Operation of X st ( for L being List of X holds L | O1 = L | O2 ) holds O1 = O2 proof let X be set ; ::_thesis: for O1, O2 being Operation of X st ( for L being List of X holds L | O1 = L | O2 ) holds O1 = O2 let O1, O2 be Operation of X; ::_thesis: ( ( for L being List of X holds L | O1 = L | O2 ) implies O1 = O2 ) assume Z0: for L being List of X holds L | O1 = L | O2 ; ::_thesis: O1 = O2 now__::_thesis:_for_x_being_Element_of_X_holds_x_._O1_=_x_._O2 let x be Element of X; ::_thesis: b1 . O1 = b1 . O2 percases ( X <> {} or X = {} ) ; suppose X <> {} ; ::_thesis: b1 . O1 = b1 . O2 then reconsider L = {x} as Subset of X by ZFMISC_1:31; thus x . O1 = L | O1 .= x . O2 by Z0 ; ::_thesis: verum end; suppose X = {} ; ::_thesis: b1 . O1 = b1 . O2 hence x . O1 = x . O2 ; ::_thesis: verum end; end; end; hence O1 = O2 by Th3a; ::_thesis: verum end; definition let X be set ; let O be Operation of X; func NOT O -> Operation of X means :DEFNOT: :: MMLQUERY:def 15 for L being List of X holds L | it = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ; existence ex b1 being Operation of X st for L being List of X holds L | b1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } proof defpred S1[ set , set ] means ( Im (O,\$1) = {} & \$2 = \$1 ); consider O1 being Relation such that A1: for a, b being set holds ( [a,b] in O1 iff ( a in X & b in X & S1[a,b] ) ) from RELAT_1:sch_1(); O1 c= [:X,X:] proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in O1 or [x,y] in [:X,X:] ) assume [x,y] in O1 ; ::_thesis: [x,y] in [:X,X:] then ( x in X & y in X ) by A1; hence [x,y] in [:X,X:] by ZFMISC_1:87; ::_thesis: verum end; then reconsider O1 = O1 as Operation of X ; take O1 ; ::_thesis: for L being List of X holds L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } let L be List of X; ::_thesis: L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } thus L | O1 c= union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } :: according to XBOOLE_0:def_10 ::_thesis: union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } c= L | O1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in L | O1 or a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) assume a in L | O1 ; ::_thesis: a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } then consider b being Element of X such that A2: ( a in b . O1 & b in L ) by Th1; [b,a] in O1 by A2, RELAT_1:169; then A3: ( a = b & b . O = {} ) by A1; then a in {b} by TARSKI:def_1; then A4: a in IFEQ ((b . O),{},{b},{}) by A3, FUNCOP_1:def_8; IFEQ ((b . O),{},{b},{}) in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } by A2; hence a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } by A4, TARSKI:def_4; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } or a in L | O1 ) assume a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ; ::_thesis: a in L | O1 then consider A being set such that A5: ( a in A & A in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) by TARSKI:def_4; consider x being Element of X such that A6: ( A = IFEQ ((x . O),{},{x},{}) & x in L ) by A5; A7: x . O = {} by A5, A6, FUNCOP_1:def_8; then A = {x} by A6, FUNCOP_1:def_8; then a = x by A5, TARSKI:def_1; then [x,a] in O1 by A1, A6, A7; hence a in L | O1 by A6, RELAT_1:def_13; ::_thesis: verum end; uniqueness for b1, b2 being Operation of X st ( for L being List of X holds L | b1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) & ( for L being List of X holds L | b2 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) holds b1 = b2 proof let O1, O2 be Operation of X; ::_thesis: ( ( for L being List of X holds L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) & ( for L being List of X holds L | O2 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) implies O1 = O2 ) assume that A1: for L being List of X holds L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } and A2: for L being List of X holds L | O2 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ; ::_thesis: O1 = O2 now__::_thesis:_for_L_being_List_of_X_holds_L_|_O1_=_L_|_O2 let L be List of X; ::_thesis: L | O1 = L | O2 thus L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } by A1 .= L | O2 by A2 ; ::_thesis: verum end; hence O1 = O2 by Th3; ::_thesis: verum end; end; :: deftheorem DEFNOT defines NOT MMLQUERY:def_15_:_ for X being set for O, b3 being Operation of X holds ( b3 = NOT O iff for L being List of X holds L | b3 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ); notation let X be set ; let O1, O2 be Operation of X; synonym O1 AND O2 for X /\ O1; synonym O1 OR O2 for X \/ O1; synonym O1 BUTNOT O2 for X \ O1; synonym O1 | O2 for X * O1; end; definition let X be set ; let O1, O2 be Operation of X; :: original: AND redefine funcO1 AND O2 -> Operation of X means :: MMLQUERY:def 16 for L being List of X holds L | it = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ; coherence O2 AND is Operation of X proof thus O1 /\ O2 is Subset of [:X,X:] ; ::_thesis: verum end; compatibility for b1 being Operation of X holds ( b1 = O2 AND iff for L being List of X holds L | b1 = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ) proof AA: for O being Operation of X st O = O2 AND holds for L being List of X holds L | O = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } proof let O be Operation of X; ::_thesis: ( O = O2 AND implies for L being List of X holds L | O = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ) assume A0: O = O1 /\ O2 ; ::_thesis: for L being List of X holds L | O = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } defpred S1[ set , set ] means ( [\$1,\$2] in O1 & [\$1,\$2] in O2 ); let L be List of X; ::_thesis: L | O = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } thus L | O c= union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } :: according to XBOOLE_0:def_10 ::_thesis: union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } c= L | O proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | O or z in union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ) assume z in L | O ; ::_thesis: z in union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } then consider y being set such that A2: ( [y,z] in O & y in L ) by RELAT_1:def_13; reconsider y = y, z = z as Element of X by A2, ZFMISC_1:87; ( [y,z] in O1 & [y,z] in O2 ) by A0, A2, XBOOLE_0:def_4; then ( z in y . O1 & z in y . O2 ) by RELAT_1:169; then ( z in (y . O1) AND (y . O2) & (y . O1) AND (y . O2) in { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ) by A2, XBOOLE_0:def_4; hence z in union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } by TARSKI:def_4; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } or z in L | O ) assume z in union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ; ::_thesis: z in L | O then consider Y being set such that A3: ( z in Y & Y in { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ) by TARSKI:def_4; consider x being Element of X such that A4: ( Y = (x . O1) AND (x . O2) & x in L ) by A3; A5: ( z in x . O1 & z in x . O2 ) by A3, A4, XBOOLE_0:def_4; reconsider z = z as Element of X by A3, A4; ( [x,z] in O1 & [x,z] in O2 ) by A5, RELAT_1:169; then [x,z] in O by A0, XBOOLE_0:def_4; hence z in L | O by A4, RELAT_1:def_13; ::_thesis: verum end; let O be Operation of X; ::_thesis: ( O = O2 AND iff for L being List of X holds L | O = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ) thus ( O = O2 AND implies for L being List of X holds L | O = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ) by AA; ::_thesis: ( ( for L being List of X holds L | O = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ) implies O = O2 AND ) assume A6: for L being List of X holds L | O = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ; ::_thesis: O = O2 AND now__::_thesis:_for_L_being_List_of_X_holds_L_|_O_=_L_|_(O1_/\_O2) let L be List of X; ::_thesis: L | O = L | (O1 /\ O2) thus L | O = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } by A6 .= L | (O1 /\ O2) by AA ; ::_thesis: verum end; hence O = O2 AND by Th3; ::_thesis: verum end; :: original: OR redefine funcO1 OR O2 -> Operation of X means :: MMLQUERY:def 17 for L being List of X holds L | it = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ; coherence O2 OR is Operation of X proof thus O1 \/ O2 is Subset of [:X,X:] ; ::_thesis: verum end; compatibility for b1 being Operation of X holds ( b1 = O2 OR iff for L being List of X holds L | b1 = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) proof AA: for O being Operation of X st O = O2 OR holds for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } proof let O be Operation of X; ::_thesis: ( O = O2 OR implies for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) assume A0: O = O1 \/ O2 ; ::_thesis: for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } defpred S1[ set , set ] means ( [\$1,\$2] in O1 or [\$1,\$2] in O2 ); let L be List of X; ::_thesis: L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } thus L | O c= union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } :: according to XBOOLE_0:def_10 ::_thesis: union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } c= L | O proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | O or z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) assume z in L | O ; ::_thesis: z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } then consider y being set such that A2: ( [y,z] in O & y in L ) by RELAT_1:def_13; reconsider y = y, z = z as Element of X by A2, ZFMISC_1:87; ( [y,z] in O1 or [y,z] in O2 ) by A0, A2, XBOOLE_0:def_3; then ( z in y . O1 or z in y . O2 ) by RELAT_1:169; then ( z in (y . O1) OR (y . O2) & (y . O1) OR (y . O2) in { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) by A2, XBOOLE_0:def_3; hence z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } by TARSKI:def_4; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } or z in L | O ) assume z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ; ::_thesis: z in L | O then consider Y being set such that A3: ( z in Y & Y in { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) by TARSKI:def_4; consider x being Element of X such that A4: ( Y = (x . O1) OR (x . O2) & x in L ) by A3; A5: ( z in x . O1 or z in x . O2 ) by A3, A4, XBOOLE_0:def_3; reconsider z = z as Element of X by A3, A4; ( [x,z] in O1 or [x,z] in O2 ) by A5, RELAT_1:169; then [x,z] in O by A0, XBOOLE_0:def_3; hence z in L | O by A4, RELAT_1:def_13; ::_thesis: verum end; let O be Operation of X; ::_thesis: ( O = O2 OR iff for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) thus ( O = O2 OR implies for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) by AA; ::_thesis: ( ( for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) implies O = O2 OR ) assume A6: for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ; ::_thesis: O = O2 OR now__::_thesis:_for_L_being_List_of_X_holds_L_|_O_=_L_|_(O1_\/_O2) let L be List of X; ::_thesis: L | O = L | (O1 \/ O2) thus L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } by A6 .= L | (O1 \/ O2) by AA ; ::_thesis: verum end; hence O = O2 OR by Th3; ::_thesis: verum end; :: original: BUTNOT redefine funcO1 BUTNOT O2 -> Operation of X means :: MMLQUERY:def 18 for L being List of X holds L | it = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ; coherence O2 BUTNOT is Operation of X proof thus O1 \ O2 is Subset of [:X,X:] ; ::_thesis: verum end; compatibility for b1 being Operation of X holds ( b1 = O2 BUTNOT iff for L being List of X holds L | b1 = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) proof AA: for O being Operation of X st O = O2 BUTNOT holds for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } proof let O be Operation of X; ::_thesis: ( O = O2 BUTNOT implies for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) assume A0: O = O1 \ O2 ; ::_thesis: for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } defpred S1[ set , set ] means ( [\$1,\$2] in O1 & not [\$1,\$2] in O2 ); let L be List of X; ::_thesis: L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } thus L | O c= union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } :: according to XBOOLE_0:def_10 ::_thesis: union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } c= L | O proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | O or z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) assume z in L | O ; ::_thesis: z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } then consider y being set such that A2: ( [y,z] in O & y in L ) by RELAT_1:def_13; reconsider y = y, z = z as Element of X by A2, ZFMISC_1:87; ( [y,z] in O1 & [y,z] nin O2 ) by A0, A2, XBOOLE_0:def_5; then ( z in y . O1 & z nin y . O2 ) by RELAT_1:169; then ( z in (y . O1) BUTNOT (y . O2) & (y . O1) BUTNOT (y . O2) in { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) by A2, XBOOLE_0:def_5; hence z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } by TARSKI:def_4; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } or z in L | O ) assume z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ; ::_thesis: z in L | O then consider Y being set such that A3: ( z in Y & Y in { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) by TARSKI:def_4; consider x being Element of X such that A4: ( Y = (x . O1) BUTNOT (x . O2) & x in L ) by A3; A5: ( z in x . O1 & z nin x . O2 ) by A3, A4, XBOOLE_0:def_5; reconsider z = z as Element of X by A3, A4; ( [x,z] in O1 & [x,z] nin O2 ) by A5, RELAT_1:169; then [x,z] in O by A0, XBOOLE_0:def_5; hence z in L | O by A4, RELAT_1:def_13; ::_thesis: verum end; let O be Operation of X; ::_thesis: ( O = O2 BUTNOT iff for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) thus ( O = O2 BUTNOT implies for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) by AA; ::_thesis: ( ( for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) implies O = O2 BUTNOT ) assume A6: for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ; ::_thesis: O = O2 BUTNOT now__::_thesis:_for_L_being_List_of_X_holds_L_|_O_=_L_|_(O1_\_O2) let L be List of X; ::_thesis: L | O = L | (O1 \ O2) thus L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } by A6 .= L | (O1 \ O2) by AA ; ::_thesis: verum end; hence O = O2 BUTNOT by Th3; ::_thesis: verum end; :: original: | redefine funcO1 | O2 -> Operation of X means :: MMLQUERY:def 19 for L being List of X holds L | it = (L | O1) | O2; coherence O2 | is Operation of X proof thus O1 * O2 is Relation of X ; ::_thesis: verum end; compatibility for b1 being Operation of X holds ( b1 = O2 | iff for L being List of X holds L | b1 = (L | O1) | O2 ) proof let O be Operation of X; ::_thesis: ( O = O2 | iff for L being List of X holds L | O = (L | O1) | O2 ) thus ( O = O2 | implies for L being List of X holds L | O = (L | O1) | O2 ) by RELAT_1:126; ::_thesis: ( ( for L being List of X holds L | O = (L | O1) | O2 ) implies O = O2 | ) assume A1: for L being List of X holds L | O = (L | O1) | O2 ; ::_thesis: O = O2 | now__::_thesis:_for_L_being_List_of_X_holds_L_|_O_=_L_|_(O1_*_O2) let L be List of X; ::_thesis: L | O = L | (O1 * O2) thus L | O = (L | O1) | O2 by A1 .= L | (O1 * O2) by RELAT_1:126 ; ::_thesis: verum end; hence O = O2 | by Th3; ::_thesis: verum end; funcO1 \& O2 -> Operation of X means :DefAmp: :: MMLQUERY:def 20 for L being List of X holds L | it = union { ((x . O1) \& O2) where x is Element of X : x in L } ; existence ex b1 being Operation of X st for L being List of X holds L | b1 = union { ((x . O1) \& O2) where x is Element of X : x in L } proof defpred S1[ set , set ] means ex x being Element of X st ( \$1 = x & \$2 in (x . O1) \& O2 ); consider O being Relation such that A1: for z, s being set holds ( [z,s] in O iff ( z in X & s in X & S1[z,s] ) ) from RELAT_1:sch_1(); O c= [:X,X:] proof let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [z,b1] in O or [z,b1] in [:X,X:] ) let s be set ; ::_thesis: ( not [z,s] in O or [z,s] in [:X,X:] ) assume [z,s] in O ; ::_thesis: [z,s] in [:X,X:] then ( z in X & s in X ) by A1; hence [z,s] in [:X,X:] by ZFMISC_1:87; ::_thesis: verum end; then reconsider O = O as Operation of X ; take O ; ::_thesis: for L being List of X holds L | O = union { ((x . O1) \& O2) where x is Element of X : x in L } let L be List of X; ::_thesis: L | O = union { ((x . O1) \& O2) where x is Element of X : x in L } thus L | O c= union { ((x . O1) \& O2) where x is Element of X : x in L } :: according to XBOOLE_0:def_10 ::_thesis: union { ((x . O1) \& O2) where x is Element of X : x in L } c= L | O proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | O or z in union { ((x . O1) \& O2) where x is Element of X : x in L } ) assume z in L | O ; ::_thesis: z in union { ((x . O1) \& O2) where x is Element of X : x in L } then consider y being Element of X such that A2: ( z in y . O & y in L ) by Th1; [y,z] in O by A2, RELAT_1:169; then ex x being Element of X st ( y = x & z in (x . O1) \& O2 ) by A1; then ( z in (y . O1) \& O2 & (y . O1) \& O2 in { ((x . O1) \& O2) where x is Element of X : x in L } ) by A2; hence z in union { ((x . O1) \& O2) where x is Element of X : x in L } by TARSKI:def_4; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { ((x . O1) \& O2) where x is Element of X : x in L } or z in L | O ) assume z in union { ((x . O1) \& O2) where x is Element of X : x in L } ; ::_thesis: z in L | O then consider Y being set such that A3: ( z in Y & Y in { ((x . O1) \& O2) where x is Element of X : x in L } ) by TARSKI:def_4; consider x being Element of X such that A4: ( Y = (x . O1) \& O2 & x in L ) by A3; [x,z] in O by A1, A3, A4; hence z in L | O by A4, RELAT_1:def_13; ::_thesis: verum end; uniqueness for b1, b2 being Operation of X st ( for L being List of X holds L | b1 = union { ((x . O1) \& O2) where x is Element of X : x in L } ) & ( for L being List of X holds L | b2 = union { ((x . O1) \& O2) where x is Element of X : x in L } ) holds b1 = b2 proof let R1, R2 be Operation of X; ::_thesis: ( ( for L being List of X holds L | R1 = union { ((x . O1) \& O2) where x is Element of X : x in L } ) & ( for L being List of X holds L | R2 = union { ((x . O1) \& O2) where x is Element of X : x in L } ) implies R1 = R2 ) assume that A1: for L being List of X holds L | R1 = union { ((x . O1) \& O2) where x is Element of X : x in L } and A2: for L being List of X holds L | R2 = union { ((x . O1) \& O2) where x is Element of X : x in L } ; ::_thesis: R1 = R2 now__::_thesis:_for_L_being_List_of_X_holds_L_|_R1_=_L_|_R2 let L be List of X; ::_thesis: L | R1 = L | R2 thus L | R1 = union { ((x . O1) \& O2) where x is Element of X : x in L } by A1 .= L | R2 by A2 ; ::_thesis: verum end; hence R1 = R2 by Th3; ::_thesis: verum end; end; :: deftheorem defines AND MMLQUERY:def_16_:_ for X being set for O1, O2, b4 being Operation of X holds ( b4 = O1 AND O2 iff for L being List of X holds L | b4 = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } ); :: deftheorem defines OR MMLQUERY:def_17_:_ for X being set for O1, O2, b4 being Operation of X holds ( b4 = O1 OR O2 iff for L being List of X holds L | b4 = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ); :: deftheorem defines BUTNOT MMLQUERY:def_18_:_ for X being set for O1, O2, b4 being Operation of X holds ( b4 = O1 BUTNOT O2 iff for L being List of X holds L | b4 = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ); :: deftheorem defines | MMLQUERY:def_19_:_ for X being set for O1, O2, b4 being Operation of X holds ( b4 = O1 | O2 iff for L being List of X holds L | b4 = (L | O1) | O2 ); :: deftheorem DefAmp defines \& MMLQUERY:def_20_:_ for X being set for O1, O2, b4 being Operation of X holds ( b4 = O1 \& O2 iff for L being List of X holds L | b4 = union { ((x . O1) \& O2) where x is Element of X : x in L } ); theorem :: MMLQUERY:31 for X being set for x being Element of X for O1, O2 being Operation of X holds x . (O1 AND O2) = (x . O1) AND (x . O2) by RELSET_2:11; theorem :: MMLQUERY:32 for X being set for x being Element of X for O1, O2 being Operation of X holds x . (O1 OR O2) = (x . O1) OR (x . O2) by RELSET_2:10; theorem :: MMLQUERY:33 for X being set for x being Element of X for O1, O2 being Operation of X holds x . (O1 BUTNOT O2) = (x . O1) BUTNOT (x . O2) by RELSET_2:12; theorem :: MMLQUERY:34 for X being set for x being Element of X for O1, O2 being Operation of X holds x . (O1 | O2) = (x . O1) | O2 by RELAT_1:126; theorem Th25: :: MMLQUERY:35 for X being set for x being Element of X for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2 proof let X be set ; ::_thesis: for x being Element of X for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2 let x be Element of X; ::_thesis: for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2 let O1, O2 be Operation of X; ::_thesis: x . (O1 \& O2) = (x . O1) \& O2 percases ( X = {} or X <> {} ) ; suppose X = {} ; ::_thesis: x . (O1 \& O2) = (x . O1) \& O2 then ( x . (O1 \& O2) = {} & (x . O1) \& O2 = {} ) ; hence x . (O1 \& O2) = (x . O1) \& O2 ; ::_thesis: verum end; suppose X <> {} ; ::_thesis: x . (O1 \& O2) = (x . O1) \& O2 then reconsider L = {x} as List of X by ZFMISC_1:31; A1: { ((a . O1) \& O2) where a is Element of X : a in L } = {((x . O1) \& O2)} proof thus { ((a . O1) \& O2) where a is Element of X : a in L } c= {((x . O1) \& O2)} :: according to XBOOLE_0:def_10 ::_thesis: {((x . O1) \& O2)} c= { ((a . O1) \& O2) where a is Element of X : a in L } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { ((a . O1) \& O2) where a is Element of X : a in L } or z in {((x . O1) \& O2)} ) assume z in { ((a . O1) \& O2) where a is Element of X : a in L } ; ::_thesis: z in {((x . O1) \& O2)} then consider a being Element of X such that A2: ( z = (a . O1) \& O2 & a in L ) ; a = x by A2, TARSKI:def_1; hence z in {((x . O1) \& O2)} by A2, TARSKI:def_1; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {((x . O1) \& O2)} or z in { ((a . O1) \& O2) where a is Element of X : a in L } ) assume z in {((x . O1) \& O2)} ; ::_thesis: z in { ((a . O1) \& O2) where a is Element of X : a in L } then ( z = (x . O1) \& O2 & x in L ) by TARSKI:def_1; hence z in { ((a . O1) \& O2) where a is Element of X : a in L } ; ::_thesis: verum end; thus x . (O1 \& O2) = union { ((a . O1) \& O2) where a is Element of X : a in L } by DefAmp .= (x . O1) \& O2 by A1, ZFMISC_1:25 ; ::_thesis: verum end; end; end; theorem Th4: :: MMLQUERY:36 for z, s, X being set for O being Operation of X holds ( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) ) proof let z, s, X be set ; ::_thesis: for O being Operation of X holds ( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) ) let O be Operation of X; ::_thesis: ( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) ) thus ( [z,s] in NOT O implies ( z = s & z in X & z nin dom O ) ) ::_thesis: ( z = s & z in X & z nin dom O implies [z,s] in NOT O ) proof assume A7: [z,s] in NOT O ; ::_thesis: ( z = s & z in X & z nin dom O ) then ( s in Im ((NOT O),z) & z in X ) by RELAT_1:169, ZFMISC_1:87; then ( s in (NOT O) .: {z} & {z} c= X ) by ZFMISC_1:31; then s in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by DEFNOT; then consider Y being set such that A1: ( s in Y & Y in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } ) by TARSKI:def_4; consider x being Element of X such that A2: ( Y = IFEQ ((x . O),{},{x},{}) & x in {z} ) by A1; A3: x = z by A2, TARSKI:def_1; A5: x . O = {} by A1, A2, FUNCOP_1:def_8; then s in {x} by A1, A2, FUNCOP_1:def_8; then ( s = x & ( for s being set holds [x,s] nin O ) ) by A5, RELAT_1:169, TARSKI:def_1; hence ( z = s & z in X & z nin dom O ) by A3, A7, XTUPLE_0:def_12, ZFMISC_1:87; ::_thesis: verum end; assume A6: ( z = s & z in X & z nin dom O ) ; ::_thesis: [z,s] in NOT O then reconsider z = z as Element of X ; z . O c= {} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in z . O or y in {} ) assume y in z . O ; ::_thesis: y in {} then [z,y] in O by RELAT_1:169; hence y in {} by A6, XTUPLE_0:def_12; ::_thesis: verum end; then z . O = {} ; then A7: IFEQ ((z . O),{},{z},{}) = {z} by FUNCOP_1:def_8; A8: z in {z} by TARSKI:def_1; reconsider L = {z} as Subset of X by A6, ZFMISC_1:31; {z} in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by A7, A8; then z in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by A8, TARSKI:def_4; then z in L | (NOT O) by DEFNOT; then z in z . (NOT O) ; hence [z,s] in NOT O by A6, RELAT_1:169; ::_thesis: verum end; theorem Th5: :: MMLQUERY:37 for X being set for O being Operation of X holds NOT O = id (X \ (dom O)) proof let X be set ; ::_thesis: for O being Operation of X holds NOT O = id (X \ (dom O)) let O be Operation of X; ::_thesis: NOT O = id (X \ (dom O)) let z be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds ( ( not [z,b1] in NOT O or [z,b1] in id (X \ (dom O)) ) & ( not [z,b1] in id (X \ (dom O)) or [z,b1] in NOT O ) ) let s be set ; ::_thesis: ( ( not [z,s] in NOT O or [z,s] in id (X \ (dom O)) ) & ( not [z,s] in id (X \ (dom O)) or [z,s] in NOT O ) ) thus ( [z,s] in NOT O implies [z,s] in id (X \ (dom O)) ) ::_thesis: ( not [z,s] in id (X \ (dom O)) or [z,s] in NOT O ) proof assume [z,s] in NOT O ; ::_thesis: [z,s] in id (X \ (dom O)) then A1: ( z = s & z in X & z nin dom O ) by Th4; then z in X \ (dom O) by XBOOLE_0:def_5; hence [z,s] in id (X \ (dom O)) by A1, RELAT_1:def_10; ::_thesis: verum end; assume [z,s] in id (X \ (dom O)) ; ::_thesis: [z,s] in NOT O then A2: ( z = s & z in X \ (dom O) ) by RELAT_1:def_10; then ( z in X & z nin dom O ) by XBOOLE_0:def_5; hence [z,s] in NOT O by A2, Th4; ::_thesis: verum end; theorem Th6: :: MMLQUERY:38 for X being set for O being Operation of X holds dom (NOT (NOT O)) = dom O proof let X be set ; ::_thesis: for O being Operation of X holds dom (NOT (NOT O)) = dom O let O be Operation of X; ::_thesis: dom (NOT (NOT O)) = dom O thus dom (NOT (NOT O)) = dom (id (X \ (dom (NOT O)))) by Th5 .= X \ (dom (NOT O)) by RELAT_1:45 .= X \ (dom (id (X \ (dom O)))) by Th5 .= X \ (X \ (dom O)) by RELAT_1:45 .= X /\ (dom O) by XBOOLE_1:48 .= dom O by XBOOLE_1:28 ; ::_thesis: verum end; theorem :: MMLQUERY:39 for X being set for L being List of X for O being Operation of X holds L WHERE (NOT (NOT O)) = L WHERE O proof let X be set ; ::_thesis: for L being List of X for O being Operation of X holds L WHERE (NOT (NOT O)) = L WHERE O let L be List of X; ::_thesis: for O being Operation of X holds L WHERE (NOT (NOT O)) = L WHERE O let O be Operation of X; ::_thesis: L WHERE (NOT (NOT O)) = L WHERE O thus L WHERE (NOT (NOT O)) c= L WHERE O :: according to XBOOLE_0:def_10 ::_thesis: L WHERE O c= L WHERE (NOT (NOT O)) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE (NOT (NOT O)) or z in L WHERE O ) assume A0: z in L WHERE (NOT (NOT O)) ; ::_thesis: z in L WHERE O then reconsider x = z as Element of X ; A1: ( x in L & x . (NOT (NOT O)) <> {} ) by A0, ThW; then x in dom (NOT (NOT O)) by RELAT_1:170; then x in dom O by Th6; then x . O <> {} by RELAT_1:170; hence z in L WHERE O by A1, ThW; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE O or z in L WHERE (NOT (NOT O)) ) assume A2: z in L WHERE O ; ::_thesis: z in L WHERE (NOT (NOT O)) then reconsider x = z as Element of X ; A3: ( z in L & x . O <> {} ) by A2, ThW; then x in dom O by RELAT_1:170; then x in dom (NOT (NOT O)) by Th6; then x . (NOT (NOT O)) <> {} by RELAT_1:170; hence z in L WHERE (NOT (NOT O)) by A3, ThW; ::_thesis: verum end; theorem :: MMLQUERY:40 for X being set for L being List of X for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O) proof let X be set ; ::_thesis: for L being List of X for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O) let L be List of X; ::_thesis: for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O) let O be Operation of X; ::_thesis: L WHEREeq (O,0) = L WHERE (NOT O) thus L WHEREeq (O,0) c= L WHERE (NOT O) :: according to XBOOLE_0:def_10 ::_thesis: L WHERE (NOT O) c= L WHEREeq (O,0) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREeq (O,0) or z in L WHERE (NOT O) ) assume z in L WHEREeq (O,0) ; ::_thesis: z in L WHERE (NOT O) then consider x being Element of X such that A1: ( z = x & card (x . O) = 0 & x in L ) ; x . O = {} by A1; then x nin dom O by RELAT_1:170; then [x,x] in NOT O by A1, Th4; then x,x in NOT O by Def1; hence z in L WHERE (NOT O) by A1; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE (NOT O) or z in L WHEREeq (O,0) ) assume z in L WHERE (NOT O) ; ::_thesis: z in L WHEREeq (O,0) then consider x being Element of X such that A2: ( z = x & ex y being Element of X st ( x,y in NOT O & x in L ) ) ; consider y being Element of X such that A3: ( x,y in NOT O & x in L ) by A2; [x,y] in NOT O by A3, Def1; then ( x = y & x in X & x nin dom O ) by Th4; then x . O = {} by RELAT_1:170; then card (x . O) = 0 ; hence z in L WHEREeq (O,0) by A2; ::_thesis: verum end; theorem :: MMLQUERY:41 for X being set for O being Operation of X holds NOT (NOT (NOT O)) = NOT O proof let X be set ; ::_thesis: for O being Operation of X holds NOT (NOT (NOT O)) = NOT O let O be Operation of X; ::_thesis: NOT (NOT (NOT O)) = NOT O thus NOT (NOT (NOT O)) = id (X \ (dom (NOT (NOT O)))) by Th5 .= id (X \ (dom O)) by Th6 .= NOT O by Th5 ; ::_thesis: verum end; theorem :: MMLQUERY:42 for X being set for O1, O2 being Operation of X holds (NOT O1) OR (NOT O2) c= NOT (O1 AND O2) proof let X be set ; ::_thesis: for O1, O2 being Operation of X holds (NOT O1) OR (NOT O2) c= NOT (O1 AND O2) let O1, O2 be Operation of X; ::_thesis: (NOT O1) OR (NOT O2) c= NOT (O1 AND O2) let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [z,b1] in (NOT O1) OR (NOT O2) or [z,b1] in NOT (O1 AND O2) ) let s be set ; ::_thesis: ( not [z,s] in (NOT O1) OR (NOT O2) or [z,s] in NOT (O1 AND O2) ) assume [z,s] in (NOT O1) OR (NOT O2) ; ::_thesis: [z,s] in NOT (O1 AND O2) then ( [z,s] in NOT O1 or [z,s] in NOT O2 ) by XBOOLE_0:def_3; then A1: ( s = z & z in X & ( z nin dom O1 or z nin dom O2 ) ) by Th4; then ( z nin (dom O1) /\ (dom O2) & dom (O1 AND O2) c= (dom O1) /\ (dom O2) ) by RELAT_1:2, XBOOLE_0:def_4; then z nin dom (O1 AND O2) ; hence [z,s] in NOT (O1 AND O2) by A1, Th4; ::_thesis: verum end; theorem :: MMLQUERY:43 for X being set for O1, O2 being Operation of X holds NOT (O1 OR O2) = (NOT O1) AND (NOT O2) proof let X be set ; ::_thesis: for O1, O2 being Operation of X holds NOT (O1 OR O2) = (NOT O1) AND (NOT O2) let O1, O2 be Operation of X; ::_thesis: NOT (O1 OR O2) = (NOT O1) AND (NOT O2) let z be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds ( ( not [z,b1] in NOT (O1 OR O2) or [z,b1] in (NOT O1) AND (NOT O2) ) & ( not [z,b1] in (NOT O1) AND (NOT O2) or [z,b1] in NOT (O1 OR O2) ) ) let s be set ; ::_thesis: ( ( not [z,s] in NOT (O1 OR O2) or [z,s] in (NOT O1) AND (NOT O2) ) & ( not [z,s] in (NOT O1) AND (NOT O2) or [z,s] in NOT (O1 OR O2) ) ) thus ( [z,s] in NOT (O1 OR O2) implies [z,s] in (NOT O1) AND (NOT O2) ) ::_thesis: ( not [z,s] in (NOT O1) AND (NOT O2) or [z,s] in NOT (O1 OR O2) ) proof assume [z,s] in NOT (O1 OR O2) ; ::_thesis: [z,s] in (NOT O1) AND (NOT O2) then A1: ( z = s & z in X & z nin dom (O1 OR O2) ) by Th4; then z nin (dom O1) \/ (dom O2) by RELAT_1:1; then ( z nin dom O1 & z nin dom O2 ) by XBOOLE_0:def_3; then ( [z,s] in NOT O1 & [z,s] in NOT O2 ) by A1, Th4; hence [z,s] in (NOT O1) AND (NOT O2) by XBOOLE_0:def_4; ::_thesis: verum end; assume [z,s] in (NOT O1) AND (NOT O2) ; ::_thesis: [z,s] in NOT (O1 OR O2) then ( [z,s] in NOT O1 & [z,s] in NOT O2 ) by XBOOLE_0:def_4; then A1: ( z = s & z in X & z nin dom O1 & z nin dom O2 ) by Th4; then z nin (dom O1) \/ (dom O2) by XBOOLE_0:def_3; then z nin dom (O1 OR O2) by RELAT_1:1; hence [z,s] in NOT (O1 OR O2) by A1, Th4; ::_thesis: verum end; theorem :: MMLQUERY:44 for X being set for O1, O2, O being Operation of X st dom O1 = X & dom O2 = X holds (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O) proof let X be set ; ::_thesis: for O1, O2, O being Operation of X st dom O1 = X & dom O2 = X holds (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O) let O1, O2, O be Operation of X; ::_thesis: ( dom O1 = X & dom O2 = X implies (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O) ) assume A0: ( dom O1 = X & dom O2 = X ) ; ::_thesis: (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O) let z be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds ( ( not [z,b1] in (O1 OR O2) \& O or [z,b1] in (O1 \& O) AND (O2 \& O) ) & ( not [z,b1] in (O1 \& O) AND (O2 \& O) or [z,b1] in (O1 OR O2) \& O ) ) let s be set ; ::_thesis: ( ( not [z,s] in (O1 OR O2) \& O or [z,s] in (O1 \& O) AND (O2 \& O) ) & ( not [z,s] in (O1 \& O) AND (O2 \& O) or [z,s] in (O1 OR O2) \& O ) ) thus ( [z,s] in (O1 OR O2) \& O implies [z,s] in (O1 \& O) AND (O2 \& O) ) ::_thesis: ( not [z,s] in (O1 \& O) AND (O2 \& O) or [z,s] in (O1 OR O2) \& O ) proof assume Z0: [z,s] in (O1 OR O2) \& O ; ::_thesis: [z,s] in (O1 \& O) AND (O2 \& O) then reconsider z = z, s = s as Element of X by ZFMISC_1:87; s in z . ((O1 OR O2) \& O) by Z0, RELAT_1:169; then s in (z . (O1 OR O2)) \& O by Th25; then ( s in ((z . O1) OR (z . O2)) \& O & z . O1 <> {} & z . O2 <> {} ) by A0, RELAT_1:170, RELSET_2:10; then s in ((z . O1) \& O) AND ((z . O2) \& O) by Th17; then s in (z . (O1 \& O)) AND ((z . O2) \& O) by Th25; then s in (z . (O1 \& O)) AND (z . (O2 \& O)) by Th25; then s in z . ((O1 \& O) AND (O2 \& O)) by RELSET_2:11; hence [z,s] in (O1 \& O) AND (O2 \& O) by RELAT_1:169; ::_thesis: verum end; assume Z1: [z,s] in (O1 \& O) AND (O2 \& O) ; ::_thesis: [z,s] in (O1 OR O2) \& O then reconsider z = z, s = s as Element of X by ZFMISC_1:87; s in z . ((O1 \& O) AND (O2 \& O)) by Z1, RELAT_1:169; then s in (z . (O1 \& O)) AND (z . (O2 \& O)) by RELSET_2:11; then s in (z . (O1 \& O)) AND ((z . O2) \& O) by Th25; then ( s in ((z . O1) \& O) AND ((z . O2) \& O) & z . O1 <> {} & z . O2 <> {} ) by Th25, A0, RELAT_1:170; then s in ((z . O1) OR (z . O2)) \& O by Th17; then s in (z . (O1 OR O2)) \& O by RELSET_2:10; then s in z . ((O1 OR O2) \& O) by Th25; hence [z,s] in (O1 OR O2) \& O by RELAT_1:169; ::_thesis: verum end; definition let X be set ; let O be Operation of X; attrO is filtering means :DEFFILT: :: MMLQUERY:def 21 O c= id X; end; :: deftheorem DEFFILT defines filtering MMLQUERY:def_21_:_ for X being set for O being Operation of X holds ( O is filtering iff O c= id X ); theorem Th20: :: MMLQUERY:45 for X being set for O being Operation of X holds ( O is filtering iff O = id (dom O) ) proof let X be set ; ::_thesis: for O being Operation of X holds ( O is filtering iff O = id (dom O) ) let O be Operation of X; ::_thesis: ( O is filtering iff O = id (dom O) ) thus ( O is filtering implies O = id (dom O) ) ::_thesis: ( O = id (dom O) implies O is filtering ) proof assume A1: O c= id X ; :: according to MMLQUERY:def_21 ::_thesis: O = id (dom O) let z be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds ( ( not [z,b1] in O or [z,b1] in id (dom O) ) & ( not [z,b1] in id (dom O) or [z,b1] in O ) ) let s be set ; ::_thesis: ( ( not [z,s] in O or [z,s] in id (dom O) ) & ( not [z,s] in id (dom O) or [z,s] in O ) ) thus ( [z,s] in O implies [z,s] in id (dom O) ) ::_thesis: ( not [z,s] in id (dom O) or [z,s] in O ) proof assume [z,s] in O ; ::_thesis: [z,s] in id (dom O) then ( z in dom O & z = s ) by A1, RELAT_1:def_10, XTUPLE_0:def_12; hence [z,s] in id (dom O) by RELAT_1:def_10; ::_thesis: verum end; assume [z,s] in id (dom O) ; ::_thesis: [z,s] in O then A2: ( z in dom O & z = s ) by RELAT_1:def_10; then consider y being set such that A3: [z,y] in O by XTUPLE_0:def_12; thus [z,s] in O by A1, A2, A3, RELAT_1:def_10; ::_thesis: verum end; assume O = id (dom O) ; ::_thesis: O is filtering hence O c= id X by SYSREL:15; :: according to MMLQUERY:def_21 ::_thesis: verum end; registration let X be set ; let O be Operation of X; cluster NOT O -> filtering ; coherence NOT O is filtering proof NOT O = id (X \ (dom O)) by Th5; hence NOT O c= id X by SYSREL:15; :: according to MMLQUERY:def_21 ::_thesis: verum end; end; registration let X be set ; cluster Relation-like X -defined X -valued filtering for Element of bool [:X,X:]; existence ex b1 being Operation of X st b1 is filtering proof set O = the Operation of X; take NOT the Operation of X ; ::_thesis: NOT the Operation of X is filtering thus NOT the Operation of X is filtering ; ::_thesis: verum end; end; registration let X be set ; let F be filtering Operation of X; let O be Operation of X; clusterO AND -> filtering for Operation of X; coherence for b1 being Operation of X st b1 = F AND O holds b1 is filtering proof let O1 be Operation of X; ::_thesis: ( O1 = F AND O implies O1 is filtering ) assume O1 = F AND O ; ::_thesis: O1 is filtering then ( O1 c= F & F c= id X ) by DEFFILT, XBOOLE_1:17; hence O1 c= id X by XBOOLE_1:1; :: according to MMLQUERY:def_21 ::_thesis: verum end; clusterF AND -> filtering for Operation of X; coherence for b1 being Operation of X st b1 = O AND F holds b1 is filtering ; clusterO BUTNOT -> filtering for Operation of X; coherence for b1 being Operation of X st b1 = F BUTNOT O holds b1 is filtering proof let O1 be Operation of X; ::_thesis: ( O1 = F BUTNOT O implies O1 is filtering ) assume O1 = F BUTNOT O ; ::_thesis: O1 is filtering then ( O1 c= F & F c= id X ) by DEFFILT, XBOOLE_1:36; hence O1 c= id X by XBOOLE_1:1; :: according to MMLQUERY:def_21 ::_thesis: verum end; end; registration let X be set ; let F1, F2 be filtering Operation of X; clusterF2 OR -> filtering for Operation of X; coherence for b1 being Operation of X st b1 = F1 OR F2 holds b1 is filtering proof let O1 be Operation of X; ::_thesis: ( O1 = F1 OR F2 implies O1 is filtering ) assume A1: O1 = F1 OR F2 ; ::_thesis: O1 is filtering ( F1 c= id X & F2 c= id X ) by DEFFILT; hence O1 c= id X by A1, XBOOLE_1:8; :: according to MMLQUERY:def_21 ::_thesis: verum end; end; theorem Th11: :: MMLQUERY:46 for X, z being set for x being Element of X for F being filtering Operation of X st z in x . F holds z = x proof let X, z be set ; ::_thesis: for x being Element of X for F being filtering Operation of X st z in x . F holds z = x let x be Element of X; ::_thesis: for F being filtering Operation of X st z in x . F holds z = x let F be filtering Operation of X; ::_thesis: ( z in x . F implies z = x ) assume z in x . F ; ::_thesis: z = x then ( [x,z] in F & F c= id X ) by DEFFILT, RELAT_1:169; hence z = x by RELAT_1:def_10; ::_thesis: verum end; theorem :: MMLQUERY:47 for X being set for L being List of X for F being filtering Operation of X holds L | F = L WHERE F proof let X be set ; ::_thesis: for L being List of X for F being filtering Operation of X holds L | F = L WHERE F let L be List of X; ::_thesis: for F being filtering Operation of X holds L | F = L WHERE F let F be filtering Operation of X; ::_thesis: L | F = L WHERE F thus L | F c= L WHERE F :: according to XBOOLE_0:def_10 ::_thesis: L WHERE F c= L | F proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | F or z in L WHERE F ) assume z in L | F ; ::_thesis: z in L WHERE F then consider y being Element of X such that A1: ( z in y . F & y in L ) by Th1; z = y by A1, Th11; hence z in L WHERE F by A1, ThW; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE F or z in L | F ) assume A2: z in L WHERE F ; ::_thesis: z in L | F then reconsider x = z as Element of X ; A3: ( x in L & x . F <> {} ) by A2, ThW; set y = the Element of x . F; A4: [x, the Element of x . F] in F by A3, RELAT_1:169; F c= id X by DEFFILT; then x = the Element of x . F by A4, RELAT_1:def_10; hence z in L | F by A3, Th1; ::_thesis: verum end; theorem :: MMLQUERY:48 for X being set for F being filtering Operation of X holds NOT (NOT F) = F proof let X be set ; ::_thesis: for F being filtering Operation of X holds NOT (NOT F) = F let F be filtering Operation of X; ::_thesis: NOT (NOT F) = F thus NOT (NOT F) = id (X \ (dom (NOT F))) by Th5 .= id (X \ (dom (id (X \ (dom F))))) by Th5 .= id (X \ (X \ (dom F))) by RELAT_1:45 .= id (X /\ (dom F)) by XBOOLE_1:48 .= id (dom F) by XBOOLE_1:28 .= F by Th20 ; ::_thesis: verum end; theorem :: MMLQUERY:49 for X being set for F1, F2 being filtering Operation of X holds NOT (F1 AND F2) = (NOT F1) OR (NOT F2) proof let X be set ; ::_thesis: for F1, F2 being filtering Operation of X holds NOT (F1 AND F2) = (NOT F1) OR (NOT F2) let F1, F2 be filtering Operation of X; ::_thesis: NOT (F1 AND F2) = (NOT F1) OR (NOT F2) A1: ( F1 = id (dom F1) & F2 = id (dom F2) ) by Th20; NOT (F1 AND F2) = id (X \ (dom (F1 AND F2))) by Th5 .= id (X \ (dom (id ((dom F1) AND (dom F2))))) by A1, SYSREL:14 .= id (X \ ((dom F1) AND (dom F2))) by RELAT_1:45 .= id ((X \ (dom F1)) \/ (X \ (dom F2))) by XBOOLE_1:54 .= (id (X \ (dom F1))) \/ (id (X \ (dom F2))) by SYSREL:14 .= (NOT F1) \/ (id (X \ (dom F2))) by Th5 ; hence NOT (F1 AND F2) = (NOT F1) OR (NOT F2) by Th5; ::_thesis: verum end; theorem Th71: :: MMLQUERY:50 for X being set for O being Operation of X holds dom (O OR (NOT O)) = X proof let X be set ; ::_thesis: for O being Operation of X holds dom (O OR (NOT O)) = X let O be Operation of X; ::_thesis: dom (O OR (NOT O)) = X thus dom (O OR (NOT O)) = (dom O) OR (dom (NOT O)) by RELAT_1:1 .= (dom O) \/ (dom (id (X \ (dom O)))) by Th5 .= (dom O) OR (X \ (dom O)) by RELAT_1:45 .= (dom O) \/ X by XBOOLE_1:39 .= X by XBOOLE_1:12 ; ::_thesis: verum end; theorem :: MMLQUERY:51 for X being set for F being filtering Operation of X holds F OR (NOT F) = id X proof let X be set ; ::_thesis: for F being filtering Operation of X holds F OR (NOT F) = id X let F be filtering Operation of X; ::_thesis: F OR (NOT F) = id X ( dom (F OR (NOT F)) = X & F OR (NOT F) c= id X ) by Th71, DEFFILT; hence F OR (NOT F) = id X by SYSREL:17; ::_thesis: verum end; theorem Th72: :: MMLQUERY:52 for X being set for O being Operation of X holds O AND (NOT O) = {} proof let X be set ; ::_thesis: for O being Operation of X holds O AND (NOT O) = {} let O be Operation of X; ::_thesis: O AND (NOT O) = {} dom (O AND (NOT O)) = dom (O /\ (id (X \ (dom O)))) by Th5; then A1: dom (O AND (NOT O)) c= (dom O) /\ (dom (id (X \ (dom O)))) by RELAT_1:2; (dom O) /\ (dom (id (X \ (dom O)))) = (dom O) /\ (X \ (dom O)) by RELAT_1:45 .= ((dom O) /\ X) \ (dom O) by XBOOLE_1:49 .= (dom O) \ (dom O) by XBOOLE_1:28 .= {} by XBOOLE_1:37 ; hence O AND (NOT O) = {} by A1, RELAT_1:41, XBOOLE_1:3; ::_thesis: verum end; theorem :: MMLQUERY:53 for X being set for O1, O2 being Operation of X holds (O1 OR O2) AND (NOT O1) c= O2 proof let X be set ; ::_thesis: for O1, O2 being Operation of X holds (O1 OR O2) AND (NOT O1) c= O2 let O1, O2 be Operation of X; ::_thesis: (O1 OR O2) AND (NOT O1) c= O2 (O1 OR O2) AND (NOT O1) = (O1 AND (NOT O1)) OR (O2 AND (NOT O1)) by XBOOLE_1:23 .= {} \/ (O2 AND (NOT O1)) by Th72 .= O2 AND (NOT O1) ; hence (O1 OR O2) AND (NOT O1) c= O2 by XBOOLE_1:17; ::_thesis: verum end; begin definition let A be FinSequence; let a be set ; func #occurrences (a,A) -> Nat equals :: MMLQUERY:def 22 card { i where i is Element of NAT : ( i in dom A & a in A . i ) } ; coherence card { i where i is Element of NAT : ( i in dom A & a in A . i ) } is Nat proof { i where i is Element of NAT : ( i in dom A & a in A . i ) } c= dom A proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } or z in dom A ) assume z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } ; ::_thesis: z in dom A then ex i being Element of NAT st ( z = i & i in dom A & a in A . i ) ; hence z in dom A ; ::_thesis: verum end; hence card { i where i is Element of NAT : ( i in dom A & a in A . i ) } is Nat ; ::_thesis: verum end; end; :: deftheorem defines #occurrences MMLQUERY:def_22_:_ for A being FinSequence for a being set holds #occurrences (a,A) = card { i where i is Element of NAT : ( i in dom A & a in A . i ) } ; theorem Th21: :: MMLQUERY:54 for A being FinSequence for a being set holds #occurrences (a,A) <= len A proof let A be FinSequence; ::_thesis: for a being set holds #occurrences (a,A) <= len A let a be set ; ::_thesis: #occurrences (a,A) <= len A { i where i is Element of NAT : ( i in dom A & a in A . i ) } c= dom A proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } or z in dom A ) assume z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } ; ::_thesis: z in dom A then ex i being Element of NAT st ( z = i & i in dom A & a in A . i ) ; hence z in dom A ; ::_thesis: verum end; then ( #occurrences (a,A) c= card (dom A) & dom A = Seg (len A) & card (Seg (len A)) = len A ) by CARD_1:11, FINSEQ_1:57, FINSEQ_1:def_3; hence #occurrences (a,A) <= len A by NAT_1:39; ::_thesis: verum end; theorem Th22: :: MMLQUERY:55 for A being FinSequence for a being set holds ( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) ) proof let A be FinSequence; ::_thesis: for a being set holds ( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) ) let a be set ; ::_thesis: ( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) ) A2: { i where i is Element of NAT : ( i in dom A & a in A . i ) } c= dom A proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } or z in dom A ) assume z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } ; ::_thesis: z in dom A then ex i being Element of NAT st ( z = i & i in dom A & a in A . i ) ; hence z in dom A ; ::_thesis: verum end; A6: ( dom A = Seg (len A) & card (Seg (len A)) = len A ) by FINSEQ_1:57, FINSEQ_1:def_3; hereby ::_thesis: ( a in meet (rng A) implies ( A <> {} & #occurrences (a,A) = len A ) ) assume A <> {} ; ::_thesis: ( #occurrences (a,A) = len A implies a in meet (rng A) ) then A0: rng A <> {} by RELAT_1:41; assume Z1: #occurrences (a,A) = len A ; ::_thesis: a in meet (rng A) A1: { i where i is Element of NAT : ( i in dom A & a in A . i ) } = dom A by Z1, A2, A6, CARD_FIN:1; now__::_thesis:_for_z_being_set_st_z_in_rng_A_holds_ a_in_z let z be set ; ::_thesis: ( z in rng A implies a in z ) assume z in rng A ; ::_thesis: a in z then consider s being set such that A3: ( s in dom A & z = A . s ) by FUNCT_1:def_3; consider i being Element of NAT such that A4: ( s = i & i in dom A & a in A . i ) by A1, A3; thus a in z by A3, A4; ::_thesis: verum end; hence a in meet (rng A) by A0, SETFAM_1:def_1; ::_thesis: verum end; assume Z2: a in meet (rng A) ; ::_thesis: ( A <> {} & #occurrences (a,A) = len A ) thus A <> {} by Z2, RELAT_1:38, SETFAM_1:def_1; ::_thesis: #occurrences (a,A) = len A dom A c= { i where i is Element of NAT : ( i in dom A & a in A . i ) } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom A or z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } ) assume A7: z in dom A ; ::_thesis: z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } then A . z in rng A by FUNCT_1:def_3; then a in A . z by Z2, SETFAM_1:def_1; hence z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } by A7; ::_thesis: verum end; hence #occurrences (a,A) = len A by A6, A2, XBOOLE_0:def_10; ::_thesis: verum end; definition let A be FinSequence; func max# A -> Nat means :MAX: :: MMLQUERY:def 23 ( ( for a being set holds #occurrences (a,A) <= it ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds it <= n ) ); existence ex b1 being Nat st ( ( for a being set holds #occurrences (a,A) <= b1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds b1 <= n ) ) proof defpred S1[ Nat] means for a being set holds #occurrences (a,A) <= \$1; S1[ len A] by Th21; then A1: ex n being Nat st S1[n] ; consider n being Nat such that A2: ( S1[n] & ( for m being Nat st S1[m] holds n <= m ) ) from NAT_1:sch_5(A1); take n ; ::_thesis: ( ( for a being set holds #occurrences (a,A) <= n ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds n <= n ) ) thus ( ( for a being set holds #occurrences (a,A) <= n ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds n <= n ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Nat st ( for a being set holds #occurrences (a,A) <= b1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds b1 <= n ) & ( for a being set holds #occurrences (a,A) <= b2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds b2 <= n ) holds b1 = b2 proof let n1, n2 be Nat; ::_thesis: ( ( for a being set holds #occurrences (a,A) <= n1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds n1 <= n ) & ( for a being set holds #occurrences (a,A) <= n2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds n2 <= n ) implies n1 = n2 ) assume that A1: ( ( for a being set holds #occurrences (a,A) <= n1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds n1 <= n ) ) and A2: ( ( for a being set holds #occurrences (a,A) <= n2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds n2 <= n ) ) ; ::_thesis: n1 = n2 ( n1 <= n2 & n2 <= n1 ) by A1, A2; hence n1 = n2 by XXREAL_0:1; ::_thesis: verum end; end; :: deftheorem MAX defines max# MMLQUERY:def_23_:_ for A being FinSequence for b2 being Nat holds ( b2 = max# A iff ( ( for a being set holds #occurrences (a,A) <= b2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds b2 <= n ) ) ); theorem Th23: :: MMLQUERY:56 for A being FinSequence holds max# A <= len A proof let A be FinSequence; ::_thesis: max# A <= len A for a being set holds #occurrences (a,A) <= len A by Th21; hence max# A <= len A by MAX; ::_thesis: verum end; theorem :: MMLQUERY:57 for A being FinSequence for a being set st #occurrences (a,A) = len A holds max# A = len A proof let A be FinSequence; ::_thesis: for a being set st #occurrences (a,A) = len A holds max# A = len A let a be set ; ::_thesis: ( #occurrences (a,A) = len A implies max# A = len A ) assume #occurrences (a,A) = len A ; ::_thesis: max# A = len A then ( len A <= max# A & max# A <= len A ) by MAX, Th23; hence max# A = len A by XXREAL_0:1; ::_thesis: verum end; definition let X be set ; let A be FinSequence of bool X; let n be Nat; func ROUGH (A,n) -> List of X equals :ROUGH1: :: MMLQUERY:def 24 { x where x is Element of X : n <= #occurrences (x,A) } if X <> {} ; consistency for b1 being List of X holds verum ; coherence ( X <> {} implies { x where x is Element of X : n <= #occurrences (x,A) } is List of X ) proof assume A1: X <> {} ; ::_thesis: { x where x is Element of X : n <= #occurrences (x,A) } is List of X { x where x is Element of X : n <= #occurrences (x,A) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : n <= #occurrences (x,A) } or z in X ) assume z in { x where x is Element of X : n <= #occurrences (x,A) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & n <= #occurrences (x,A) ) ; hence z in X by A1; ::_thesis: verum end; hence { x where x is Element of X : n <= #occurrences (x,A) } is List of X ; ::_thesis: verum end; let m be Nat; func ROUGH (A,n,m) -> List of X equals :ROUGH2: :: MMLQUERY:def 25 { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } if X <> {} ; consistency for b1 being List of X holds verum ; coherence ( X <> {} implies { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } is List of X ) proof assume A1: X <> {} ; ::_thesis: { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } is List of X { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } or z in X ) assume z in { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } ; ::_thesis: z in X then ex x being Element of X st ( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= m ) ; hence z in X by A1; ::_thesis: verum end; hence { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } is List of X ; ::_thesis: verum end; end; :: deftheorem ROUGH1 defines ROUGH MMLQUERY:def_24_:_ for X being set for A being FinSequence of bool X for n being Nat st X <> {} holds ROUGH (A,n) = { x where x is Element of X : n <= #occurrences (x,A) } ; :: deftheorem ROUGH2 defines ROUGH MMLQUERY:def_25_:_ for X being set for A being FinSequence of bool X for n, m being Nat st X <> {} holds ROUGH (A,n,m) = { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } ; definition let X be set ; let A be FinSequence of bool X; func ROUGH A -> List of X equals :: MMLQUERY:def 26 ROUGH (A,(max# A)); coherence ROUGH (A,(max# A)) is List of X ; end; :: deftheorem defines ROUGH MMLQUERY:def_26_:_ for X being set for A being FinSequence of bool X holds ROUGH A = ROUGH (A,(max# A)); theorem :: MMLQUERY:58 for X being set for n being Nat for A being FinSequence of bool X holds ROUGH (A,n,(len A)) = ROUGH (A,n) proof let X be set ; ::_thesis: for n being Nat for A being FinSequence of bool X holds ROUGH (A,n,(len A)) = ROUGH (A,n) let n be Nat; ::_thesis: for A being FinSequence of bool X holds ROUGH (A,n,(len A)) = ROUGH (A,n) let A be FinSequence of bool X; ::_thesis: ROUGH (A,n,(len A)) = ROUGH (A,n) thus ROUGH (A,n,(len A)) c= ROUGH (A,n) :: according to XBOOLE_0:def_10 ::_thesis: ROUGH (A,n) c= ROUGH (A,n,(len A)) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,n,(len A)) or z in ROUGH (A,n) ) assume A1: z in ROUGH (A,n,(len A)) ; ::_thesis: z in ROUGH (A,n) then z in { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= len A ) } by ROUGH2; then ex x being Element of X st ( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= len A ) ; then z in { x where x is Element of X : n <= #occurrences (x,A) } ; hence z in ROUGH (A,n) by A1, ROUGH1; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,n) or z in ROUGH (A,n,(len A)) ) assume A2: z in ROUGH (A,n) ; ::_thesis: z in ROUGH (A,n,(len A)) then z in { x where x is Element of X : n <= #occurrences (x,A) } by ROUGH1; then consider x being Element of X such that A3: ( z = x & n <= #occurrences (x,A) ) ; #occurrences (x,A) <= len A by Th21; then z in { x1 where x1 is Element of X : ( n <= #occurrences (x1,A) & #occurrences (x1,A) <= len A ) } by A3; hence z in ROUGH (A,n,(len A)) by A2, ROUGH2; ::_thesis: verum end; theorem :: MMLQUERY:59 for X being set for n, m being Nat for A being FinSequence of bool X st n <= m holds ROUGH (A,m) c= ROUGH (A,n) proof let X be set ; ::_thesis: for n, m being Nat for A being FinSequence of bool X st n <= m holds ROUGH (A,m) c= ROUGH (A,n) let n, m be Nat; ::_thesis: for A being FinSequence of bool X st n <= m holds ROUGH (A,m) c= ROUGH (A,n) let A be FinSequence of bool X; ::_thesis: ( n <= m implies ROUGH (A,m) c= ROUGH (A,n) ) assume Z0: n <= m ; ::_thesis: ROUGH (A,m) c= ROUGH (A,n) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,m) or z in ROUGH (A,n) ) assume A1: z in ROUGH (A,m) ; ::_thesis: z in ROUGH (A,n) then z in { x where x is Element of X : m <= #occurrences (x,A) } by ROUGH1; then consider a being Element of X such that A2: ( z = a & m <= #occurrences (a,A) ) ; n <= #occurrences (a,A) by Z0, A2, XXREAL_0:2; then z in { x where x is Element of X : n <= #occurrences (x,A) } by A2; hence z in ROUGH (A,n) by A1, ROUGH1; ::_thesis: verum end; theorem :: MMLQUERY:60 for X being set for A being FinSequence of bool X for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) proof let X be set ; ::_thesis: for A being FinSequence of bool X for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) let A be FinSequence of bool X; ::_thesis: for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) let n1, n2, m1, m2 be Nat; ::_thesis: ( n1 <= m1 & n2 <= m2 implies ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) ) assume Z1: n1 <= m1 ; ::_thesis: ( not n2 <= m2 or ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) ) assume Z2: n2 <= m2 ; ::_thesis: ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,m1,n2) or z in ROUGH (A,n1,m2) ) assume A1: z in ROUGH (A,m1,n2) ; ::_thesis: z in ROUGH (A,n1,m2) then z in { x where x is Element of X : ( m1 <= #occurrences (x,A) & #occurrences (x,A) <= n2 ) } by ROUGH2; then consider a being Element of X such that A2: ( z = a & m1 <= #occurrences (a,A) & #occurrences (a,A) <= n2 ) ; ( n1 <= #occurrences (a,A) & #occurrences (a,A) <= m2 ) by Z1, Z2, A2, XXREAL_0:2; then z in { x where x is Element of X : ( n1 <= #occurrences (x,A) & #occurrences (x,A) <= m2 ) } by A2; hence z in ROUGH (A,n1,m2) by A1, ROUGH2; ::_thesis: verum end; theorem :: MMLQUERY:61 for X being set for n, m being Nat for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n) proof let X be set ; ::_thesis: for n, m being Nat for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n) let n, m be Nat; ::_thesis: for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n) let A be FinSequence of bool X; ::_thesis: ROUGH (A,n,m) c= ROUGH (A,n) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,n,m) or z in ROUGH (A,n) ) assume A1: z in ROUGH (A,n,m) ; ::_thesis: z in ROUGH (A,n) then z in { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } by ROUGH2; then ex x being Element of X st ( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= m ) ; then z in { x where x is Element of X : n <= #occurrences (x,A) } ; hence z in ROUGH (A,n) by A1, ROUGH1; ::_thesis: verum end; theorem Th31: :: MMLQUERY:62 for X being set for A being FinSequence of bool X st A <> {} holds ROUGH (A,(len A)) = meet (rng A) proof let X be set ; ::_thesis: for A being FinSequence of bool X st A <> {} holds ROUGH (A,(len A)) = meet (rng A) let A be FinSequence of bool X; ::_thesis: ( A <> {} implies ROUGH (A,(len A)) = meet (rng A) ) assume A0: A <> {} ; ::_thesis: ROUGH (A,(len A)) = meet (rng A) thus ROUGH (A,(len A)) c= meet (rng A) :: according to XBOOLE_0:def_10 ::_thesis: meet (rng A) c= ROUGH (A,(len A)) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,(len A)) or z in meet (rng A) ) assume z in ROUGH (A,(len A)) ; ::_thesis: z in meet (rng A) then z in { x where x is Element of X : len A <= #occurrences (x,A) } by ROUGH1; then consider x being Element of X such that A3: ( z = x & len A <= #occurrences (x,A) ) ; #occurrences (x,A) <= len A by Th21; hence z in meet (rng A) by A0, A3, Th22, XXREAL_0:1; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet (rng A) or z in ROUGH (A,(len A)) ) assume A2: z in meet (rng A) ; ::_thesis: z in ROUGH (A,(len A)) then #occurrences (z,A) = len A by Th22; then z in { x where x is Element of X : len A <= #occurrences (x,A) } by A2; hence z in ROUGH (A,(len A)) by A2, ROUGH1; ::_thesis: verum end; theorem Th32: :: MMLQUERY:63 for X being set for A being FinSequence of bool X holds ROUGH (A,1) = Union A proof let X be set ; ::_thesis: for A being FinSequence of bool X holds ROUGH (A,1) = Union A let A be FinSequence of bool X; ::_thesis: ROUGH (A,1) = Union A thus ROUGH (A,1) c= Union A :: according to XBOOLE_0:def_10 ::_thesis: Union A c= ROUGH (A,1) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,1) or z in Union A ) assume z in ROUGH (A,1) ; ::_thesis: z in Union A then z in { x where x is Element of X : 1 <= #occurrences (x,A) } by ROUGH1; then consider x being Element of X such that A3: ( z = x & 1 <= #occurrences (x,A) ) ; 1 = 0 + 1 ; then #occurrences (x,A) > 0 by A3, NAT_1:13; then { i where i is Element of NAT : ( i in dom A & x in A . i ) } <> {} ; then consider s being set such that A2: s in { i where i is Element of NAT : ( i in dom A & x in A . i ) } by XBOOLE_0:def_1; consider i being Element of NAT such that A4: ( s = i & i in dom A & x in A . i ) by A2; thus z in Union A by A3, A4, CARD_5:2; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Union A or z in ROUGH (A,1) ) assume A6: z in Union A ; ::_thesis: z in ROUGH (A,1) then consider s being set such that A5: ( s in dom A & z in A . s ) by CARD_5:2; s in { i where i is Element of NAT : ( i in dom A & z in A . i ) } by A5; then card {s} c= #occurrences (z,A) by CARD_1:11, ZFMISC_1:31; then 1 c= #occurrences (z,A) by CARD_1:30; then 1 <= #occurrences (z,A) by NAT_1:39; then z in { x where x is Element of X : 1 <= #occurrences (x,A) } by A6; hence z in ROUGH (A,1) by A6, ROUGH1; ::_thesis: verum end; theorem :: MMLQUERY:64 for X being set for L1, L2 being List of X holds ROUGH (<*L1,L2*>,2) = L1 AND L2 proof let X be set ; ::_thesis: for L1, L2 being List of X holds ROUGH (<*L1,L2*>,2) = L1 AND L2 let L1, L2 be List of X; ::_thesis: ROUGH (<*L1,L2*>,2) = L1 AND L2 ( len <*L1,L2*> = 2 & rng <*L1,L2*> = {L1,L2} & meet {L1,L2} = L1 AND L2 ) by FINSEQ_1:44, FINSEQ_2:127, SETFAM_1:11; hence ROUGH (<*L1,L2*>,2) = L1 AND L2 by Th31; ::_thesis: verum end; theorem :: MMLQUERY:65 for X being set for L1, L2 being List of X holds ROUGH (<*L1,L2*>,1) = L1 OR L2 proof let X be set ; ::_thesis: for L1, L2 being List of X holds ROUGH (<*L1,L2*>,1) = L1 OR L2 let L1, L2 be List of X; ::_thesis: ROUGH (<*L1,L2*>,1) = L1 OR L2 ( len <*L1,L2*> = 2 & rng <*L1,L2*> = {L1,L2} & union {L1,L2} = L1 OR L2 & Union <*L1,L2*> = union (rng <*L1,L2*>) ) by CARD_3:def_4, FINSEQ_1:44, FINSEQ_2:127, ZFMISC_1:75; hence ROUGH (<*L1,L2*>,1) = L1 OR L2 by Th32; ::_thesis: verum end; begin definition attrc1 is strict ; struct ConstructorDB -> 1-sorted ; aggrConstructorDB(# carrier, Constrs, ref-operation #) -> ConstructorDB ; sel Constrs c1 -> List of the carrier of c1; sel ref-operation c1 -> Relation of the carrier of c1, the Constrs of c1; end; definition let X be 1-sorted ; mode List of X is List of the carrier of X; mode Operation of X is Operation of the carrier of X; end; definition let X be set ; let S be Subset of X; let R be Relation of X,S; func @ R -> Relation of X equals :: MMLQUERY:def 27 R; coherence R is Relation of X proof [:X,S:] c= [:X,X:] by ZFMISC_1:96; hence R is Relation of X by XBOOLE_1:1; ::_thesis: verum end; end; :: deftheorem defines @ MMLQUERY:def_27_:_ for X being set for S being Subset of X for R being Relation of X,S holds @ R = R; definition let X be ConstructorDB ; let a be Element of X; funca ref -> List of X equals :: MMLQUERY:def 28 a . (@ the ref-operation of X); coherence a . (@ the ref-operation of X) is List of X ; funca occur -> List of X equals :: MMLQUERY:def 29 a . ((@ the ref-operation of X) ~); coherence a . ((@ the ref-operation of X) ~) is List of X ; end; :: deftheorem defines ref MMLQUERY:def_28_:_ for X being ConstructorDB for a being Element of X holds a ref = a . (@ the ref-operation of X); :: deftheorem defines occur MMLQUERY:def_29_:_ for X being ConstructorDB for a being Element of X holds a occur = a . ((@ the ref-operation of X) ~); theorem Th10: :: MMLQUERY:66 for X being ConstructorDB for x, y being Element of X holds ( x in y ref iff y in x occur ) proof let X be ConstructorDB ; ::_thesis: for x, y being Element of X holds ( x in y ref iff y in x occur ) let x, y be Element of X; ::_thesis: ( x in y ref iff y in x occur ) hereby ::_thesis: ( y in x occur implies x in y ref ) assume x in y ref ; ::_thesis: y in x occur then [y,x] in @ the ref-operation of X by RELAT_1:169; then [x,y] in (@ the ref-operation of X) ~ by RELAT_1:def_7; hence y in x occur by RELAT_1:169; ::_thesis: verum end; assume y in x occur ; ::_thesis: x in y ref then [x,y] in (@ the ref-operation of X) ~ by RELAT_1:169; then [y,x] in @ the ref-operation of X by RELAT_1:def_7; hence x in y ref by RELAT_1:169; ::_thesis: verum end; definition let X be ConstructorDB ; attrX is ref-finite means :REFF: :: MMLQUERY:def 30 for x being Element of X holds x ref is finite ; end; :: deftheorem REFF defines ref-finite MMLQUERY:def_30_:_ for X being ConstructorDB holds ( X is ref-finite iff for x being Element of X holds x ref is finite ); registration cluster finite -> ref-finite for ConstructorDB ; coherence for b1 being ConstructorDB st b1 is finite holds b1 is ref-finite proof let X be ConstructorDB ; ::_thesis: ( X is finite implies X is ref-finite ) assume A1: the carrier of X is finite ; :: according to STRUCT_0:def_11 ::_thesis: X is ref-finite let x be Element of X; :: according to MMLQUERY:def_30 ::_thesis: x ref is finite thus x ref is finite by A1; ::_thesis: verum end; end; registration cluster non empty finite for ConstructorDB ; existence ex b1 being ConstructorDB st ( b1 is finite & not b1 is empty ) proof set X = the non empty finite set ; set C = the Subset of the non empty finite set ; set R = the Relation of the non empty finite set , the Subset of the non empty finite set ; take D = ConstructorDB(# the non empty finite set , the Subset of the non empty finite set , the Relation of the non empty finite set , the Subset of the non empty finite set #); ::_thesis: ( D is finite & not D is empty ) thus ( the carrier of D is finite & not the carrier of D is empty ) ; :: according to STRUCT_0:def_1,STRUCT_0:def_11 ::_thesis: verum end; end; registration let X be ref-finite ConstructorDB ; let x be Element of X; clusterx ref -> finite ; coherence x ref is finite by REFF; end; definition let X be ConstructorDB ; let A be FinSequence of the Constrs of X; func ATLEAST A -> List of X equals :DefAtleast: :: MMLQUERY:def 31 { x where x is Element of X : rng A c= x ref } if the carrier of X <> {} ; consistency for b1 being List of X holds verum ; coherence ( the carrier of X <> {} implies { x where x is Element of X : rng A c= x ref } is List of X ) proof assume A1: the carrier of X <> {} ; ::_thesis: { x where x is Element of X : rng A c= x ref } is List of X { x where x is Element of X : rng A c= x ref } c= the carrier of X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : rng A c= x ref } or z in the carrier of X ) assume z in { x where x is Element of X : rng A c= x ref } ; ::_thesis: z in the carrier of X then ex x being Element of X st ( z = x & rng A c= x ref ) ; hence z in the carrier of X by A1; ::_thesis: verum end; hence { x where x is Element of X : rng A c= x ref } is List of X ; ::_thesis: verum end; func ATMOST A -> List of X equals :DefAtmost: :: MMLQUERY:def 32 { x where x is Element of X : x ref c= rng A } if the carrier of X <> {} ; consistency for b1 being List of X holds verum ; coherence ( the carrier of X <> {} implies { x where x is Element of X : x ref c= rng A } is List of X ) proof assume A1: the carrier of X <> {} ; ::_thesis: { x where x is Element of X : x ref c= rng A } is List of X { x where x is Element of X : x ref c= rng A } c= the carrier of X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : x ref c= rng A } or z in the carrier of X ) assume z in { x where x is Element of X : x ref c= rng A } ; ::_thesis: z in the carrier of X then ex x being Element of X st ( z = x & x ref c= rng A ) ; hence z in the carrier of X by A1; ::_thesis: verum end; hence { x where x is Element of X : x ref c= rng A } is List of X ; ::_thesis: verum end; func EXACTLY A -> List of X equals :DefExactly: :: MMLQUERY:def 33 { x where x is Element of X : x ref = rng A } if the carrier of X <> {} ; consistency for b1 being List of X holds verum ; coherence ( the carrier of X <> {} implies { x where x is Element of X : x ref = rng A } is List of X ) proof assume A1: the carrier of X <> {} ; ::_thesis: { x where x is Element of X : x ref = rng A } is List of X { x where x is Element of X : x ref = rng A } c= the carrier of X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : x ref = rng A } or z in the carrier of X ) assume z in { x where x is Element of X : x ref = rng A } ; ::_thesis: z in the carrier of X then ex x being Element of X st ( z = x & x ref = rng A ) ; hence z in the carrier of X by A1; ::_thesis: verum end; hence { x where x is Element of X : x ref = rng A } is List of X ; ::_thesis: verum end; let n be Nat; func ATLEAST- (A,n) -> List of X equals :DefAtleastMinus: :: MMLQUERY:def 34 { x where x is Element of X : card ((rng A) \ (x ref)) <= n } if the carrier of X <> {} ; consistency for b1 being List of X holds verum ; coherence ( the carrier of X <> {} implies { x where x is Element of X : card ((rng A) \ (x ref)) <= n } is List of X ) proof assume A1: the carrier of X <> {} ; ::_thesis: { x where x is Element of X : card ((rng A) \ (x ref)) <= n } is List of X { x where x is Element of X : card ((rng A) \ (x ref)) <= n } c= the carrier of X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : card ((rng A) \ (x ref)) <= n } or z in the carrier of X ) assume z in { x where x is Element of X : card ((rng A) \ (x ref)) <= n } ; ::_thesis: z in the carrier of X then ex x being Element of X st ( z = x & card ((rng A) \ (x ref)) <= n ) ; hence z in the carrier of X by A1; ::_thesis: verum end; hence { x where x is Element of X : card ((rng A) \ (x ref)) <= n } is List of X ; ::_thesis: verum end; end; :: deftheorem DefAtleast defines ATLEAST MMLQUERY:def_31_:_ for X being ConstructorDB for A being FinSequence of the Constrs of X st the carrier of X <> {} holds ATLEAST A = { x where x is Element of X : rng A c= x ref } ; :: deftheorem DefAtmost defines ATMOST MMLQUERY:def_32_:_ for X being ConstructorDB for A being FinSequence of the Constrs of X st the carrier of X <> {} holds ATMOST A = { x where x is Element of X : x ref c= rng A } ; :: deftheorem DefExactly defines EXACTLY MMLQUERY:def_33_:_ for X being ConstructorDB for A being FinSequence of the Constrs of X st the carrier of X <> {} holds EXACTLY A = { x where x is Element of X : x ref = rng A } ; :: deftheorem DefAtleastMinus defines ATLEAST- MMLQUERY:def_34_:_ for X being ConstructorDB for A being FinSequence of the Constrs of X for n being Nat st the carrier of X <> {} holds ATLEAST- (A,n) = { x where x is Element of X : card ((rng A) \ (x ref)) <= n } ; definition let X be ref-finite ConstructorDB ; let A be FinSequence of the Constrs of X; let n be Nat; func ATMOST+ (A,n) -> List of X equals :DefAtmostPlus: :: MMLQUERY:def 35 { x where x is Element of X : card ((x ref) \ (rng A)) <= n } if the carrier of X <> {} ; consistency for b1 being List of X holds verum ; coherence ( the carrier of X <> {} implies { x where x is Element of X : card ((x ref) \ (rng A)) <= n } is List of X ) proof assume A1: the carrier of X <> {} ; ::_thesis: { x where x is Element of X : card ((x ref) \ (rng A)) <= n } is List of X { x where x is Element of X : card ((x ref) \ (rng A)) <= n } c= the carrier of X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : card ((x ref) \ (rng A)) <= n } or z in the carrier of X ) assume z in { x where x is Element of X : card ((x ref) \ (rng A)) <= n } ; ::_thesis: z in the carrier of X then ex x being Element of X st ( z = x & card ((x ref) \ (rng A)) <= n ) ; hence z in the carrier of X by A1; ::_thesis: verum end; hence { x where x is Element of X : card ((x ref) \ (rng A)) <= n } is List of X ; ::_thesis: verum end; let m be Nat; func EXACTLY+- (A,n,m) -> List of X equals :DefExactlyPlusMinus: :: MMLQUERY:def 36 { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } if the carrier of X <> {} ; consistency for b1 being List of X holds verum ; coherence ( the carrier of X <> {} implies { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } is List of X ) proof assume A1: the carrier of X <> {} ; ::_thesis: { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } is List of X { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } c= the carrier of X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } or z in the carrier of X ) assume z in { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } ; ::_thesis: z in the carrier of X then ex x being Element of X st ( z = x & card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) ; hence z in the carrier of X by A1; ::_thesis: verum end; hence { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } is List of X ; ::_thesis: verum end; end; :: deftheorem DefAtmostPlus defines ATMOST+ MMLQUERY:def_35_:_ for X being ref-finite ConstructorDB for A being FinSequence of the Constrs of X for n being Nat st the carrier of X <> {} holds ATMOST+ (A,n) = { x where x is Element of X : card ((x ref) \ (rng A)) <= n } ; :: deftheorem DefExactlyPlusMinus defines EXACTLY+- MMLQUERY:def_36_:_ for X being ref-finite ConstructorDB for A being FinSequence of the Constrs of X for n, m being Nat st the carrier of X <> {} holds EXACTLY+- (A,n,m) = { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } ; theorem Th41: :: MMLQUERY:67 for X being ConstructorDB for A being FinSequence of the Constrs of X holds ATLEAST- (A,0) = ATLEAST A proof let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X holds ATLEAST- (A,0) = ATLEAST A let A be FinSequence of the Constrs of X; ::_thesis: ATLEAST- (A,0) = ATLEAST A percases ( the carrier of X = {} or the carrier of X <> {} ) ; suppose the carrier of X = {} ; ::_thesis: ATLEAST- (A,0) = ATLEAST A then ( ATLEAST- (A,0) = {} & ATLEAST A = {} ) ; hence ATLEAST- (A,0) = ATLEAST A ; ::_thesis: verum end; supposeA0: the carrier of X <> {} ; ::_thesis: ATLEAST- (A,0) = ATLEAST A then A1: ATLEAST- (A,0) = { x where x is Element of X : card ((rng A) \ (x ref)) <= 0 } by DefAtleastMinus; A2: ATLEAST A = { x where x is Element of X : rng A c= x ref } by A0, DefAtleast; thus ATLEAST- (A,0) c= ATLEAST A :: according to XBOOLE_0:def_10 ::_thesis: ATLEAST A c= ATLEAST- (A,0) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATLEAST- (A,0) or z in ATLEAST A ) assume z in ATLEAST- (A,0) ; ::_thesis: z in ATLEAST A then consider x being Element of X such that A3: ( z = x & card ((rng A) \ (x ref)) <= 0 ) by A1; (rng A) \ (x ref) = {} by A3, NAT_1:3; then rng A c= x ref by XBOOLE_1:37; hence z in ATLEAST A by A3, A2; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATLEAST A or z in ATLEAST- (A,0) ) assume z in ATLEAST A ; ::_thesis: z in ATLEAST- (A,0) then consider x being Element of X such that A4: ( z = x & rng A c= x ref ) by A2; (rng A) \ (x ref) = {} by A4, XBOOLE_1:37; then card ((rng A) \ (x ref)) = 0 ; hence z in ATLEAST- (A,0) by A1, A4; ::_thesis: verum end; end; end; theorem Th42: :: MMLQUERY:68 for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y holds ATMOST+ (B,0) = ATMOST B proof let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds ATMOST+ (B,0) = ATMOST B let B be FinSequence of the Constrs of Y; ::_thesis: ATMOST+ (B,0) = ATMOST B percases ( the carrier of Y = {} or the carrier of Y <> {} ) ; suppose the carrier of Y = {} ; ::_thesis: ATMOST+ (B,0) = ATMOST B then ( ATMOST+ (B,0) = {} & ATMOST B = {} ) ; hence ATMOST+ (B,0) = ATMOST B ; ::_thesis: verum end; supposeA0: the carrier of Y <> {} ; ::_thesis: ATMOST+ (B,0) = ATMOST B then A1: ATMOST+ (B,0) = { y where y is Element of Y : card ((y ref) \ (rng B)) <= 0 } by DefAtmostPlus; A2: ATMOST B = { y where y is Element of Y : y ref c= rng B } by A0, DefAtmost; thus ATMOST+ (B,0) c= ATMOST B :: according to XBOOLE_0:def_10 ::_thesis: ATMOST B c= ATMOST+ (B,0) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATMOST+ (B,0) or z in ATMOST B ) assume z in ATMOST+ (B,0) ; ::_thesis: z in ATMOST B then consider y being Element of Y such that A3: ( z = y & card ((y ref) \ (rng B)) <= 0 ) by A1; (y ref) \ (rng B) = {} by A3, NAT_1:3; then y ref c= rng B by XBOOLE_1:37; hence z in ATMOST B by A3, A2; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATMOST B or z in ATMOST+ (B,0) ) assume z in ATMOST B ; ::_thesis: z in ATMOST+ (B,0) then consider y being Element of Y such that A4: ( z = y & y ref c= rng B ) by A2; (y ref) \ (rng B) = {} by A4, XBOOLE_1:37; then card ((y ref) \ (rng B)) = 0 ; hence z in ATMOST+ (B,0) by A1, A4; ::_thesis: verum end; end; end; theorem Th43: :: MMLQUERY:69 for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,0,0) = EXACTLY B proof let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,0,0) = EXACTLY B let B be FinSequence of the Constrs of Y; ::_thesis: EXACTLY+- (B,0,0) = EXACTLY B percases ( the carrier of Y = {} or the carrier of Y <> {} ) ; suppose the carrier of Y = {} ; ::_thesis: EXACTLY+- (B,0,0) = EXACTLY B then ( EXACTLY+- (B,0,0) = {} & EXACTLY B = {} ) ; hence EXACTLY+- (B,0,0) = EXACTLY B ; ::_thesis: verum end; supposeA0: the carrier of Y <> {} ; ::_thesis: EXACTLY+- (B,0,0) = EXACTLY B then A1: EXACTLY+- (B,0,0) = { y where y is Element of Y : ( card ((y ref) \ (rng B)) <= 0 & card ((rng B) \ (y ref)) <= 0 ) } by DefExactlyPlusMinus; A2: EXACTLY B = { y where y is Element of Y : y ref = rng B } by A0, DefExactly; thus EXACTLY+- (B,0,0) c= EXACTLY B :: according to XBOOLE_0:def_10 ::_thesis: EXACTLY B c= EXACTLY+- (B,0,0) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY+- (B,0,0) or z in EXACTLY B ) assume z in EXACTLY+- (B,0,0) ; ::_thesis: z in EXACTLY B then consider y being Element of Y such that A3: ( z = y & card ((y ref) \ (rng B)) <= 0 & card ((rng B) \ (y ref)) <= 0 ) by A1; ( (y ref) \ (rng B) = {} & (rng B) \ (y ref) = {} ) by A3, NAT_1:3; then ( y ref c= rng B & rng B c= y ref ) by XBOOLE_1:37; then y ref = rng B by XBOOLE_0:def_10; hence z in EXACTLY B by A3, A2; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY B or z in EXACTLY+- (B,0,0) ) assume z in EXACTLY B ; ::_thesis: z in EXACTLY+- (B,0,0) then consider y being Element of Y such that A4: ( z = y & y ref = rng B ) by A2; ( (y ref) \ (rng B) = {} & (rng B) \ (y ref) = {} ) by A4, XBOOLE_1:37; then ( card ((y ref) \ (rng B)) = 0 & card ((rng B) \ (y ref)) = 0 ) ; hence z in EXACTLY+- (B,0,0) by A1, A4; ::_thesis: verum end; end; end; theorem Th44: :: MMLQUERY:70 for n, m being Nat for X being ConstructorDB for A being FinSequence of the Constrs of X st n <= m holds ATLEAST- (A,n) c= ATLEAST- (A,m) proof let n, m be Nat; ::_thesis: for X being ConstructorDB for A being FinSequence of the Constrs of X st n <= m holds ATLEAST- (A,n) c= ATLEAST- (A,m) let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X st n <= m holds ATLEAST- (A,n) c= ATLEAST- (A,m) let A be FinSequence of the Constrs of X; ::_thesis: ( n <= m implies ATLEAST- (A,n) c= ATLEAST- (A,m) ) assume A1: n <= m ; ::_thesis: ATLEAST- (A,n) c= ATLEAST- (A,m) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATLEAST- (A,n) or z in ATLEAST- (A,m) ) assume A2: z in ATLEAST- (A,n) ; ::_thesis: z in ATLEAST- (A,m) then z in { x where x is Element of X : card ((rng A) \ (x ref)) <= n } by DefAtleastMinus; then consider x being Element of X such that A3: ( z = x & card ((rng A) \ (x ref)) <= n ) ; card ((rng A) \ (x ref)) <= m by A1, A3, XXREAL_0:2; then x in { x1 where x1 is Element of X : card ((rng A) \ (x1 ref)) <= m } ; hence z in ATLEAST- (A,m) by A2, A3, DefAtleastMinus; ::_thesis: verum end; theorem Th45: :: MMLQUERY:71 for n, m being Nat for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y st n <= m holds ATMOST+ (B,n) c= ATMOST+ (B,m) proof let n, m be Nat; ::_thesis: for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y st n <= m holds ATMOST+ (B,n) c= ATMOST+ (B,m) let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y st n <= m holds ATMOST+ (B,n) c= ATMOST+ (B,m) let B be FinSequence of the Constrs of Y; ::_thesis: ( n <= m implies ATMOST+ (B,n) c= ATMOST+ (B,m) ) assume A1: n <= m ; ::_thesis: ATMOST+ (B,n) c= ATMOST+ (B,m) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATMOST+ (B,n) or z in ATMOST+ (B,m) ) assume A2: z in ATMOST+ (B,n) ; ::_thesis: z in ATMOST+ (B,m) then z in { y where y is Element of Y : card ((y ref) \ (rng B)) <= n } by DefAtmostPlus; then consider y being Element of Y such that A3: ( z = y & card ((y ref) \ (rng B)) <= n ) ; card ((y ref) \ (rng B)) <= m by A1, A3, XXREAL_0:2; then y in { x1 where x1 is Element of Y : card ((x1 ref) \ (rng B)) <= m } ; hence z in ATMOST+ (B,m) by A2, A3, DefAtmostPlus; ::_thesis: verum end; theorem Th46: :: MMLQUERY:72 for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2) proof let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2) let B be FinSequence of the Constrs of Y; ::_thesis: for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2) let n1, n2, m1, m2 be Nat; ::_thesis: ( n1 <= m1 & n2 <= m2 implies EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2) ) assume A1: ( n1 <= m1 & n2 <= m2 ) ; ::_thesis: EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY+- (B,n1,n2) or z in EXACTLY+- (B,m1,m2) ) assume A2: z in EXACTLY+- (B,n1,n2) ; ::_thesis: z in EXACTLY+- (B,m1,m2) then z in { y where y is Element of Y : ( card ((y ref) \ (rng B)) <= n1 & card ((rng B) \ (y ref)) <= n2 ) } by DefExactlyPlusMinus; then consider y being Element of Y such that A3: ( z = y & card ((y ref) \ (rng B)) <= n1 & card ((rng B) \ (y ref)) <= n2 ) ; ( card ((y ref) \ (rng B)) <= m1 & card ((rng B) \ (y ref)) <= m2 ) by A1, A3, XXREAL_0:2; then y in { x1 where x1 is Element of Y : ( card ((x1 ref) \ (rng B)) <= m1 & card ((rng B) \ (x1 ref)) <= m2 ) } ; hence z in EXACTLY+- (B,m1,m2) by A2, A3, DefExactlyPlusMinus; ::_thesis: verum end; theorem :: MMLQUERY:73 for n being Nat for X being ConstructorDB for A being FinSequence of the Constrs of X holds ATLEAST A c= ATLEAST- (A,n) proof let n be Nat; ::_thesis: for X being ConstructorDB for A being FinSequence of the Constrs of X holds ATLEAST A c= ATLEAST- (A,n) let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X holds ATLEAST A c= ATLEAST- (A,n) let A be FinSequence of the Constrs of X; ::_thesis: ATLEAST A c= ATLEAST- (A,n) ( ATLEAST A = ATLEAST- (A,0) & 0 <= n ) by Th41, NAT_1:2; hence ATLEAST A c= ATLEAST- (A,n) by Th44; ::_thesis: verum end; theorem :: MMLQUERY:74 for n being Nat for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y holds ATMOST B c= ATMOST+ (B,n) proof let n be Nat; ::_thesis: for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y holds ATMOST B c= ATMOST+ (B,n) let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds ATMOST B c= ATMOST+ (B,n) let B be FinSequence of the Constrs of Y; ::_thesis: ATMOST B c= ATMOST+ (B,n) ( ATMOST B = ATMOST+ (B,0) & 0 <= n ) by Th42, NAT_1:2; hence ATMOST B c= ATMOST+ (B,n) by Th45; ::_thesis: verum end; theorem :: MMLQUERY:75 for n, m being Nat for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m) proof let n, m be Nat; ::_thesis: for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m) let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m) let B be FinSequence of the Constrs of Y; ::_thesis: EXACTLY B c= EXACTLY+- (B,n,m) ( EXACTLY B = EXACTLY+- (B,0,0) & 0 <= n & 0 <= m ) by Th43, NAT_1:2; hence EXACTLY B c= EXACTLY+- (B,n,m) by Th46; ::_thesis: verum end; theorem :: MMLQUERY:76 for X being ConstructorDB for A being FinSequence of the Constrs of X holds EXACTLY A = (ATLEAST A) AND (ATMOST A) proof let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X holds EXACTLY A = (ATLEAST A) AND (ATMOST A) let A be FinSequence of the Constrs of X; ::_thesis: EXACTLY A = (ATLEAST A) AND (ATMOST A) thus EXACTLY A c= (ATLEAST A) AND (ATMOST A) :: according to XBOOLE_0:def_10 ::_thesis: (ATLEAST A) AND (ATMOST A) c= EXACTLY A proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY A or z in (ATLEAST A) AND (ATMOST A) ) assume A1: z in EXACTLY A ; ::_thesis: z in (ATLEAST A) AND (ATMOST A) then z in { x where x is Element of X : x ref = rng A } by DefExactly; then consider x being Element of X such that A2: ( z = x & x ref = rng A ) ; z in { y where y is Element of X : rng A c= y ref } by A2; then A3: z in ATLEAST A by A1, DefAtleast; z in { y where y is Element of X : y ref c= rng A } by A2; then z in ATMOST A by A1, DefAtmost; hence z in (ATLEAST A) AND (ATMOST A) by A3, XBOOLE_0:def_4; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (ATLEAST A) AND (ATMOST A) or z in EXACTLY A ) assume A6: z in (ATLEAST A) AND (ATMOST A) ; ::_thesis: z in EXACTLY A then A4: ( z in ATLEAST A & z in ATMOST A ) by XBOOLE_0:def_4; then z in { y where y is Element of X : y ref c= rng A } by DefAtmost; then consider a being Element of X such that A5: ( z = a & a ref c= rng A ) ; z in { y where y is Element of X : rng A c= y ref } by A4, DefAtleast; then consider b being Element of X such that A7: ( z = b & rng A c= b ref ) ; ( z = a & a ref = rng A ) by A5, A7, XBOOLE_0:def_10; then z in { y where y is Element of X : y ref = rng A } ; hence z in EXACTLY A by A6, DefExactly; ::_thesis: verum end; theorem :: MMLQUERY:77 for n, m being Nat for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) proof let n, m be Nat; ::_thesis: for Y being ref-finite ConstructorDB for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) let B be FinSequence of the Constrs of Y; ::_thesis: EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) thus EXACTLY+- (B,n,m) c= (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) :: according to XBOOLE_0:def_10 ::_thesis: (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) c= EXACTLY+- (B,n,m) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY+- (B,n,m) or z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) ) assume A1: z in EXACTLY+- (B,n,m) ; ::_thesis: z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) then z in { x where x is Element of Y : ( card ((x ref) \ (rng B)) <= n & card ((rng B) \ (x ref)) <= m ) } by DefExactlyPlusMinus; then consider x being Element of Y such that A2: ( z = x & card ((x ref) \ (rng B)) <= n & card ((rng B) \ (x ref)) <= m ) ; z in { y where y is Element of Y : card ((rng B) \ (y ref)) <= m } by A2; then A3: z in ATLEAST- (B,m) by A1, DefAtleastMinus; z in { y where y is Element of Y : card ((y ref) \ (rng B)) <= n } by A2; then z in ATMOST+ (B,n) by A1, DefAtmostPlus; hence z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) by A3, XBOOLE_0:def_4; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) or z in EXACTLY+- (B,n,m) ) assume A6: z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) ; ::_thesis: z in EXACTLY+- (B,n,m) then A4: ( z in ATLEAST- (B,m) & z in ATMOST+ (B,n) ) by XBOOLE_0:def_4; then z in { y where y is Element of Y : card ((y ref) \ (rng B)) <= n } by DefAtmostPlus; then A5: ex y being Element of Y st ( z = y & card ((y ref) \ (rng B)) <= n ) ; z in { y where y is Element of Y : card ((rng B) \ (y ref)) <= m } by A4, DefAtleastMinus; then ex y being Element of Y st ( z = y & card ((rng B) \ (y ref)) <= m ) ; then z in { y where y is Element of Y : ( card ((y ref) \ (rng B)) <= n & card ((rng B) \ (y ref)) <= m ) } by A5; hence z in EXACTLY+- (B,n,m) by A6, DefExactlyPlusMinus; ::_thesis: verum end; theorem Th65: :: MMLQUERY:78 for X being ConstructorDB for A being FinSequence of the Constrs of X st A <> {} holds ATLEAST A = meet { (x occur) where x is Element of X : x in rng A } proof let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X st A <> {} holds ATLEAST A = meet { (x occur) where x is Element of X : x in rng A } let A be FinSequence of the Constrs of X; ::_thesis: ( A <> {} implies ATLEAST A = meet { (x occur) where x is Element of X : x in rng A } ) assume A <> {} ; ::_thesis: ATLEAST A = meet { (x occur) where x is Element of X : x in rng A } then rng A <> {} by RELAT_1:41; then consider s being set such that A1: s in rng A by XBOOLE_0:def_1; ( s in the Constrs of X & the Constrs of X c= the carrier of X ) by A1; then reconsider s = s as Element of X ; A2: s occur in { (x occur) where x is Element of X : x in rng A } by A1; thus ATLEAST A c= meet { (x occur) where x is Element of X : x in rng A } :: according to XBOOLE_0:def_10 ::_thesis: meet { (x occur) where x is Element of X : x in rng A } c= ATLEAST A proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATLEAST A or z in meet { (x occur) where x is Element of X : x in rng A } ) assume z in ATLEAST A ; ::_thesis: z in meet { (x occur) where x is Element of X : x in rng A } then z in { y where y is Element of X : rng A c= y ref } by DefAtleast; then consider a being Element of X such that A5: ( z = a & rng A c= a ref ) ; now__::_thesis:_for_Y_being_set_st_Y_in__{__(x_occur)_where_x_is_Element_of_X_:_x_in_rng_A__}__holds_ z_in_Y let Y be set ; ::_thesis: ( Y in { (x occur) where x is Element of X : x in rng A } implies z in Y ) assume Y in { (x occur) where x is Element of X : x in rng A } ; ::_thesis: z in Y then consider x being Element of X such that A3: ( Y = x occur & x in rng A ) ; thus z in Y by A5, A3, Th10; ::_thesis: verum end; hence z in meet { (x occur) where x is Element of X : x in rng A } by A2, SETFAM_1:def_1; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet { (x occur) where x is Element of X : x in rng A } or z in ATLEAST A ) assume A6: z in meet { (x occur) where x is Element of X : x in rng A } ; ::_thesis: z in ATLEAST A then A8: z in s occur by A2, SETFAM_1:def_1; then reconsider z = z as Element of X ; rng A c= z ref proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in rng A or s in z ref ) assume A7: s in rng A ; ::_thesis: s in z ref then s in the Constrs of X ; then reconsider s = s as Element of X ; s occur in { (x occur) where x is Element of X : x in rng A } by A7; then z in s occur by A6, SETFAM_1:def_1; hence s in z ref by Th10; ::_thesis: verum end; then z in { x where x is Element of X : rng A c= x ref } ; hence z in ATLEAST A by A8, DefAtleast; ::_thesis: verum end; theorem :: MMLQUERY:79 for X being ConstructorDB for A being FinSequence of the Constrs of X for c1, c2 being Element of X st A = <*c1,c2*> holds ATLEAST A = (c1 occur) AND (c2 occur) proof let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X for c1, c2 being Element of X st A = <*c1,c2*> holds ATLEAST A = (c1 occur) AND (c2 occur) let A be FinSequence of the Constrs of X; ::_thesis: for c1, c2 being Element of X st A = <*c1,c2*> holds ATLEAST A = (c1 occur) AND (c2 occur) let c1, c2 be Element of X; ::_thesis: ( A = <*c1,c2*> implies ATLEAST A = (c1 occur) AND (c2 occur) ) assume Z0: A = <*c1,c2*> ; ::_thesis: ATLEAST A = (c1 occur) AND (c2 occur) then A0: rng A = {c1,c2} by FINSEQ_2:127; A1: { (x occur) where x is Element of X : x in rng A } = {(c1 occur),(c2 occur)} proof thus { (x occur) where x is Element of X : x in rng A } c= {(c1 occur),(c2 occur)} :: according to XBOOLE_0:def_10 ::_thesis: {(c1 occur),(c2 occur)} c= { (x occur) where x is Element of X : x in rng A } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (x occur) where x is Element of X : x in rng A } or z in {(c1 occur),(c2 occur)} ) assume z in { (x occur) where x is Element of X : x in rng A } ; ::_thesis: z in {(c1 occur),(c2 occur)} then consider x being Element of X such that A2: ( z = x occur & x in rng A ) ; ( x = c1 or x = c2 ) by A0, A2, TARSKI:def_2; hence z in {(c1 occur),(c2 occur)} by A2, TARSKI:def_2; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {(c1 occur),(c2 occur)} or z in { (x occur) where x is Element of X : x in rng A } ) assume z in {(c1 occur),(c2 occur)} ; ::_thesis: z in { (x occur) where x is Element of X : x in rng A } then A3: ( z = c1 occur or z = c2 occur ) by TARSKI:def_2; ( c1 in rng A & c2 in rng A ) by A0, TARSKI:def_2; hence z in { (x occur) where x is Element of X : x in rng A } by A3; ::_thesis: verum end; thus ATLEAST A = meet { (x occur) where x is Element of X : x in rng A } by Z0, Th65 .= (c1 occur) AND (c2 occur) by A1, SETFAM_1:11 ; ::_thesis: verum end;