:: 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;