:: Semantic of MML Query
:: by Grzegorz Bancerek
::
:: Received December 18, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users


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 ;
pred x,y in R means :: MMLQUERY:def 1
[x,y] in R;
end;

:: deftheorem 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 Th1: :: MMLQUERY:1
for R1, R2 being Relation holds
( R1 c= R2 iff for z being object holds Im (R1,z) c= Im (R2,z) )
proof 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 func x . O -> List of X;
coherence
. x is List of X
proof end;
end;

theorem Th2: :: 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 ) by RELAT_1:169;

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 func L | 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 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 end;
func L \& 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 end;
func L 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 end;
let O2 be Operation of X;
func L 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 end;
func L 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 end;
func L 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 end;
func L 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 end;
func L 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 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;
func L 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 end;
func L 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 end;
func L 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 end;
func L 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 end;
func L 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 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 Th3: :: 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 end;

theorem Th4: :: MMLQUERY:4
for X being set
for L being List of X
for O being Operation of X holds L WHERE O c= L by Th3;

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

theorem Th6: :: 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 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 end;

theorem Th8: :: 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 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 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 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 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 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 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 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 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 end;

theorem :: MMLQUERY:17
for X being set
for L1, L2 being List of X
for O, O1, O2, 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 end;

theorem :: MMLQUERY:18
for X being set
for L1, L2 being List of X
for O, O1, O2, 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 end;

theorem :: MMLQUERY:19
for X being set
for L1, L2 being List of X
for O, O1, O2, 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 end;

theorem :: MMLQUERY:20
for X being set
for L1, L2 being List of X
for O, O1, O2, 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 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 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 end;

theorem Th23: :: 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 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 func A AND B -> List of X;
coherence
B AND is List of X
proof end;
:: original: OR
redefine func A OR B -> List of X;
coherence
B OR is List of X
proof end;
:: original: BUTNOT
redefine func A BUTNOT B -> List of X;
coherence
B BUTNOT is List of X
proof end;
end;

theorem Th24: :: 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 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 end;

theorem Th26: :: 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 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 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 end;

theorem Th29: :: 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 end;

theorem Th30: :: 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 end;

definition
let X be set ;
let O be Operation of X;
func NOT O -> Operation of X means :Def15: :: 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 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 end;
end;

:: deftheorem Def15 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 func O1 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 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 end;
:: original: OR
redefine func O1 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 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 end;
:: original: BUTNOT
redefine func O1 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 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 end;
:: original: |
redefine func O1 | 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 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 end;
func O1 \& O2 -> Operation of X means :Def20: :: 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 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 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 Def20 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 Th35: :: 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 end;

theorem Th36: :: MMLQUERY:36
for X being set
for O being Operation of X
for z, s being object holds
( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )
proof end;

theorem Th37: :: MMLQUERY:37
for X being set
for O being Operation of X holds NOT O = id (X \ (dom O))
proof end;

theorem Th38: :: MMLQUERY:38
for X being set
for O being Operation of X holds dom (NOT (NOT O)) = dom O
proof 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 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 end;

theorem :: MMLQUERY:41
for X being set
for O being Operation of X holds NOT (NOT (NOT O)) = NOT O
proof 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 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 end;

theorem :: MMLQUERY:44
for X being set
for O, O1, O2 being Operation of X st dom O1 = X & dom O2 = X holds
(O1 OR O2) \& O = (O1 \& O) AND (O2 \& O)
proof end;

definition
let X be set ;
let O be Operation of X;
attr O is filtering means :Def21: :: MMLQUERY:def 21
O c= id X;
end;

:: deftheorem Def21 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 Th45: :: MMLQUERY:45
for X being set
for O being Operation of X holds
( O is filtering iff O = id (dom O) )
proof end;

registration
let X be set ;
let O be Operation of X;
cluster NOT O -> filtering ;
coherence
NOT O is filtering
proof 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 end;
end;

registration
let X be set ;
let F be filtering Operation of X;
let O be Operation of X;
cluster O AND -> filtering for Operation of X;
coherence
for b1 being Operation of X st b1 = F AND O holds
b1 is filtering
proof end;
cluster F AND -> filtering for Operation of X;
coherence
for b1 being Operation of X st b1 = O AND F holds
b1 is filtering ;
cluster O BUTNOT -> filtering for Operation of X;
coherence
for b1 being Operation of X st b1 = F BUTNOT O holds
b1 is filtering
proof end;
end;

registration
let X be set ;
let F1, F2 be filtering Operation of X;
cluster F2 OR -> filtering for Operation of X;
coherence
for b1 being Operation of X st b1 = F1 OR F2 holds
b1 is filtering
proof end;
end;

theorem Th46: :: 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 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 end;

theorem :: MMLQUERY:48
for X being set
for F being filtering Operation of X holds NOT (NOT F) = F
proof 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 end;

theorem Th50: :: MMLQUERY:50
for X being set
for O being Operation of X holds dom (O OR (NOT O)) = X
proof end;

theorem :: MMLQUERY:51
for X being set
for F being filtering Operation of X holds F OR (NOT F) = id X
proof end;

theorem Th52: :: MMLQUERY:52
for X being set
for O being Operation of X holds O AND (NOT O) = {}
proof 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 end;

definition
let A be FinSequence;
let a be object ;
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 end;
end;

:: deftheorem defines #occurrences MMLQUERY:def 22 :
for A being FinSequence
for a being object holds #occurrences (a,A) = card { i where i is Element of NAT : ( i in dom A & a in A . i ) } ;

theorem Th54: :: MMLQUERY:54
for A being FinSequence
for a being set holds #occurrences (a,A) <= len A
proof end;

theorem Th55: :: MMLQUERY:55
for A being FinSequence
for a being set holds
( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) )
proof end;

definition
let A be FinSequence;
func max# A -> Nat means :Def23: :: 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 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 end;
end;

:: deftheorem Def23 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 Th56: :: MMLQUERY:56
for A being FinSequence holds max# A <= len A
proof end;

theorem :: MMLQUERY:57
for A being FinSequence
for a being set st #occurrences (a,A) = len A holds
max# A = len A
proof 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 :Def24: :: 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 end;
let m be Nat;
func ROUGH (A,n,m) -> List of X equals :Def25: :: 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 end;
end;

:: deftheorem Def24 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 Def25 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 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 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 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 end;

theorem Th62: :: MMLQUERY:62
for X being set
for A being FinSequence of bool X st A <> {} holds
ROUGH (A,(len A)) = meet (rng A)
proof end;

theorem Th63: :: MMLQUERY:63
for X being set
for A being FinSequence of bool X holds ROUGH (A,1) = Union A
proof end;

theorem :: MMLQUERY:64
for X being set
for L1, L2 being List of X holds ROUGH (<*L1,L2*>,2) = L1 AND L2
proof end;

theorem :: MMLQUERY:65
for X being set
for L1, L2 being List of X holds ROUGH (<*L1,L2*>,1) = L1 OR L2
proof end;

definition
attr c1 is strict ;
struct ConstructorDB -> 1-sorted ;
aggr ConstructorDB(# 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 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;
func a 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 ;
func a 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 Th66: :: MMLQUERY:66
for X being ConstructorDB
for x, y being Element of X holds
( x in y ref iff y in x occur )
proof end;

definition
let X be ConstructorDB ;
attr X is ref-finite means :Def30: :: MMLQUERY:def 30
 for x being Element of X holds x ref is finite ;
end;

:: deftheorem Def30 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 end;
end;

registration
cluster non empty finite for ConstructorDB ;
existence
ex b1 being ConstructorDB st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
let X be ref-finite ConstructorDB ;
let x be Element of X;
cluster x ref -> finite ;
coherence
x ref is finite by Def30;
end;

definition
let X be ConstructorDB ;
let A be FinSequence of the Constrs of X;
func ATLEAST A -> List of X equals :Def31: :: 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 end;
func ATMOST A -> List of X equals :Def32: :: 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 end;
func EXACTLY A -> List of X equals :Def33: :: 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 end;
let n be Nat;
func ATLEAST- (A,n) -> List of X equals :Def34: :: 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 end;
end;

:: deftheorem Def31 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 Def32 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 Def33 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 Def34 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 :Def35: :: 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 end;
let m be Nat;
func EXACTLY+- (A,n,m) -> List of X equals :Def36: :: 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 end;
end;

:: deftheorem Def35 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 Def36 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 Th67: :: MMLQUERY:67
for X being ConstructorDB
for A being FinSequence of the Constrs of X holds ATLEAST- (A,0) = ATLEAST A
proof end;

theorem Th68: :: MMLQUERY:68
for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds ATMOST+ (B,0) = ATMOST B
proof end;

theorem Th69: :: 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 end;

theorem Th70: :: 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 end;

theorem Th71: :: 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 end;

theorem Th72: :: 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 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 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 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 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 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 end;

theorem Th78: :: 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 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 end;