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


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) )
proofend;

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
proofend;
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 )
proofend;

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
proofend;
compatibility
 for b1 being List of X holds
( b1 = | L iff b1 = union  {  (x . O) where x is Element of X : x in L  }  )
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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 &amp; x . O <> {} ) )
proofend;

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

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

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 &amp; L1 c= L2 holds
L1 WHEREge (O,n) c= L2 WHERE O
proofend;

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

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

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

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 &amp; L1 c= L2 holds
L1 WHEREeq (O,n) c= L2 WHERE O
proofend;

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)
proofend;

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))
proofend;

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 &amp; L1 c= L2 &amp; O1 c= O2 holds
L1 WHEREge (O1,m) c= L2 WHEREge (O2,n)
proofend;

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 &amp; L1 c= L2 &amp; O1 c= O2 holds
L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n)
proofend;

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 &amp; L1 c= L2 &amp; O1 c= O2 holds
L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)
proofend;

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 &amp; L1 c= L2 &amp; O1 c= O2 holds
L1 WHERElt (O2,n) c= L2 WHERElt (O1,m)
proofend;

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 &amp; L1 c= L2 &amp; O c= O3 holds
L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1)
proofend;

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 &amp; L1 c= L2 &amp; O c= O3 holds
L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1)
proofend;

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 &amp; L1 c= L2 &amp; O c= O3 holds
L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)
proofend;

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 &amp; L1 c= L2 &amp; O c= O3 holds
L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2)
proofend;

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

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 &amp; L1 c= L2 holds
L1 WHERE O1 c= L2 WHERE O2
proofend;

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 &amp; b in L ) )
proofend;

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
proofend;
:: original:OR
redefine funcA OR B ->  List of X;
coherence
 B OR is List of X
proofend;
:: original:BUTNOT
redefine funcA BUTNOT B ->  List of X;
coherence
 B BUTNOT is List of X
proofend;
end;

theorem Th17: :: MMLQUERY:24
for X being set
for L1, L2 being List of X
for O being Operation of X st L1 <> {} &amp; L2 <> {} holds
(L1 OR L2) \&amp; O = (L1 \&amp; O) AND (L2 \&amp; O)
proofend;

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 &amp; O1 c= O2 holds
L1 | O1 c= L2 | O2
proofend;

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 \&amp; O1 c= L \&amp; O2
proofend;

theorem :: MMLQUERY:27
for X being set
for L being List of X
for O1, O2 being Operation of X holds L \&amp; (O1 AND O2) = (L \&amp; O1) AND (L \&amp; O2)
proofend;

theorem :: MMLQUERY:28
for X being set
for L1, L2 being List of X
for O being Operation of X st L1 <> {} &amp; L1 c= L2 holds
L2 \&amp; O c= L1 \&amp; O
proofend;

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

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

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  }
proofend;
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  }  ) &amp; ( 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
proofend;
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
proofend;
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  }  )
proofend;
:: 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
proofend;
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  }  )
proofend;
:: 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
proofend;
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  }  )
proofend;
:: 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
proofend;
compatibility
 for b1 being Operation of X holds
( b1 = O2 | iff for L being List of X holds L | b1 = (L | O1) | O2 )
proofend;
funcO1 \&amp; O2 ->  Operation of X means :DefAmp: :: MMLQUERY:def 20
 for L being List of X holds L | it = union  {  ((x . O1) \&amp; 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) \&amp; O2) where x is Element of X : x in L  }
proofend;
uniqueness
 for b1, b2 being Operation of X st ( for L being List of X holds L | b1 = union  {  ((x . O1) \&amp; O2) where x is Element of X : x in L  }  ) &amp; ( for L being List of X holds L | b2 = union  {  ((x . O1) \&amp; O2) where x is Element of X : x in L  }  ) holds
b1 = b2
proofend;
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 \&amp; MMLQUERY:def_20_:_
 for X being set
for O1, O2, b4 being Operation of X holds
( b4 = O1 \&amp; O2 iff for L being List of X holds L | b4 = union  {  ((x . O1) \&amp; 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 \&amp; O2) = (x . O1) \&amp; O2
proofend;

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 &amp; z in X &amp; z nin dom O ) )
proofend;

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

theorem Th6: :: MMLQUERY:38
for X being set
for O being Operation of X holds dom (NOT (NOT O)) = dom O
proofend;

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

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)
proofend;

theorem :: MMLQUERY:41
for X being set
for O being Operation of X holds NOT (NOT (NOT O)) = NOT O
proofend;

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)
proofend;

theorem :: MMLQUERY:43
for X being set
for O1, O2 being Operation of X holds NOT (O1 OR O2) = (NOT O1) AND (NOT O2)
proofend;

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

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) )
proofend;

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

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

theorem :: MMLQUERY:48
for X being set
for F being filtering Operation of X holds NOT (NOT F) = F
proofend;

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)
proofend;

theorem Th71: :: MMLQUERY:50
for X being set
for O being Operation of X holds dom (O OR (NOT O)) = X
proofend;

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

theorem Th72: :: MMLQUERY:52
for X being set
for O being Operation of X holds O AND (NOT O) = {}
proofend;

theorem :: MMLQUERY:53
for X being set
for O1, O2 being Operation of X holds (O1 OR O2) AND (NOT O1) c= O2
proofend;

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 &amp; a in A . i )  }  ;
coherence
 card  {  i where i is Element of NAT : ( i in dom A &amp; a in A . i )  }  is Nat
proofend;
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 &amp; a in A . i )  }  ;

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

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

definition
let A be FinSequence;
func max# A ->  Nat means :MAX: :: MMLQUERY:def 23
( ( for a being set holds #occurrences (a,A) <= it ) &amp; ( 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 ) &amp; ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
b1 <= n ) )
proofend;
uniqueness
 for b1, b2 being Nat st ( for a being set holds #occurrences (a,A) <= b1 ) &amp; ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
b1 <= n ) &amp; ( for a being set holds #occurrences (a,A) <= b2 ) &amp; ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
b2 <= n ) holds
b1 = b2
proofend;
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 ) &amp; ( 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
proofend;

theorem :: MMLQUERY:57
for A being FinSequence
for a being set st #occurrences (a,A) = len A holds
max# A = len A
proofend;

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 )
proofend;
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) &amp; #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) &amp; #occurrences (x,A) <= m )  }  is List of X )
proofend;
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) &amp; #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)
proofend;

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)
proofend;

theorem :: MMLQUERY:60
for X being set
for A being FinSequence of bool X
for n1, n2, m1, m2 being Nat st n1 <= m1 &amp; n2 <= m2 holds
ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)
proofend;

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)
proofend;

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)
proofend;

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

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

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

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
proofend;
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 )
proofend;

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

registration
cluster non empty finite for ConstructorDB ;
existence
 ex b1 being ConstructorDB st
( b1 is finite &amp; not b1 is empty )
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
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 &amp; 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 &amp; card ((rng A) \ (x ref)) <= m )  }  is List of X )
proofend;
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 &amp; 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
proofend;

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

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

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)
proofend;

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)
proofend;

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 &amp; n2 <= m2 holds
EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

theorem :: MMLQUERY:76
for X being ConstructorDB
for A being FinSequence of the Constrs of X holds EXACTLY A = (ATLEAST A) AND (ATMOST A)
proofend;

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))
proofend;

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  }
proofend;

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)
proofend;