:: by Grzegorz Bancerek

::

:: Received December 18, 2011

:: Copyright (c) 2011-2018 Association of Mizar Users

notation
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

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

definition

let X be set ;

let O be Operation of X;

let L be List of X;

| L is List of X

for b_{1} being List of X holds

( b_{1} = | L iff b_{1} = union { (x . O) where x is Element of X : x in L } )

meet { (x . O) where x is Element of X : x in L } is List of X

{ 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

{ x where x is Element of X : ( card (x . O) = card (x . O2) & x in L ) } is List of X

{ x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L ) } is List of X

{ x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L ) } is List of X

{ x where x is Element of X : ( card (x . O) in card (x . O2) & x in L ) } is List of X

{ x where x is Element of X : ( card (x . O2) in card (x . O) & x in L ) } is List of X

end;
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 redefine func L | O -> List of X equals :: MMLQUERY:def 2

union { (x . O) where x is Element of X : x in L } ;

| L is List of X

proof end;

compatibility for b

( b

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

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

{ 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 ) } ;

{ 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 ) } ;

{ 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 ) } ;

{ 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 ) } ;

{ 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 ) } ;

{ x where x is Element of X : ( card (x . O2) in card (x . O) & x in L ) } is List of X

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

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

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

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

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

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

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

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

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;

{ x where x is Element of X : ( card (x . O) = n & x in L ) } is List of X

{ x where x is Element of X : ( card (x . O) c= n & x in L ) } is List of X

{ x where x is Element of X : ( n c= card (x . O) & x in L ) } is List of X

{ x where x is Element of X : ( card (x . O) in n & x in L ) } is List of X

{ x where x is Element of X : ( n in card (x . O) & x in L ) } is List of X

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

{ 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 ) } ;

{ 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 ) } ;

{ 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 ) } ;

{ 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 ) } ;

{ x where x is Element of X : ( n in card (x . O) & x in L ) } is List of X

proof 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 ) } ;

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

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

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

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

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 <> {} ) )

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

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

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

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)

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

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)

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)

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)

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)

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)

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)

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)

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)

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

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

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

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

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

redefine func A OR B -> List of X;

coherence

B OR is List of X

redefine func A BUTNOT B -> List of X;

coherence

B BUTNOT is List of X

end;
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: ORredefine func A OR B -> List of X;

coherence

B OR is List of X

proof end;

:: original: BUTNOTredefine func A BUTNOT B -> List of X;

coherence

B BUTNOT is List of X

proof 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)

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

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

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)

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

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

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

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;

ex b_{1} being Operation of X st

for L being List of X holds L | b_{1} = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }

for b_{1}, b_{2} being Operation of X st ( for L being List of X holds L | b_{1} = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) & ( for L being List of X holds L | b_{2} = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) holds

b_{1} = b_{2}

end;
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 for L being List of X holds L | it = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ;

ex b

for L being List of X holds L | b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def15 defines NOT MMLQUERY:def 15 :

for X being set

for O, b_{3} being Operation of X holds

( b_{3} = NOT O iff for L being List of X holds L | b_{3} = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } );

for X being set

for O, b

( b

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

definition

let X be set ;

let O1, O2 be Operation of X;

O2 AND is Operation of X

for b_{1} being Operation of X holds

( b_{1} = O2 AND iff for L being List of X holds L | b_{1} = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } )

O2 OR is Operation of X

for b_{1} being Operation of X holds

( b_{1} = O2 OR iff for L being List of X holds L | b_{1} = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } )

O2 BUTNOT is Operation of X

for b_{1} being Operation of X holds

( b_{1} = O2 BUTNOT iff for L being List of X holds L | b_{1} = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } )

O2 | is Operation of X

for b_{1} being Operation of X holds

( b_{1} = O2 | iff for L being List of X holds L | b_{1} = (L | O1) | O2 )

ex b_{1} being Operation of X st

for L being List of X holds L | b_{1} = union { ((x . O1) \& O2) where x is Element of X : x in L }

for b_{1}, b_{2} being Operation of X st ( for L being List of X holds L | b_{1} = union { ((x . O1) \& O2) where x is Element of X : x in L } ) & ( for L being List of X holds L | b_{2} = union { ((x . O1) \& O2) where x is Element of X : x in L } ) holds

b_{1} = b_{2}

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

O2 AND is Operation of X

proof end;

compatibility for b

( b

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

O2 OR is Operation of X

proof end;

compatibility for b

( b

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

O2 BUTNOT is Operation of X

proof end;

compatibility for b

( b

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 redefine func O1 | O2 -> Operation of X means :: MMLQUERY:def 19

for L being List of X holds L | it = (L | O1) | O2;

O2 | is Operation of X

proof end;

compatibility for b

( b

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 for L being List of X holds L | it = union { ((x . O1) \& O2) where x is Element of X : x in L } ;

ex b

for L being List of X holds L | b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines AND MMLQUERY:def 16 :

for X being set

for O1, O2, b_{4} being Operation of X holds

( b_{4} = O1 AND O2 iff for L being List of X holds L | b_{4} = union { ((x . O1) AND (x . O2)) where x is Element of X : x in L } );

for X being set

for O1, O2, b

( b

:: deftheorem defines OR MMLQUERY:def 17 :

for X being set

for O1, O2, b_{4} being Operation of X holds

( b_{4} = O1 OR O2 iff for L being List of X holds L | b_{4} = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } );

for X being set

for O1, O2, b

( b

:: deftheorem defines BUTNOT MMLQUERY:def 18 :

for X being set

for O1, O2, b_{4} being Operation of X holds

( b_{4} = O1 BUTNOT O2 iff for L being List of X holds L | b_{4} = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } );

for X being set

for O1, O2, b

( b

:: deftheorem defines | MMLQUERY:def 19 :

for X being set

for O1, O2, b_{4} being Operation of X holds

( b_{4} = O1 | O2 iff for L being List of X holds L | b_{4} = (L | O1) | O2 );

for X being set

for O1, O2, b

( b

:: deftheorem Def20 defines \& MMLQUERY:def 20 :

for X being set

for O1, O2, b_{4} being Operation of X holds

( b_{4} = O1 \& O2 iff for L being List of X holds L | b_{4} = union { ((x . O1) \& O2) where x is Element of X : x in L } );

for X being set

for O1, O2, b

( b

theorem :: MMLQUERY:31

theorem :: MMLQUERY:32

theorem :: MMLQUERY:33

theorem :: MMLQUERY:34

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

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

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

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)

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

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;

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

for X being set

for O being Operation of X holds

( O is filtering iff O c= id X );

registration
end;

registration

let X be set ;

let F be filtering Operation of X;

let O be Operation of X;

coherence

for b_{1} being Operation of X st b_{1} = F AND O holds

b_{1} is filtering

for b_{1} being Operation of X st b_{1} = O AND F holds

b_{1} is filtering
;

coherence

for b_{1} being Operation of X st b_{1} = F BUTNOT O holds

b_{1} is filtering

end;
let F be filtering Operation of X;

let O be Operation of X;

coherence

for b

b

proof end;

coherence for b

b

coherence

for b

b

proof end;

registration

let X be set ;

let F1, F2 be filtering Operation of X;

coherence

for b_{1} being Operation of X st b_{1} = F1 OR F2 holds

b_{1} is filtering

end;
let F1, F2 be filtering Operation of X;

coherence

for b

b

proof 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

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

for X being set

for F1, F2 being filtering Operation of X holds NOT (F1 AND F2) = (NOT F1) OR (NOT F2)

for F1, F2 being filtering Operation of X holds NOT (F1 AND F2) = (NOT F1) OR (NOT F2)

proof end;

definition

let A be FinSequence;

let a be object ;

card { i where i is Element of NAT : ( i in dom A & a in A . i ) } is Nat

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

card { i where i is Element of NAT : ( i in dom A & a in A . i ) } is Nat

proof 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 ) } ;

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 Th55: :: MMLQUERY:55

for A being FinSequence

for a being set holds

( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) )

for a being set holds

( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) )

proof end;

definition

let A be FinSequence;

ex b_{1} being Nat st

( ( for a being set holds #occurrences (a,A) <= b_{1} ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds

b_{1} <= n ) )

for b_{1}, b_{2} being Nat st ( for a being set holds #occurrences (a,A) <= b_{1} ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds

b_{1} <= n ) & ( for a being set holds #occurrences (a,A) <= b_{2} ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds

b_{2} <= n ) holds

b_{1} = b_{2}

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

ex b

( ( for a being set holds #occurrences (a,A) <= b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def23 defines max# MMLQUERY:def 23 :

for A being FinSequence

for b_{2} being Nat holds

( b_{2} = max# A iff ( ( for a being set holds #occurrences (a,A) <= b_{2} ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds

b_{2} <= n ) ) );

for A being FinSequence

for b

( b

b

definition

let X be set ;

let A be FinSequence of bool X;

let n be Nat;

for b_{1} being List of X holds verum
;

coherence

( X <> {} implies { x where x is Element of X : n <= #occurrences (x,A) } is List of X )

for b_{1} 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 )

end;
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 { x where x is Element of X : n <= #occurrences (x,A) } if X <> {}

;

for b

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 { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } if X <> {}

;

for b

coherence

( X <> {} implies { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } is List of X )

proof 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) } ;

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

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

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)

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)

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)

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)

for n, m being Nat

for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n)

proof end;

definition

attr c_{1} is strict ;

struct ConstructorDB -> 1-sorted ;

aggr ConstructorDB(# carrier, Constrs, ref-operation #) -> ConstructorDB ;

sel Constrs c_{1} -> List of the carrier of c_{1};

sel ref-operation c_{1} -> Relation of the carrier of c_{1}, the Constrs of c_{1};

end;
struct ConstructorDB -> 1-sorted ;

aggr ConstructorDB(# carrier, Constrs, ref-operation #) -> ConstructorDB ;

sel Constrs c

sel ref-operation c

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;
mode List of X is List of the carrier of X;

mode Operation of X is Operation of the carrier of X;

definition

let X be set ;

let S be Subset of X;

let R be Relation of X,S;

coherence

R is Relation of X

end;
let S be Subset of X;

let R be Relation of X,S;

coherence

R is Relation of X

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

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;

coherence

a . (@ the ref-operation of X) is List of X ;

coherence

a . ((@ the ref-operation of X) ~) is List of X ;

end;
let a be Element of X;

coherence

a . (@ the ref-operation of X) is List of X ;

coherence

a . ((@ the ref-operation of X) ~) is List of X ;

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

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

for X being ConstructorDB

for a being Element of X holds a occur = a . ((@ the ref-operation of X) ~);

definition

let X be ConstructorDB ;

end;
attr X is ref-finite means :Def30: :: MMLQUERY:def 30

for x being Element of X holds x ref is finite ;

for x being Element of X holds x ref is finite ;

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

for X being ConstructorDB holds

( X is ref-finite iff for x being Element of X holds x ref is finite );

registration
end;

registration
end;

registration
end;

definition

let X be ConstructorDB ;

let A be FinSequence of the Constrs of X;

for b_{1} 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 )

for b_{1} 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 )

for b_{1} 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 )

for b_{1} 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 )

end;
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 { x where x is Element of X : rng A c= x ref } if the carrier of X <> {}

;

for b

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 { x where x is Element of X : x ref c= rng A } if the carrier of X <> {}

;

for b

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 { x where x is Element of X : x ref = rng A } if the carrier of X <> {}

;

for b

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 { x where x is Element of X : card ((rng A) \ (x ref)) <= n } if the carrier of X <> {}

;

for b

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;

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

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

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

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

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;

for b_{1} 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 )

for b_{1} 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 )

end;
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 { x where x is Element of X : card ((x ref) \ (rng A)) <= n } if the carrier of X <> {}

;

for b

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 { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } if the carrier of X <> {}

;

for b

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;

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

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

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

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

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

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)

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)

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)

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)

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)

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)

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)

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

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 }

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)

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;