mmlquery.miz
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;
::
MMLQUERY:def1
pred x,y
in R means
[x, y]
in R;
end
notation
let x,y,R be
set;
antonym x,y
nin R for x,y
in R;
end
reserve X,Y,z,s for
set,
L,L1,L2,A,B for
List of X,
x for
Element of X,
O,O1,O2,O3 for
Operation of X,
a,b,y for
Element of X,
n,m for
Nat;
theorem ::
MMLQUERY:1
Th1: for R1,R2 be
Relation holds R1
c= R2 iff for z be
object holds (
Im (R1,z))
c= (
Im (R2,z))
proof
let R1,R2 be
Relation;
hereby
assume
A1: R1
c= R2;
let z be
object;
thus (
Im (R1,z))
c= (
Im (R2,z))
proof
let s be
object;
assume s
in (
Im (R1,z));
then
consider v be
object such that
A2:
[v, s]
in R1 & v
in
{z} by
RELAT_1:def 13;
thus thesis by
A1,
A2,
RELAT_1:def 13;
end;
end;
assume
A3: for z be
object holds (
Im (R1,z))
c= (
Im (R2,z));
let a,b be
object;
assume
[a, b]
in R1;
then b
in (
Im (R1,a)) & (
Im (R1,a))
c= (
Im (R2,a)) by
A3,
RELAT_1: 169;
hence thesis by
RELAT_1: 169;
end;
notation
let X, O, x;
synonym x
. O for
Im (O,x);
end
definition
let X, O, x;
:: original:
.
redefine
func x
. O ->
List of X ;
coherence
proof
(x
. O)
= (O
.:
{x});
hence (x
. O) is
Subset of X;
end;
end
theorem ::
MMLQUERY:2
Th2: (x,y)
in O iff y
in (x
. O) by
RELAT_1: 169;
notation
let X, O, L;
synonym L
| O for O
.: L;
end
definition
let X, O, L;
:: original:
|
redefine
::
MMLQUERY:def2
func L
| O ->
List of X equals (
union { (x
. O) : x
in L });
coherence
proof
thus (O
.: L) is
Subset of X;
end;
compatibility
proof
(
union { (x
. O) : x
in L })
= (L
| O)
proof
thus (
union { (x
. O) : x
in L })
c= (L
| O)
proof
let z be
object;
assume z
in (
union { (x
. O) : x
in L });
then
consider Y be
set such that
A1: z
in Y & Y
in { (x
. O) : x
in L } by
TARSKI:def 4;
consider x such that
A2: Y
= (x
. O) & x
in L by
A1;
[x, z]
in O by
A1,
A2,
RELAT_1: 169;
hence thesis by
A2,
RELAT_1:def 13;
end;
thus (L
| O)
c= (
union { (x
. O) : x
in L })
proof
let z be
object;
assume z
in (L
| O);
then
consider y be
object such that
A3:
[y, z]
in O & y
in L by
RELAT_1:def 13;
reconsider y as
Element of X by
A3;
z
in (y
. O) & (y
. O)
in { (x
. O) : x
in L } by
A3,
RELAT_1: 169;
hence thesis by
TARSKI:def 4;
end;
end;
hence thesis;
end;
::
MMLQUERY:def3
func L
\& O ->
List of X equals (
meet { (x
. O) : x
in L });
coherence
proof
(
meet { (x
. O) : x
in L })
c= X
proof
let z be
object;
assume
A4: z
in (
meet { (x
. O) : x
in L });
then { (x
. O) : x
in L }
<>
{} by
SETFAM_1:def 1;
then
consider Y be
object such that
A5: Y
in { (x
. O) : x
in L } by
XBOOLE_0:def 1;
consider x such that
A6: Y
= (x
. O) & x
in L by
A5;
z
in (x
. O) by
A4,
A5,
A6,
SETFAM_1:def 1;
hence thesis;
end;
hence thesis;
end;
::
MMLQUERY:def4
func L
WHERE O ->
List of X equals { x : ex y st (x,y)
in O & x
in L };
coherence
proof
{ x : ex y st (x,y)
in O & x
in L }
c= X
proof
let z be
object;
assume z
in { x : ex y st (x,y)
in O & x
in L };
then
consider x such that
A7: z
= x & ex y st (x,y)
in O & x
in L;
thus thesis by
A7;
end;
hence thesis;
end;
let O2 be
Operation of X;
::
MMLQUERY:def5
func L
WHEREeq (O,O2) ->
List of X equals { x : (
card (x
. O))
= (
card (x
. O2)) & x
in L };
coherence
proof
{ x : (
card (x
. O))
= (
card (x
. O2)) & x
in L }
c= X
proof
let z be
object;
assume z
in { x : (
card (x
. O))
= (
card (x
. O2)) & x
in L };
then ex x st z
= x & (
card (x
. O))
= (
card (x
. O2)) & x
in L;
hence thesis;
end;
hence thesis;
end;
::
MMLQUERY:def6
func L
WHEREle (O,O2) ->
List of X equals { x : (
card (x
. O))
c= (
card (x
. O2)) & x
in L };
coherence
proof
{ x : (
card (x
. O))
c= (
card (x
. O2)) & x
in L }
c= X
proof
let z be
object;
assume z
in { x : (
card (x
. O))
c= (
card (x
. O2)) & x
in L };
then ex x st z
= x & (
card (x
. O))
c= (
card (x
. O2)) & x
in L;
hence thesis;
end;
hence thesis;
end;
::
MMLQUERY:def7
func L
WHEREge (O,O2) ->
List of X equals { x : (
card (x
. O2))
c= (
card (x
. O)) & x
in L };
coherence
proof
{ x : (
card (x
. O2))
c= (
card (x
. O)) & x
in L }
c= X
proof
let z be
object;
assume z
in { x : (
card (x
. O2))
c= (
card (x
. O)) & x
in L };
then ex x st z
= x & (
card (x
. O2))
c= (
card (x
. O)) & x
in L;
hence thesis;
end;
hence thesis;
end;
::
MMLQUERY:def8
func L
WHERElt (O,O2) ->
List of X equals { x : (
card (x
. O))
in (
card (x
. O2)) & x
in L };
coherence
proof
{ x : (
card (x
. O))
in (
card (x
. O2)) & x
in L }
c= X
proof
let z be
object;
assume z
in { x : (
card (x
. O))
in (
card (x
. O2)) & x
in L };
then ex x st z
= x & (
card (x
. O))
in (
card (x
. O2)) & x
in L;
hence thesis;
end;
hence thesis;
end;
::
MMLQUERY:def9
func L
WHEREgt (O,O2) ->
List of X equals { x : (
card (x
. O2))
in (
card (x
. O)) & x
in L };
coherence
proof
{ x : (
card (x
. O2))
in (
card (x
. O)) & x
in L }
c= X
proof
let z be
object;
assume z
in { x : (
card (x
. O2))
in (
card (x
. O)) & x
in L };
then ex x st z
= x & (
card (x
. O2))
in (
card (x
. O)) & x
in L;
hence thesis;
end;
hence thesis;
end;
end
definition
let X, L, O, n;
::
MMLQUERY:def10
func L
WHEREeq (O,n) ->
List of X equals { x : (
card (x
. O))
= n & x
in L };
coherence
proof
{ x : (
card (x
. O))
= n & x
in L }
c= X
proof
let z be
object;
assume z
in { x : (
card (x
. O))
= n & x
in L };
then ex x st z
= x & (
card (x
. O))
= n & x
in L;
hence thesis;
end;
hence thesis;
end;
::
MMLQUERY:def11
func L
WHEREle (O,n) ->
List of X equals { x : (
card (x
. O))
c= n & x
in L };
coherence
proof
{ x : (
card (x
. O))
c= n & x
in L }
c= X
proof
let z be
object;
assume z
in { x : (
card (x
. O))
c= n & x
in L };
then ex x st z
= x & (
card (x
. O))
c= n & x
in L;
hence thesis;
end;
hence thesis;
end;
::
MMLQUERY:def12
func L
WHEREge (O,n) ->
List of X equals { x : n
c= (
card (x
. O)) & x
in L };
coherence
proof
{ x : n
c= (
card (x
. O)) & x
in L }
c= X
proof
let z be
object;
assume z
in { x : n
c= (
card (x
. O)) & x
in L };
then ex x st z
= x & n
c= (
card (x
. O)) & x
in L;
hence thesis;
end;
hence thesis;
end;
::
MMLQUERY:def13
func L
WHERElt (O,n) ->
List of X equals { x : (
card (x
. O))
in n & x
in L };
coherence
proof
{ x : (
card (x
. O))
in n & x
in L }
c= X
proof
let z be
object;
assume z
in { x : (
card (x
. O))
in n & x
in L };
then ex x st z
= x & (
card (x
. O))
in n & x
in L;
hence thesis;
end;
hence thesis;
end;
::
MMLQUERY:def14
func L
WHEREgt (O,n) ->
List of X equals { x : n
in (
card (x
. O)) & x
in L };
coherence
proof
{ x : n
in (
card (x
. O)) & x
in L }
c= X
proof
let z be
object;
assume z
in { x : n
in (
card (x
. O)) & x
in L };
then ex x st z
= x & n
in (
card (x
. O)) & x
in L;
hence thesis;
end;
hence thesis;
end;
end
theorem ::
MMLQUERY:3
Th3: x
in (L
WHERE O) iff x
in L & (x
. O)
<>
{}
proof
hereby
assume x
in (L
WHERE O);
then
consider y such that
A1: x
= y & ex a st (y,a)
in O & y
in L;
thus x
in L & (x
. O)
<>
{} by
A1,
Th2;
end;
assume
A2: x
in L & (x
. O)
<>
{} ;
set y = the
Element of (x
. O);
y
in (x
. O) by
A2;
then
reconsider y as
Element of X;
(x,y)
in O by
A2,
Th2;
hence thesis by
A2;
end;
theorem ::
MMLQUERY:4
Th4: (L
WHERE O)
c= L by
Th3;
theorem ::
MMLQUERY:5
L
c= (
dom O) implies (L
WHERE O)
= L
proof
assume
A1: L
c= (
dom O);
thus (L
WHERE O)
c= L by
Th4;
let z be
object;
assume
A2: z
in L;
then
reconsider z as
Element of X;
(z
. O)
<>
{} by
A1,
A2,
RELAT_1: 170;
hence thesis by
A2,
Th3;
end;
theorem ::
MMLQUERY:6
Th6: n
<>
0 & L1
c= L2 implies (L1
WHEREge (O,n))
c= (L2
WHERE O)
proof
assume
A1: n
<>
0 & L1
c= L2;
let z be
object;
assume z
in (L1
WHEREge (O,n));
then
consider x such that
A2: z
= x & n
c= (
card (x
. O)) & x
in L1;
(x
. O)
<>
{} by
A1,
A2;
hence thesis by
A1,
A2,
Th3;
end;
theorem ::
MMLQUERY:7
(L
WHEREge (O,1))
= (L
WHERE O)
proof
thus (L
WHEREge (O,1))
c= (L
WHERE O) by
Th6;
let z be
object;
assume
A1: z
in (L
WHERE O);
then
reconsider z as
Element of X;
A2: (z
. O)
<>
{} & z
in L by
A1,
Th3;
then (
succ
0 )
c= (
card (z
. O)) by
ORDINAL1: 21,
ORDINAL3: 8;
hence thesis by
A2;
end;
theorem ::
MMLQUERY:8
Th8: L1
c= L2 implies (L1
WHEREgt (O,n))
c= (L2
WHERE O)
proof
assume
A1: L1
c= L2;
let z be
object;
assume z
in (L1
WHEREgt (O,n));
then
consider x such that
A2: z
= x & n
in (
card (x
. O)) & x
in L1;
(x
. O)
<>
{} by
A2;
hence thesis by
A1,
A2,
Th3;
end;
theorem ::
MMLQUERY:9
(L
WHEREgt (O,
0 ))
= (L
WHERE O)
proof
thus (L
WHEREgt (O,
0 ))
c= (L
WHERE O) by
Th8;
let z be
object;
assume
A1: z
in (L
WHERE O);
then
reconsider z as
Element of X;
A2: (z
. O)
<>
{} & z
in L by
A1,
Th3;
then
0
in (
card (z
. O)) by
ORDINAL3: 8;
hence thesis by
A2;
end;
theorem ::
MMLQUERY:10
n
<>
0 & L1
c= L2 implies (L1
WHEREeq (O,n))
c= (L2
WHERE O)
proof
assume
A1: n
<>
0 & L1
c= L2;
let z be
object;
assume z
in (L1
WHEREeq (O,n));
then
consider x such that
A2: z
= x & (
card (x
. O))
= n & x
in L1;
(x
. O)
<>
{} by
A1,
A2;
hence thesis by
A1,
A2,
Th3;
end;
theorem ::
MMLQUERY:11
(L
WHEREge (O,(n
+ 1)))
= (L
WHEREgt (O,n))
proof
thus (L
WHEREge (O,(n
+ 1)))
c= (L
WHEREgt (O,n))
proof
let z be
object;
assume z
in (L
WHEREge (O,(n
+ 1)));
then
consider x such that
A1: z
= x & (n
+ 1)
c= (
card (x
. O)) & x
in L;
(
Segm (n
+ 1))
= (
succ (
Segm n)) by
NAT_1: 38;
then n
in (
card (x
. O)) by
A1,
ORDINAL1: 21;
hence thesis by
A1;
end;
let z be
object;
assume z
in (L
WHEREgt (O,n));
then
consider x such that
A2: z
= x & n
in (
card (x
. O)) & x
in L;
(
Segm (n
+ 1))
= (
succ (
Segm n)) by
NAT_1: 38;
then (n
+ 1)
c= (
card (x
. O)) by
A2,
ORDINAL1: 21;
hence thesis by
A2;
end;
theorem ::
MMLQUERY:12
(L
WHEREle (O,n))
= (L
WHERElt (O,(n
+ 1)))
proof
thus (L
WHEREle (O,n))
c= (L
WHERElt (O,(n
+ 1)))
proof
let z be
object;
assume z
in (L
WHEREle (O,n));
then
consider x such that
A1: z
= x & (
card (x
. O))
c= n & x
in L;
(
Segm (n
+ 1))
= (
succ (
Segm n)) by
NAT_1: 38;
then (
card (x
. O))
in (n
+ 1) by
A1,
ORDINAL1: 22;
hence thesis by
A1;
end;
let z be
object;
assume z
in (L
WHERElt (O,(n
+ 1)));
then
consider x such that
A2: z
= x & (
card (x
. O))
in (n
+ 1) & x
in L;
(
Segm (n
+ 1))
= (
succ (
Segm n)) by
NAT_1: 38;
then (
card (x
. O))
c= n by
A2,
ORDINAL1: 22;
hence thesis by
A2;
end;
theorem ::
MMLQUERY:13
n
<= m & L1
c= L2 & O1
c= O2 implies (L1
WHEREge (O1,m))
c= (L2
WHEREge (O2,n))
proof
assume
A1: n
<= m & L1
c= L2 & O1
c= O2;
let z be
object;
assume z
in (L1
WHEREge (O1,m));
then
consider x such that
A2: z
= x & m
c= (
card (x
. O1)) & x
in L1;
(
Segm n)
c= (
Segm m) & (x
. O1)
c= (x
. O2) by
A1,
Th1,
NAT_1: 39;
then n
c= (
card (x
. O1)) & (
card (x
. O1))
c= (
card (x
. O2)) by
A2,
CARD_1: 11;
then n
c= (
card (x
. O2));
hence thesis by
A1,
A2;
end;
theorem ::
MMLQUERY:14
n
<= m & L1
c= L2 & O1
c= O2 implies (L1
WHEREgt (O1,m))
c= (L2
WHEREgt (O2,n))
proof
assume
A1: n
<= m & L1
c= L2 & O1
c= O2;
let z be
object;
assume z
in (L1
WHEREgt (O1,m));
then
consider x such that
A2: z
= x & m
in (
card (x
. O1)) & x
in L1;
(
Segm n)
c= (
Segm m) & (
card (x
. O1))
c= (
card (x
. O2)) by
A1,
Th1,
CARD_1: 11,
NAT_1: 39;
then n
in (
card (x
. O2)) by
A2,
ORDINAL1: 12;
hence thesis by
A1,
A2;
end;
theorem ::
MMLQUERY:15
n
<= m & L1
c= L2 & O1
c= O2 implies (L1
WHEREle (O2,n))
c= (L2
WHEREle (O1,m))
proof
assume
A1: n
<= m & L1
c= L2 & O1
c= O2;
let z be
object;
assume z
in (L1
WHEREle (O2,n));
then
consider x such that
A2: z
= x & (
card (x
. O2))
c= n & x
in L1;
(
Segm n)
c= (
Segm m) & (x
. O1)
c= (x
. O2) by
A1,
Th1,
NAT_1: 39;
then (
card (x
. O1))
c= (
card (x
. O2)) & (
card (x
. O2))
c= m by
A2,
CARD_1: 11;
then (
card (x
. O1))
c= m;
hence thesis by
A1,
A2;
end;
theorem ::
MMLQUERY:16
n
<= m & L1
c= L2 & O1
c= O2 implies (L1
WHERElt (O2,n))
c= (L2
WHERElt (O1,m))
proof
assume
A1: n
<= m & L1
c= L2 & O1
c= O2;
let z be
object;
assume z
in (L1
WHERElt (O2,n));
then
consider x such that
A2: z
= x & (
card (x
. O2))
in n & x
in L1;
(
Segm n)
c= (
Segm m) & (
card (x
. O1))
c= (
card (x
. O2)) by
A1,
Th1,
CARD_1: 11,
NAT_1: 39;
then (
card (x
. O1))
in m by
A2,
ORDINAL1: 12;
hence thesis by
A1,
A2;
end;
theorem ::
MMLQUERY:17
O1
c= O2 & L1
c= L2 & O
c= O3 implies (L1
WHEREge (O,O2))
c= (L2
WHEREge (O3,O1))
proof
assume
A1: O1
c= O2 & L1
c= L2 & O
c= O3;
let z be
object;
assume z
in (L1
WHEREge (O,O2));
then
consider x such that
A2: z
= x & (
card (x
. O2))
c= (
card (x
. O)) & x
in L1;
A3: (
card (x
. O1))
c= (
card (x
. O2)) & (
card (x
. O))
c= (
card (x
. O3)) by
A1,
Th1,
CARD_1: 11;
then (
card (x
. O1))
c= (
card (x
. O)) by
A2;
then (
card (x
. O1))
c= (
card (x
. O3)) by
A3;
hence z
in (L2
WHEREge (O3,O1)) by
A2,
A1;
end;
theorem ::
MMLQUERY:18
O1
c= O2 & L1
c= L2 & O
c= O3 implies (L1
WHEREgt (O,O2))
c= (L2
WHEREgt (O3,O1))
proof
assume
A1: O1
c= O2 & L1
c= L2 & O
c= O3;
let z be
object;
assume z
in (L1
WHEREgt (O,O2));
then
consider x such that
A2: z
= x & (
card (x
. O2))
in (
card (x
. O)) & x
in L1;
(x
. O1)
c= (x
. O2) & (x
. O)
c= (x
. O3) by
A1,
Th1;
then (
card (x
. O1))
in (
card (x
. O)) & (
card (x
. O))
c= (
card (x
. O3)) by
A2,
CARD_1: 11,
ORDINAL1: 12;
hence z
in (L2
WHEREgt (O3,O1)) by
A2,
A1;
end;
theorem ::
MMLQUERY:19
O1
c= O2 & L1
c= L2 & O
c= O3 implies (L1
WHEREle (O3,O1))
c= (L2
WHEREle (O,O2))
proof
assume
A1: O1
c= O2 & L1
c= L2 & O
c= O3;
let z be
object;
assume z
in (L1
WHEREle (O3,O1));
then
consider x such that
A2: z
= x & (
card (x
. O3))
c= (
card (x
. O1)) & x
in L1;
A3: (
card (x
. O1))
c= (
card (x
. O2)) & (
card (x
. O))
c= (
card (x
. O3)) by
A1,
Th1,
CARD_1: 11;
then (
card (x
. O3))
c= (
card (x
. O2)) by
A2;
then (
card (x
. O))
c= (
card (x
. O2)) by
A3;
hence z
in (L2
WHEREle (O,O2)) by
A2,
A1;
end;
theorem ::
MMLQUERY:20
O1
c= O2 & L1
c= L2 & O
c= O3 implies (L1
WHERElt (O3,O1))
c= (L2
WHERElt (O,O2))
proof
assume
A1: O1
c= O2 & L1
c= L2 & O
c= O3;
let z be
object;
assume z
in (L1
WHERElt (O3,O1));
then
consider x such that
A2: z
= x & (
card (x
. O3))
in (
card (x
. O1)) & x
in L1;
(
card (x
. O1))
c= (
card (x
. O2)) & (
card (x
. O))
c= (
card (x
. O3)) by
A1,
Th1,
CARD_1: 11;
then (
card (x
. O))
in (
card (x
. O2)) by
A2,
ORDINAL1: 12;
hence z
in (L2
WHERElt (O,O2)) by
A2,
A1;
end;
theorem ::
MMLQUERY:21
(L
WHEREgt (O,O1))
c= (L
WHERE O)
proof
let z be
object;
assume z
in (L
WHEREgt (O,O1));
then
consider x such that
A1: z
= x & (
card (x
. O1))
in (
card (x
. O)) & x
in L;
(x
. O)
<>
{} by
A1;
hence thesis by
A1,
Th3;
end;
theorem ::
MMLQUERY:22
O1
c= O2 & L1
c= L2 implies (L1
WHERE O1)
c= (L2
WHERE O2)
proof
assume
A1: O1
c= O2 & L1
c= L2;
let z be
object;
assume
A2: z
in (L1
WHERE O1);
then
reconsider z as
Element of X;
A3: (z
. O1)
<>
{} & z
in L1 by
A2,
Th3;
(z
. O1)
c= (z
. O2) by
A1,
Th1;
then (z
. O2)
<>
{} by
A3;
hence thesis by
A1,
A3,
Th3;
end;
theorem ::
MMLQUERY:23
Th23: a
in (L
| O) iff ex b st a
in (b
. O) & b
in L
proof
hereby
assume a
in (L
| O);
then
consider b be
object such that
A1:
[b, a]
in O & b
in L by
RELAT_1:def 13;
reconsider b as
Element of X by
A1;
take b;
thus a
in (b
. O) by
A1,
RELAT_1: 169;
thus b
in L by
A1;
end;
given b such that
A2: a
in (b
. O) & b
in L;
[b, a]
in O by
A2,
RELAT_1: 169;
hence a
in (L
| O) by
A2,
RELAT_1:def 13;
end;
notation
let X, A, B;
synonym A
AND B for A
/\ B;
synonym A
OR B for A
\/ B;
synonym A
BUTNOT B for A
\ B;
end
definition
let X, A, B;
:: original:
AND
redefine
func A
AND B ->
List of X ;
coherence
proof
(A
/\ B) is
Subset of X;
hence thesis;
end;
:: original:
OR
redefine
func A
OR B ->
List of X ;
coherence
proof
(A
\/ B) is
Subset of X;
hence thesis;
end;
:: original:
BUTNOT
redefine
func A
BUTNOT B ->
List of X ;
coherence
proof
(A
\ B) is
Subset of X;
hence thesis;
end;
end
theorem ::
MMLQUERY:24
Th24: L1
<>
{} & L2
<>
{} implies ((L1
OR L2)
\& O)
= ((L1
\& O)
AND (L2
\& O))
proof
assume
A1: L1
<>
{} & L2
<>
{} ;
thus ((L1
OR L2)
\& O)
c= ((L1
\& O)
AND (L2
\& O))
proof
let z be
object;
assume
A2: z
in ((L1
OR L2)
\& O);
now
set c = the
Element of L1;
c
in L1 by
A1;
then
reconsider c as
Element of X;
(c
. O)
in { (x
. O) : x
in L1 } by
A1;
hence { (x
. O) : x
in L1 }
<>
{} ;
let Y;
assume Y
in { (x
. O) : x
in L1 };
then
consider x such that
A3: Y
= (x
. O) & x
in L1;
x
in (L1
OR L2) by
A3,
XBOOLE_0:def 3;
then Y
in { (a
. O) : a
in (L1
OR L2) } by
A3;
hence z
in Y by
A2,
SETFAM_1:def 1;
end;
then
A4: z
in (L1
\& O) by
SETFAM_1:def 1;
now
set c = the
Element of L2;
c
in L2 by
A1;
then
reconsider c as
Element of X;
(c
. O)
in { (x
. O) : x
in L2 } by
A1;
hence { (x
. O) : x
in L2 }
<>
{} ;
let Y;
assume Y
in { (x
. O) : x
in L2 };
then
consider x such that
A5: Y
= (x
. O) & x
in L2;
x
in (L1
OR L2) by
A5,
XBOOLE_0:def 3;
then Y
in { (a
. O) : a
in (L1
OR L2) } by
A5;
hence z
in Y by
A2,
SETFAM_1:def 1;
end;
then z
in (L2
\& O) by
SETFAM_1:def 1;
hence thesis by
A4,
XBOOLE_0:def 4;
end;
let z be
object;
assume z
in ((L1
\& O)
AND (L2
\& O));
then
A6: z
in (L1
\& O) & z
in (L2
\& O) by
XBOOLE_0:def 4;
now
set c = the
Element of L2;
c
in L2 by
A1;
then
reconsider c as
Element of X;
c
in (L1
OR L2) by
A1,
XBOOLE_0:def 3;
then (c
. O)
in { (x
. O) : x
in (L1
OR L2) };
hence { (x
. O) : x
in (L1
OR L2) }
<>
{} ;
let Y;
assume Y
in { (x
. O) : x
in (L1
OR L2) };
then
consider x such that
A7: Y
= (x
. O) & x
in (L1
OR L2);
x
in L1 or x
in L2 by
A7,
XBOOLE_0:def 3;
then Y
in { (a
. O) : a
in L1 } or Y
in { (b
. O) : b
in L2 } by
A7;
hence z
in Y by
A6,
SETFAM_1:def 1;
end;
hence thesis by
SETFAM_1:def 1;
end;
theorem ::
MMLQUERY:25
L1
c= L2 & O1
c= O2 implies (L1
| O1)
c= (L2
| O2)
proof
assume L1
c= L2 & O1
c= O2;
then (L1
| O1)
c= (L2
| O1) & (L2
| O1)
c= (L2
| O2) by
RELAT_1: 123,
RELAT_1: 124;
hence thesis;
end;
theorem ::
MMLQUERY:26
Th26: O1
c= O2 implies (L
\& O1)
c= (L
\& O2)
proof
assume
A1: O1
c= O2;
let z be
object;
assume
A2: z
in (L
\& O1);
then { (x
. O1) : x
in L }
<>
{} by
SETFAM_1:def 1;
then
consider Y be
object such that
A3: Y
in { (x
. O1) : x
in L } by
XBOOLE_0:def 1;
consider y such that
A4: Y
= (y
. O1) & y
in L by
A3;
A5: (y
. O2)
in { (x
. O2) : x
in L } by
A4;
now
let Y;
assume Y
in { (x
. O2) : x
in L };
then
consider a such that
A6: Y
= (a
. O2) & a
in L;
(a
. O1)
in { (x
. O1) : x
in L } by
A6;
then z
in (a
. O1) & (a
. O1)
c= Y by
A1,
A2,
A6,
Th1,
SETFAM_1:def 1;
hence z
in Y;
end;
hence thesis by
A5,
SETFAM_1:def 1;
end;
theorem ::
MMLQUERY:27
(L
\& (O1
AND O2))
= ((L
\& O1)
AND (L
\& O2))
proof
(L
\& (O1
AND O2))
c= (L
\& O1) & (L
\& (O1
AND O2))
c= (L
\& O2) by
Th26,
XBOOLE_1: 17;
hence (L
\& (O1
AND O2))
c= ((L
\& O1)
AND (L
\& O2)) by
XBOOLE_1: 19;
let z be
object;
assume z
in ((L
\& O1)
AND (L
\& O2));
then
A1: z
in (L
\& O1) & z
in (L
\& O2) by
XBOOLE_0:def 4;
now
set O = (O1
AND O2);
set c = the
Element of L;
{ (x
. O1) : x
in L }
<>
{} by
A1,
SETFAM_1:def 1;
then
consider c be
object such that
A2: c
in { (x
. O1) : x
in L } by
XBOOLE_0:def 1;
consider a such that
A3: c
= (a
. O1) & a
in L by
A2;
(a
. O)
in { (x
. O) : x
in L } by
A3;
hence { (x
. O) : x
in L }
<>
{} ;
let Y;
assume Y
in { (x
. O) : x
in L };
then
consider x such that
A4: Y
= (x
. O) & x
in L;
A5: Y
= ((x
. O1)
AND (x
. O2)) by
A4,
RELSET_2: 11;
(x
. O1)
in { (y
. O1) : y
in L } by
A4;
then
A6: z
in (x
. O1) by
A1,
SETFAM_1:def 1;
(x
. O2)
in { (y
. O2) : y
in L } by
A4;
then z
in (x
. O2) by
A1,
SETFAM_1:def 1;
hence z
in Y by
A5,
A6,
XBOOLE_0:def 4;
end;
hence thesis by
SETFAM_1:def 1;
end;
theorem ::
MMLQUERY:28
L1
<>
{} & L1
c= L2 implies (L2
\& O)
c= (L1
\& O)
proof
assume
A1: L1
<>
{} ;
assume
A2: L1
c= L2;
let z be
object;
assume
A3: z
in (L2
\& O);
now
set c = the
Element of L1;
c
in L1 by
A1;
then
reconsider c as
Element of X;
(c
. O)
in { (x
. O) : x
in L1 } by
A1;
hence { (x
. O) : x
in L1 }
<>
{} ;
let Y;
assume Y
in { (x
. O) : x
in L1 };
then
consider x such that
A4: Y
= (x
. O) & x
in L1;
Y
in { (a
. O) : a
in L2 } by
A4,
A2;
hence z
in Y by
A3,
SETFAM_1:def 1;
end;
hence z
in (L1
\& O) by
SETFAM_1:def 1;
end;
begin
theorem ::
MMLQUERY:29
Th29: for O1,O2 be
Operation of X st for x holds (x
. O1)
= (x
. O2) holds O1
= O2
proof
let O1,O2 be
Operation of X;
assume
A1: for x holds (x
. O1)
= (x
. O2);
let a,b be
object;
thus
[a, b]
in O1 implies
[a, b]
in O2
proof
assume
A2:
[a, b]
in O1;
reconsider a, b as
Element of X by
A2,
ZFMISC_1: 87;
b
in (a
. O1) by
A2,
RELAT_1: 169;
then b
in (a
. O2) by
A1;
hence thesis by
RELAT_1: 169;
end;
assume
A3:
[a, b]
in O2;
then
A4: a
in X & b
in X by
ZFMISC_1: 87;
reconsider a, b as
Element of X by
A3,
ZFMISC_1: 87;
reconsider L =
{a} as
Subset of X by
A4,
ZFMISC_1: 31;
b
in (a
. O2) by
A3,
RELAT_1: 169;
then b
in (a
. O1) by
A1;
hence thesis by
RELAT_1: 169;
end;
theorem ::
MMLQUERY:30
Th30: for O1,O2 be
Operation of X st for L holds (L
| O1)
= (L
| O2) holds O1
= O2
proof
let O1,O2 be
Operation of X;
assume
A1: for L holds (L
| O1)
= (L
| O2);
now
let x;
per cases ;
suppose X
<>
{} ;
then
reconsider L =
{x} as
Subset of X by
ZFMISC_1: 31;
thus (x
. O1)
= (L
| O1)
.= (x
. O2) by
A1;
end;
suppose X
=
{} ;
hence (x
. O1)
= (x
. O2);
end;
end;
hence thesis by
Th29;
end;
definition
let X, O;
::
MMLQUERY:def15
func
NOT O ->
Operation of X means
:
Def15: for L holds (L
| it )
= (
union { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in L });
existence
proof
defpred
P[
object,
object] means (
Im (O,$1))
=
{} & $2
= $1;
consider O1 be
Relation such that
A1: for a,b be
object holds
[a, b]
in O1 iff a
in X & b
in X &
P[a, b] from
RELAT_1:sch 1;
O1
c=
[:X, X:]
proof
let x,y be
object;
assume
[x, y]
in O1;
then x
in X & y
in X by
A1;
hence thesis by
ZFMISC_1: 87;
end;
then
reconsider O1 as
Operation of X;
take O1;
let L;
thus (L
| O1)
c= (
union { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in L })
proof
let a be
object;
assume a
in (L
| O1);
then
consider b such that
A2: a
in (b
. O1) & b
in L by
Th23;
[b, a]
in O1 by
A2,
RELAT_1: 169;
then
A3: a
= b & (b
. O)
=
{} by
A1;
then
B1: a
in
{b} by
TARSKI:def 1;
reconsider Z = (
IFEQ ((b
. O),
{} ,
{b},
{} )) as
set;
A4: a
in Z by
A3,
B1,
FUNCOP_1:def 8;
(
IFEQ ((b
. O),
{} ,
{b},
{} ))
in { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in L } by
A2;
hence thesis by
A4,
TARSKI:def 4;
end;
let a be
object;
assume a
in (
union { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in L });
then
consider A be
set such that
A5: a
in A & A
in { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in L } by
TARSKI:def 4;
consider x such that
A6: A
= (
IFEQ ((x
. O),
{} ,
{x},
{} )) & x
in L by
A5;
A7: (x
. O)
=
{} by
A5,
A6,
FUNCOP_1:def 8;
then A
=
{x} by
A6,
FUNCOP_1:def 8;
then a
= x by
A5,
TARSKI:def 1;
then
[x, a]
in O1 by
A1,
A6,
A7;
hence thesis by
A6,
RELAT_1:def 13;
end;
uniqueness
proof
let O1,O2 be
Operation of X such that
A8: for L holds (L
| O1)
= (
union { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in L }) and
A9: for L holds (L
| O2)
= (
union { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in L });
now
let L;
thus (L
| O1)
= (
union { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in L }) by
A8
.= (L
| O2) by
A9;
end;
hence thesis by
Th30;
end;
end
notation
let X;
let O1,O2 be
Operation of X;
synonym O1
AND O2 for O1
/\ O2;
synonym O1
OR O2 for O1
\/ O2;
synonym O1
BUTNOT O2 for O1
\ O2;
synonym O1
| O2 for O1
* O2;
end
definition
let X;
let O1,O2 be
Operation of X;
:: original:
AND
redefine
::
MMLQUERY:def16
func O1
AND O2 ->
Operation of X means for L holds (L
| it )
= (
union { ((x
. O1)
AND (x
. O2)) : x
in L });
coherence
proof
thus (O1
/\ O2) is
Subset of
[:X, X:];
end;
compatibility
proof
A1: for O be
Operation of X holds O
= (O1
AND O2) implies for L holds (L
| O)
= (
union { ((x
. O1)
AND (x
. O2)) : x
in L })
proof
let O;
assume
A2: O
= (O1
/\ O2);
defpred
P[
set,
set] means
[$1, $2]
in O1 &
[$1, $2]
in O2;
let L;
thus (L
| O)
c= (
union { ((x
. O1)
AND (x
. O2)) : x
in L })
proof
let z be
object;
assume z
in (L
| O);
then
consider y be
object such that
A3:
[y, z]
in O & y
in L by
RELAT_1:def 13;
reconsider y, z as
Element of X by
A3,
ZFMISC_1: 87;
[y, z]
in O1 &
[y, z]
in O2 by
A2,
A3,
XBOOLE_0:def 4;
then z
in (y
. O1) & z
in (y
. O2) by
RELAT_1: 169;
then z
in ((y
. O1)
AND (y
. O2)) & ((y
. O1)
AND (y
. O2))
in { ((x
. O1)
AND (x
. O2)) : x
in L } by
A3,
XBOOLE_0:def 4;
hence thesis by
TARSKI:def 4;
end;
let z be
object;
assume z
in (
union { ((x
. O1)
AND (x
. O2)) : x
in L });
then
consider Y be
set such that
A4: z
in Y & Y
in { ((x
. O1)
AND (x
. O2)) : x
in L } by
TARSKI:def 4;
consider x such that
A5: Y
= ((x
. O1)
AND (x
. O2)) & x
in L by
A4;
A6: z
in (x
. O1) & z
in (x
. O2) by
A4,
A5,
XBOOLE_0:def 4;
reconsider z as
Element of X by
A4,
A5;
[x, z]
in O1 &
[x, z]
in O2 by
A6,
RELAT_1: 169;
then
[x, z]
in O by
A2,
XBOOLE_0:def 4;
hence thesis by
A5,
RELAT_1:def 13;
end;
let O be
Operation of X;
thus O
= (O1
AND O2) implies for L holds (L
| O)
= (
union { ((x
. O1)
AND (x
. O2)) : x
in L }) by
A1;
assume
A7: for L holds (L
| O)
= (
union { ((x
. O1)
AND (x
. O2)) : x
in L });
now
let L;
thus (L
| O)
= (
union { ((x
. O1)
AND (x
. O2)) : x
in L }) by
A7
.= (L
| (O1
/\ O2)) by
A1;
end;
hence thesis by
Th30;
end;
:: original:
OR
redefine
::
MMLQUERY:def17
func O1
OR O2 ->
Operation of X means for L holds (L
| it )
= (
union { ((x
. O1)
OR (x
. O2)) : x
in L });
coherence
proof
thus (O1
\/ O2) is
Subset of
[:X, X:];
end;
compatibility
proof
A8: for O be
Operation of X holds O
= (O1
OR O2) implies for L holds (L
| O)
= (
union { ((x
. O1)
OR (x
. O2)) : x
in L })
proof
let O;
assume
A9: O
= (O1
\/ O2);
defpred
P[
set,
set] means
[$1, $2]
in O1 or
[$1, $2]
in O2;
let L;
thus (L
| O)
c= (
union { ((x
. O1)
OR (x
. O2)) : x
in L })
proof
let z be
object;
assume z
in (L
| O);
then
consider y be
object such that
A10:
[y, z]
in O & y
in L by
RELAT_1:def 13;
reconsider y, z as
Element of X by
A10,
ZFMISC_1: 87;
[y, z]
in O1 or
[y, z]
in O2 by
A9,
A10,
XBOOLE_0:def 3;
then z
in (y
. O1) or z
in (y
. O2) by
RELAT_1: 169;
then z
in ((y
. O1)
OR (y
. O2)) & ((y
. O1)
OR (y
. O2))
in { ((x
. O1)
OR (x
. O2)) : x
in L } by
A10,
XBOOLE_0:def 3;
hence thesis by
TARSKI:def 4;
end;
let z be
object;
assume z
in (
union { ((x
. O1)
OR (x
. O2)) : x
in L });
then
consider Y be
set such that
A11: z
in Y & Y
in { ((x
. O1)
OR (x
. O2)) : x
in L } by
TARSKI:def 4;
consider x such that
A12: Y
= ((x
. O1)
OR (x
. O2)) & x
in L by
A11;
A13: z
in (x
. O1) or z
in (x
. O2) by
A11,
A12,
XBOOLE_0:def 3;
reconsider z as
Element of X by
A11,
A12;
[x, z]
in O1 or
[x, z]
in O2 by
A13,
RELAT_1: 169;
then
[x, z]
in O by
A9,
XBOOLE_0:def 3;
hence thesis by
A12,
RELAT_1:def 13;
end;
let O be
Operation of X;
thus O
= (O1
OR O2) implies for L holds (L
| O)
= (
union { ((x
. O1)
OR (x
. O2)) : x
in L }) by
A8;
assume
A14: for L holds (L
| O)
= (
union { ((x
. O1)
OR (x
. O2)) : x
in L });
now
let L;
thus (L
| O)
= (
union { ((x
. O1)
OR (x
. O2)) : x
in L }) by
A14
.= (L
| (O1
\/ O2)) by
A8;
end;
hence thesis by
Th30;
end;
:: original:
BUTNOT
redefine
::
MMLQUERY:def18
func O1
BUTNOT O2 ->
Operation of X means for L holds (L
| it )
= (
union { ((x
. O1)
BUTNOT (x
. O2)) : x
in L });
coherence
proof
thus (O1
\ O2) is
Subset of
[:X, X:];
end;
compatibility
proof
A15: for O be
Operation of X holds O
= (O1
BUTNOT O2) implies for L holds (L
| O)
= (
union { ((x
. O1)
BUTNOT (x
. O2)) : x
in L })
proof
let O;
assume
A16: O
= (O1
\ O2);
defpred
P[
set,
set] means
[$1, $2]
in O1 & not
[$1, $2]
in O2;
let L;
thus (L
| O)
c= (
union { ((x
. O1)
BUTNOT (x
. O2)) : x
in L })
proof
let z be
object;
assume z
in (L
| O);
then
consider y be
object such that
A17:
[y, z]
in O & y
in L by
RELAT_1:def 13;
reconsider y, z as
Element of X by
A17,
ZFMISC_1: 87;
[y, z]
in O1 &
[y, z]
nin O2 by
A16,
A17,
XBOOLE_0:def 5;
then z
in (y
. O1) & z
nin (y
. O2) by
RELAT_1: 169;
then z
in ((y
. O1)
BUTNOT (y
. O2)) & ((y
. O1)
BUTNOT (y
. O2))
in { ((x
. O1)
BUTNOT (x
. O2)) : x
in L } by
A17,
XBOOLE_0:def 5;
hence thesis by
TARSKI:def 4;
end;
let z be
object;
assume z
in (
union { ((x
. O1)
BUTNOT (x
. O2)) : x
in L });
then
consider Y be
set such that
A18: z
in Y & Y
in { ((x
. O1)
BUTNOT (x
. O2)) : x
in L } by
TARSKI:def 4;
consider x such that
A19: Y
= ((x
. O1)
BUTNOT (x
. O2)) & x
in L by
A18;
A20: z
in (x
. O1) & not z
in (x
. O2) by
A18,
A19,
XBOOLE_0:def 5;
reconsider z as
Element of X by
A18,
A19;
[x, z]
in O1 &
[x, z]
nin O2 by
A20,
RELAT_1: 169;
then
[x, z]
in O by
A16,
XBOOLE_0:def 5;
hence thesis by
A19,
RELAT_1:def 13;
end;
let O be
Operation of X;
thus O
= (O1
BUTNOT O2) implies for L holds (L
| O)
= (
union { ((x
. O1)
BUTNOT (x
. O2)) : x
in L }) by
A15;
assume
A21: for L holds (L
| O)
= (
union { ((x
. O1)
BUTNOT (x
. O2)) : x
in L });
now
let L;
thus (L
| O)
= (
union { ((x
. O1)
BUTNOT (x
. O2)) : x
in L }) by
A21
.= (L
| (O1
\ O2)) by
A15;
end;
hence thesis by
Th30;
end;
:: original:
|
redefine
::
MMLQUERY:def19
func O1
| O2 ->
Operation of X means for L holds (L
| it )
= ((L
| O1)
| O2);
coherence
proof
thus (O1
* O2) is
Relation of X;
end;
compatibility
proof
let O be
Operation of X;
thus O
= (O1
| O2) implies for L holds (L
| O)
= ((L
| O1)
| O2) by
RELAT_1: 126;
assume
A22: for L holds (L
| O)
= ((L
| O1)
| O2);
now
let L;
thus (L
| O)
= ((L
| O1)
| O2) by
A22
.= (L
| (O1
* O2)) by
RELAT_1: 126;
end;
hence thesis by
Th30;
end;
::
MMLQUERY:def20
func O1
\& O2 ->
Operation of X means
:
Def20: for L holds (L
| it )
= (
union { ((x
. O1)
\& O2) : x
in L });
existence
proof
defpred
P[
object,
object] means ex x st $1
= x & $2
in ((x
. O1)
\& O2);
consider O be
Relation such that
A23: for z,s be
object holds
[z, s]
in O iff z
in X & s
in X &
P[z, s] from
RELAT_1:sch 1;
O
c=
[:X, X:]
proof
let z,s be
object;
assume
[z, s]
in O;
then z
in X & s
in X by
A23;
hence thesis by
ZFMISC_1: 87;
end;
then
reconsider O as
Operation of X;
take O;
let L;
thus (L
| O)
c= (
union { ((x
. O1)
\& O2) : x
in L })
proof
let z be
object;
assume z
in (L
| O);
then
consider y such that
A24: z
in (y
. O) & y
in L by
Th23;
[y, z]
in O by
A24,
RELAT_1: 169;
then ex x st y
= x & z
in ((x
. O1)
\& O2) by
A23;
then z
in ((y
. O1)
\& O2) & ((y
. O1)
\& O2)
in { ((x
. O1)
\& O2) : x
in L } by
A24;
hence thesis by
TARSKI:def 4;
end;
let z be
object;
assume z
in (
union { ((x
. O1)
\& O2) : x
in L });
then
consider Y such that
A25: z
in Y & Y
in { ((x
. O1)
\& O2) : x
in L } by
TARSKI:def 4;
consider x such that
A26: Y
= ((x
. O1)
\& O2) & x
in L by
A25;
[x, z]
in O by
A23,
A25,
A26;
hence thesis by
A26,
RELAT_1:def 13;
end;
uniqueness
proof
let R1,R2 be
Operation of X such that
A27: for L holds (L
| R1)
= (
union { ((x
. O1)
\& O2) : x
in L }) and
A28: for L holds (L
| R2)
= (
union { ((x
. O1)
\& O2) : x
in L });
now
let L;
thus (L
| R1)
= (
union { ((x
. O1)
\& O2) : x
in L }) by
A27
.= (L
| R2) by
A28;
end;
hence thesis by
Th30;
end;
end
theorem ::
MMLQUERY:31
(x
. (O1
AND O2))
= ((x
. O1)
AND (x
. O2)) by
RELSET_2: 11;
theorem ::
MMLQUERY:32
(x
. (O1
OR O2))
= ((x
. O1)
OR (x
. O2)) by
RELSET_2: 10;
theorem ::
MMLQUERY:33
(x
. (O1
BUTNOT O2))
= ((x
. O1)
BUTNOT (x
. O2)) by
RELSET_2: 12;
theorem ::
MMLQUERY:34
(x
. (O1
| O2))
= ((x
. O1)
| O2) by
RELAT_1: 126;
theorem ::
MMLQUERY:35
Th35: (x
. (O1
\& O2))
= ((x
. O1)
\& O2)
proof
per cases ;
suppose X
=
{} ;
then (x
. (O1
\& O2))
=
{} & ((x
. O1)
\& O2)
=
{} ;
hence thesis;
end;
suppose X
<>
{} ;
then
reconsider L =
{x} as
List of X by
ZFMISC_1: 31;
A1: { ((a
. O1)
\& O2) : a
in L }
=
{((x
. O1)
\& O2)}
proof
thus { ((a
. O1)
\& O2) : a
in L }
c=
{((x
. O1)
\& O2)}
proof
let z be
object;
assume z
in { ((a
. O1)
\& O2) : a
in L };
then
consider a such that
A2: z
= ((a
. O1)
\& O2) & a
in L;
a
= x by
A2,
TARSKI:def 1;
hence thesis by
A2,
TARSKI:def 1;
end;
let z be
object;
assume z
in
{((x
. O1)
\& O2)};
then z
= ((x
. O1)
\& O2) & x
in L by
TARSKI:def 1;
hence thesis;
end;
thus (x
. (O1
\& O2))
= (
union { ((a
. O1)
\& O2) : a
in L }) by
Def20
.= ((x
. O1)
\& O2) by
A1,
ZFMISC_1: 25;
end;
end;
theorem ::
MMLQUERY:36
Th36: for z,s be
object holds
[z, s]
in (
NOT O) iff z
= s & z
in X & z
nin (
dom O)
proof
let z,s be
object;
thus
[z, s]
in (
NOT O) implies z
= s & z
in X & z
nin (
dom O)
proof
assume
A1:
[z, s]
in (
NOT O);
then s
in (
Im ((
NOT O),z)) & z
in X by
RELAT_1: 169,
ZFMISC_1: 87;
then s
in ((
NOT O)
.:
{z}) &
{z}
c= X by
ZFMISC_1: 31;
then s
in (
union { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in
{z} }) by
Def15;
then
consider Y such that
A2: s
in Y & Y
in { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in
{z} } by
TARSKI:def 4;
consider x such that
A3: Y
= (
IFEQ ((x
. O),
{} ,
{x},
{} )) & x
in
{z} by
A2;
A4: x
= z by
A3,
TARSKI:def 1;
A5: (x
. O)
=
{} by
A2,
A3,
FUNCOP_1:def 8;
then s
in
{x} by
A2,
A3,
FUNCOP_1:def 8;
then
A6: s
= x & for s be
object holds
[x, s]
nin O by
A5,
RELAT_1: 169,
TARSKI:def 1;
hence z
= s by
A4;
thus z
in X by
A1,
ZFMISC_1: 87;
x
in (
dom O) iff ex y be
object st
[x, y]
in O by
XTUPLE_0:def 12;
hence z
nin (
dom O) by
A4,
A6;
end;
assume
A7: z
= s & z
in X & z
nin (
dom O);
then
reconsider z as
Element of X;
(z
. O)
c=
{}
proof
let y be
object;
assume y
in (z
. O);
then
[z, y]
in O by
RELAT_1: 169;
hence thesis by
A7,
XTUPLE_0:def 12;
end;
then (z
. O)
=
{} ;
then
A8: (
IFEQ ((z
. O),
{} ,
{z},
{} ))
=
{z} by
FUNCOP_1:def 8;
A9: z
in
{z} by
TARSKI:def 1;
reconsider L =
{z} as
Subset of X by
A7,
ZFMISC_1: 31;
{z}
in { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in
{z} } by
A8,
A9;
then z
in (
union { (
IFEQ ((x
. O),
{} ,
{x},
{} )) : x
in
{z} }) by
A9,
TARSKI:def 4;
then z
in (L
| (
NOT O)) by
Def15;
then z
in (z
. (
NOT O));
hence thesis by
A7,
RELAT_1: 169;
end;
theorem ::
MMLQUERY:37
Th37: (
NOT O)
= (
id (X
\ (
dom O)))
proof
let z,s be
object;
thus
[z, s]
in (
NOT O) implies
[z, s]
in (
id (X
\ (
dom O)))
proof
assume
[z, s]
in (
NOT O);
then
A1: z
= s & z
in X & z
nin (
dom O) by
Th36;
then z
in (X
\ (
dom O)) by
XBOOLE_0:def 5;
hence thesis by
A1,
RELAT_1:def 10;
end;
assume
[z, s]
in (
id (X
\ (
dom O)));
then
A2: z
= s & z
in (X
\ (
dom O)) by
RELAT_1:def 10;
then z
in X & z
nin (
dom O) by
XBOOLE_0:def 5;
hence thesis by
A2,
Th36;
end;
theorem ::
MMLQUERY:38
Th38: (
dom (
NOT (
NOT O)))
= (
dom O)
proof
thus (
dom (
NOT (
NOT O)))
= (
dom (
id (X
\ (
dom (
NOT O))))) by
Th37
.= (X
\ (
dom (
NOT O))) by
RELAT_1: 45
.= (X
\ (
dom (
id (X
\ (
dom O))))) by
Th37
.= (X
\ (X
\ (
dom O))) by
RELAT_1: 45
.= (X
/\ (
dom O)) by
XBOOLE_1: 48
.= (
dom O) by
XBOOLE_1: 28;
end;
theorem ::
MMLQUERY:39
(L
WHERE (
NOT (
NOT O)))
= (L
WHERE O)
proof
thus (L
WHERE (
NOT (
NOT O)))
c= (L
WHERE O)
proof
let z be
object;
assume
A1: z
in (L
WHERE (
NOT (
NOT O)));
then
reconsider x = z as
Element of X;
A2: x
in L & (x
. (
NOT (
NOT O)))
<>
{} by
A1,
Th3;
then x
in (
dom (
NOT (
NOT O))) by
RELAT_1: 170;
then x
in (
dom O) by
Th38;
then (x
. O)
<>
{} by
RELAT_1: 170;
hence thesis by
A2,
Th3;
end;
let z be
object;
assume
A3: z
in (L
WHERE O);
then
reconsider x = z as
Element of X;
A4: z
in L & (x
. O)
<>
{} by
A3,
Th3;
then x
in (
dom O) by
RELAT_1: 170;
then x
in (
dom (
NOT (
NOT O))) by
Th38;
then (x
. (
NOT (
NOT O)))
<>
{} by
RELAT_1: 170;
hence thesis by
A4,
Th3;
end;
theorem ::
MMLQUERY:40
(L
WHEREeq (O,
0 ))
= (L
WHERE (
NOT O))
proof
thus (L
WHEREeq (O,
0 ))
c= (L
WHERE (
NOT O))
proof
let z be
object;
assume z
in (L
WHEREeq (O,
0 ));
then
consider x such that
A1: z
= x & (
card (x
. O))
=
0 & x
in L;
(x
. O)
=
{} by
A1;
then x
nin (
dom O) by
RELAT_1: 170;
then
[x, x]
in (
NOT O) by
A1,
Th36;
then (x,x)
in (
NOT O);
hence thesis by
A1;
end;
let z be
object;
assume z
in (L
WHERE (
NOT O));
then
consider x such that
A2: z
= x & ex y st (x,y)
in (
NOT O) & x
in L;
consider y such that
A3: (x,y)
in (
NOT O) & x
in L by
A2;
[x, y]
in (
NOT O) by
A3;
then x
= y & x
in X & x
nin (
dom O) by
Th36;
then (x
. O)
=
{} by
RELAT_1: 170;
then (
card (x
. O))
=
0 ;
hence thesis by
A2;
end;
theorem ::
MMLQUERY:41
(
NOT (
NOT (
NOT O)))
= (
NOT O)
proof
thus (
NOT (
NOT (
NOT O)))
= (
id (X
\ (
dom (
NOT (
NOT O))))) by
Th37
.= (
id (X
\ (
dom O))) by
Th38
.= (
NOT O) by
Th37;
end;
theorem ::
MMLQUERY:42
((
NOT O1)
OR (
NOT O2))
c= (
NOT (O1
AND O2))
proof
let z,s be
object;
assume
[z, s]
in ((
NOT O1)
OR (
NOT O2));
then
[z, s]
in (
NOT O1) or
[z, s]
in (
NOT O2) by
XBOOLE_0:def 3;
then
A1: s
= z & z
in X & (z
nin (
dom O1) or z
nin (
dom O2)) by
Th36;
then z
nin ((
dom O1)
/\ (
dom O2)) & (
dom (O1
AND O2))
c= ((
dom O1)
/\ (
dom O2)) by
XBOOLE_0:def 4,
XTUPLE_0: 24;
then z
nin (
dom (O1
AND O2));
hence thesis by
A1,
Th36;
end;
theorem ::
MMLQUERY:43
(
NOT (O1
OR O2))
= ((
NOT O1)
AND (
NOT O2))
proof
let z,s be
object;
thus
[z, s]
in (
NOT (O1
OR O2)) implies
[z, s]
in ((
NOT O1)
AND (
NOT O2))
proof
assume
[z, s]
in (
NOT (O1
OR O2));
then
A1: z
= s & z
in X & z
nin (
dom (O1
OR O2)) by
Th36;
then z
nin ((
dom O1)
\/ (
dom O2)) by
XTUPLE_0: 23;
then z
nin (
dom O1) & z
nin (
dom O2) by
XBOOLE_0:def 3;
then
[z, s]
in (
NOT O1) &
[z, s]
in (
NOT O2) by
A1,
Th36;
hence thesis by
XBOOLE_0:def 4;
end;
assume
[z, s]
in ((
NOT O1)
AND (
NOT O2));
then
[z, s]
in (
NOT O1) &
[z, s]
in (
NOT O2) by
XBOOLE_0:def 4;
then
A2: z
= s & z
in X & z
nin (
dom O1) & z
nin (
dom O2) by
Th36;
then z
nin ((
dom O1)
\/ (
dom O2)) by
XBOOLE_0:def 3;
then z
nin (
dom (O1
OR O2)) by
XTUPLE_0: 23;
hence thesis by
A2,
Th36;
end;
theorem ::
MMLQUERY:44
(
dom O1)
= X & (
dom O2)
= X implies ((O1
OR O2)
\& O)
= ((O1
\& O)
AND (O2
\& O))
proof
assume
A1: (
dom O1)
= X & (
dom O2)
= X;
let z,s be
object;
thus
[z, s]
in ((O1
OR O2)
\& O) implies
[z, s]
in ((O1
\& O)
AND (O2
\& O))
proof
assume
A2:
[z, s]
in ((O1
OR O2)
\& O);
then
reconsider z, s as
Element of X by
ZFMISC_1: 87;
s
in (z
. ((O1
OR O2)
\& O)) by
A2,
RELAT_1: 169;
then s
in ((z
. (O1
OR O2))
\& O) by
Th35;
then s
in (((z
. O1)
OR (z
. O2))
\& O) & (z
. O1)
<>
{} & (z
. O2)
<>
{} by
A1,
RELAT_1: 170,
RELSET_2: 10;
then s
in (((z
. O1)
\& O)
AND ((z
. O2)
\& O)) by
Th24;
then s
in ((z
. (O1
\& O))
AND ((z
. O2)
\& O)) by
Th35;
then s
in ((z
. (O1
\& O))
AND (z
. (O2
\& O))) by
Th35;
then s
in (z
. ((O1
\& O)
AND (O2
\& O))) by
RELSET_2: 11;
hence thesis by
RELAT_1: 169;
end;
assume
A3:
[z, s]
in ((O1
\& O)
AND (O2
\& O));
then
reconsider z, s as
Element of X by
ZFMISC_1: 87;
s
in (z
. ((O1
\& O)
AND (O2
\& O))) by
A3,
RELAT_1: 169;
then s
in ((z
. (O1
\& O))
AND (z
. (O2
\& O))) by
RELSET_2: 11;
then s
in ((z
. (O1
\& O))
AND ((z
. O2)
\& O)) by
Th35;
then s
in (((z
. O1)
\& O)
AND ((z
. O2)
\& O)) & (z
. O1)
<>
{} & (z
. O2)
<>
{} by
Th35,
A1,
RELAT_1: 170;
then s
in (((z
. O1)
OR (z
. O2))
\& O) by
Th24;
then s
in ((z
. (O1
OR O2))
\& O) by
RELSET_2: 10;
then s
in (z
. ((O1
OR O2)
\& O)) by
Th35;
hence thesis by
RELAT_1: 169;
end;
definition
let X, O;
::
MMLQUERY:def21
attr O is
filtering means
:
Def21: O
c= (
id X);
end
theorem ::
MMLQUERY:45
Th45: O is
filtering iff O
= (
id (
dom O))
proof
thus O is
filtering implies O
= (
id (
dom O))
proof
assume
A1: O
c= (
id X);
let z,s be
object;
thus
[z, s]
in O implies
[z, s]
in (
id (
dom O))
proof
assume
[z, s]
in O;
then z
in (
dom O) & z
= s by
A1,
RELAT_1:def 10,
XTUPLE_0:def 12;
hence thesis by
RELAT_1:def 10;
end;
assume
[z, s]
in (
id (
dom O));
then
A2: z
in (
dom O) & z
= s by
RELAT_1:def 10;
then
consider y be
object such that
A3:
[z, y]
in O by
XTUPLE_0:def 12;
thus thesis by
A1,
A2,
A3,
RELAT_1:def 10;
end;
assume O
= (
id (
dom O));
hence O
c= (
id X) by
SYSREL: 15;
end;
registration
let X, O;
cluster (
NOT O) ->
filtering;
coherence
proof
(
NOT O)
= (
id (X
\ (
dom O))) by
Th37;
hence (
NOT O)
c= (
id X) by
SYSREL: 15;
end;
end
registration
let X;
cluster
filtering for
Operation of X;
existence
proof
set O = the
Operation of X;
take (
NOT O);
thus thesis;
end;
end
reserve F,F1,F2 for
filtering
Operation of X;
registration
let X, F, O;
cluster (F
AND O) ->
filtering;
coherence
proof
let O1;
assume O1
= (F
AND O);
then O1
c= F & F
c= (
id X) by
Def21,
XBOOLE_1: 17;
hence O1
c= (
id X);
end;
cluster (O
AND F) ->
filtering;
coherence ;
cluster (F
BUTNOT O) ->
filtering;
coherence
proof
let O1;
assume O1
= (F
BUTNOT O);
then O1
c= F & F
c= (
id X) by
Def21,
XBOOLE_1: 36;
hence O1
c= (
id X);
end;
end
registration
let X, F1, F2;
cluster (F1
OR F2) ->
filtering;
coherence
proof
let O1;
assume
A1: O1
= (F1
OR F2);
F1
c= (
id X) & F2
c= (
id X) by
Def21;
hence O1
c= (
id X) by
A1,
XBOOLE_1: 8;
end;
end
theorem ::
MMLQUERY:46
Th46: z
in (x
. F) implies z
= x
proof
assume z
in (x
. F);
then
[x, z]
in F & F
c= (
id X) by
Def21,
RELAT_1: 169;
hence thesis by
RELAT_1:def 10;
end;
theorem ::
MMLQUERY:47
(L
| F)
= (L
WHERE F)
proof
thus (L
| F)
c= (L
WHERE F)
proof
let z be
object;
assume z
in (L
| F);
then
consider y such that
A1: z
in (y
. F) & y
in L by
Th23;
z
= y by
A1,
Th46;
hence thesis by
A1,
Th3;
end;
let z be
object;
assume
A2: z
in (L
WHERE F);
then
reconsider x = z as
Element of X;
A3: x
in L & (x
. F)
<>
{} by
A2,
Th3;
set y = the
Element of (x
. F);
A4:
[x, y]
in F by
A3,
RELAT_1: 169;
F
c= (
id X) by
Def21;
then x
= y by
A4,
RELAT_1:def 10;
hence thesis by
A3,
Th23;
end;
theorem ::
MMLQUERY:48
(
NOT (
NOT F))
= F
proof
thus (
NOT (
NOT F))
= (
id (X
\ (
dom (
NOT F)))) by
Th37
.= (
id (X
\ (
dom (
id (X
\ (
dom F)))))) by
Th37
.= (
id (X
\ (X
\ (
dom F)))) by
RELAT_1: 45
.= (
id (X
/\ (
dom F))) by
XBOOLE_1: 48
.= (
id (
dom F)) by
XBOOLE_1: 28
.= F by
Th45;
end;
theorem ::
MMLQUERY:49
(
NOT (F1
AND F2))
= ((
NOT F1)
OR (
NOT F2))
proof
A1: F1
= (
id (
dom F1)) & F2
= (
id (
dom F2)) by
Th45;
(
NOT (F1
AND F2))
= (
id (X
\ (
dom (F1
AND F2)))) by
Th37
.= (
id (X
\ (
dom (
id ((
dom F1)
AND (
dom F2)))))) by
A1,
SYSREL: 14
.= (
id (X
\ ((
dom F1)
AND (
dom F2)))) by
RELAT_1: 45
.= (
id ((X
\ (
dom F1))
\/ (X
\ (
dom F2)))) by
XBOOLE_1: 54
.= ((
id (X
\ (
dom F1)))
\/ (
id (X
\ (
dom F2)))) by
SYSREL: 14
.= ((
NOT F1)
\/ (
id (X
\ (
dom F2)))) by
Th37;
hence thesis by
Th37;
end;
theorem ::
MMLQUERY:50
Th50: (
dom (O
OR (
NOT O)))
= X
proof
thus (
dom (O
OR (
NOT O)))
= ((
dom O)
OR (
dom (
NOT O))) by
XTUPLE_0: 23
.= ((
dom O)
\/ (
dom (
id (X
\ (
dom O))))) by
Th37
.= ((
dom O)
OR (X
\ (
dom O))) by
RELAT_1: 45
.= ((
dom O)
\/ X) by
XBOOLE_1: 39
.= X by
XBOOLE_1: 12;
end;
theorem ::
MMLQUERY:51
(F
OR (
NOT F))
= (
id X)
proof
(
dom (F
OR (
NOT F)))
= X & (F
OR (
NOT F))
c= (
id X) by
Th50,
Def21;
hence thesis by
SYSREL: 17;
end;
theorem ::
MMLQUERY:52
Th52: (O
AND (
NOT O))
=
{}
proof
(
dom (O
AND (
NOT O)))
= (
dom (O
/\ (
id (X
\ (
dom O))))) by
Th37;
then
A1: (
dom (O
AND (
NOT O)))
c= ((
dom O)
/\ (
dom (
id (X
\ (
dom O))))) by
XTUPLE_0: 24;
((
dom O)
/\ (
dom (
id (X
\ (
dom O)))))
= ((
dom O)
/\ (X
\ (
dom O))) by
RELAT_1: 45
.= (((
dom O)
/\ X)
\ (
dom O)) by
XBOOLE_1: 49
.= ((
dom O)
\ (
dom O)) by
XBOOLE_1: 28
.=
{} by
XBOOLE_1: 37;
hence thesis by
A1,
RELAT_1: 41,
XBOOLE_1: 3;
end;
theorem ::
MMLQUERY:53
((O1
OR O2)
AND (
NOT O1))
c= O2
proof
((O1
OR O2)
AND (
NOT O1))
= ((O1
AND (
NOT O1))
OR (O2
AND (
NOT O1))) by
XBOOLE_1: 23
.= (
{}
\/ (O2
AND (
NOT O1))) by
Th52
.= (O2
AND (
NOT O1));
hence thesis by
XBOOLE_1: 17;
end;
begin
reserve i for
Element of
NAT ;
definition
let A be
FinSequence;
let a be
object;
::
MMLQUERY:def22
func
#occurrences (a,A) ->
Nat equals (
card { i : i
in (
dom A) & a
in (A
. i) });
coherence
proof
{ i : i
in (
dom A) & a
in (A
. i) }
c= (
dom A)
proof
let z be
object;
assume z
in { i : i
in (
dom A) & a
in (A
. i) };
then ex i st z
= i & i
in (
dom A) & a
in (A
. i);
hence thesis;
end;
hence thesis;
end;
end
theorem ::
MMLQUERY:54
Th54: for A be
FinSequence, a be
set holds (
#occurrences (a,A))
<= (
len A)
proof
let A be
FinSequence;
let a be
set;
{ i : i
in (
dom A) & a
in (A
. i) }
c= (
dom A)
proof
let z be
object;
assume z
in { i : i
in (
dom A) & a
in (A
. i) };
then ex i st z
= i & i
in (
dom A) & a
in (A
. i);
hence thesis;
end;
then (
Segm (
#occurrences (a,A)))
c= (
Segm (
card (
dom A))) & (
dom A)
= (
Seg (
len A)) & (
card (
Seg (
len A)))
= (
len A) by
CARD_1: 11,
FINSEQ_1: 57,
FINSEQ_1:def 3;
hence (
#occurrences (a,A))
<= (
len A) by
NAT_1: 39;
end;
theorem ::
MMLQUERY:55
Th55: for A be
FinSequence, a be
set holds A
<>
{} & (
#occurrences (a,A))
= (
len A) iff a
in (
meet (
rng A))
proof
let A be
FinSequence;
let a be
set;
A1: { i : i
in (
dom A) & a
in (A
. i) }
c= (
dom A)
proof
let z be
object;
assume z
in { i : i
in (
dom A) & a
in (A
. i) };
then ex i st z
= i & i
in (
dom A) & a
in (A
. i);
hence thesis;
end;
A2: (
dom A)
= (
Seg (
len A)) & (
card (
Seg (
len A)))
= (
len A) by
FINSEQ_1: 57,
FINSEQ_1:def 3;
hereby
assume A
<>
{} ;
then
A3: (
rng A)
<>
{} by
RELAT_1: 41;
assume
A4: (
#occurrences (a,A))
= (
len A);
A5: { i : i
in (
dom A) & a
in (A
. i) }
= (
dom A) by
A4,
A1,
A2,
CARD_2: 102;
now
let z;
assume z
in (
rng A);
then
consider s be
object such that
A6: s
in (
dom A) & z
= (A
. s) by
FUNCT_1:def 3;
consider i such that
A7: s
= i & i
in (
dom A) & a
in (A
. i) by
A5,
A6;
thus a
in z by
A6,
A7;
end;
hence a
in (
meet (
rng A)) by
A3,
SETFAM_1:def 1;
end;
assume
A8: a
in (
meet (
rng A));
thus A
<>
{} by
A8,
RELAT_1: 38,
SETFAM_1:def 1;
(
dom A)
c= { i : i
in (
dom A) & a
in (A
. i) }
proof
let z be
object;
assume
A9: z
in (
dom A);
then (A
. z)
in (
rng A) by
FUNCT_1:def 3;
then a
in (A
. z) by
A8,
SETFAM_1:def 1;
hence thesis by
A9;
end;
hence (
#occurrences (a,A))
= (
len A) by
A2,
A1,
XBOOLE_0:def 10;
end;
definition
let A be
FinSequence;
::
MMLQUERY:def23
func
max# A ->
Nat means
:
Def23: (for a be
set holds (
#occurrences (a,A))
<= it ) & (for n st for a be
set holds (
#occurrences (a,A))
<= n holds it
<= n);
existence
proof
defpred
P[
Nat] means for a be
set holds (
#occurrences (a,A))
<= $1;
P[(
len A)] by
Th54;
then
A1: ex n st
P[n];
consider n such that
A2:
P[n] & for m be
Nat st
P[m] holds n
<= m from
NAT_1:sch 5(
A1);
take n;
thus thesis by
A2;
end;
uniqueness
proof
let n1,n2 be
Nat such that
A3: (for a be
set holds (
#occurrences (a,A))
<= n1) & (for n st for a be
set holds (
#occurrences (a,A))
<= n holds n1
<= n) and
A4: (for a be
set holds (
#occurrences (a,A))
<= n2) & (for n st for a be
set holds (
#occurrences (a,A))
<= n holds n2
<= n);
n1
<= n2 & n2
<= n1 by
A3,
A4;
hence thesis by
XXREAL_0: 1;
end;
end
theorem ::
MMLQUERY:56
Th56: for A be
FinSequence holds (
max# A)
<= (
len A)
proof
let A be
FinSequence;
for a be
set holds (
#occurrences (a,A))
<= (
len A) by
Th54;
hence (
max# A)
<= (
len A) by
Def23;
end;
theorem ::
MMLQUERY:57
for A be
FinSequence, a be
set st (
#occurrences (a,A))
= (
len A) holds (
max# A)
= (
len A)
proof
let A be
FinSequence;
let a be
set;
assume (
#occurrences (a,A))
= (
len A);
then (
len A)
<= (
max# A) & (
max# A)
<= (
len A) by
Def23,
Th56;
hence (
max# A)
= (
len A) by
XXREAL_0: 1;
end;
definition
let X;
let A be
FinSequence of (
bool X);
let n be
Nat;
::
MMLQUERY:def24
func
ROUGH (A,n) ->
List of X equals
:
Def24: { x : n
<= (
#occurrences (x,A)) } if X
<>
{} ;
consistency ;
coherence
proof
assume
A1: X
<>
{} ;
{ x : n
<= (
#occurrences (x,A)) }
c= X
proof
let z be
object;
assume z
in { x : n
<= (
#occurrences (x,A)) };
then ex x st z
= x & n
<= (
#occurrences (x,A));
hence thesis by
A1;
end;
hence { x : n
<= (
#occurrences (x,A)) } is
List of X;
end;
let m be
Nat;
::
MMLQUERY:def25
func
ROUGH (A,n,m) ->
List of X equals
:
Def25: { x : n
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= m } if X
<>
{} ;
consistency ;
coherence
proof
assume
A2: X
<>
{} ;
{ x : n
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= m }
c= X
proof
let z be
object;
assume z
in { x : n
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= m };
then ex x st z
= x & n
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= m;
hence thesis by
A2;
end;
hence thesis;
end;
end
definition
let X;
let A be
FinSequence of (
bool X);
::
MMLQUERY:def26
func
ROUGH (A) ->
List of X equals (
ROUGH (A,(
max# A)));
coherence ;
end
theorem ::
MMLQUERY:58
for A be
FinSequence of (
bool X) holds (
ROUGH (A,n,(
len A)))
= (
ROUGH (A,n))
proof
let A be
FinSequence of (
bool X);
thus (
ROUGH (A,n,(
len A)))
c= (
ROUGH (A,n))
proof
let z be
object;
assume
A1: z
in (
ROUGH (A,n,(
len A)));
then z
in { x : n
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= (
len A) } by
Def25;
then ex x st z
= x & n
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= (
len A);
then z
in { x : n
<= (
#occurrences (x,A)) };
hence thesis by
A1,
Def24;
end;
let z be
object;
assume
A2: z
in (
ROUGH (A,n));
then z
in { x : n
<= (
#occurrences (x,A)) } by
Def24;
then
consider x such that
A3: z
= x & n
<= (
#occurrences (x,A));
(
#occurrences (x,A))
<= (
len A) by
Th54;
then z
in { x1 where x1 be
Element of X : n
<= (
#occurrences (x1,A)) & (
#occurrences (x1,A))
<= (
len A) } by
A3;
hence thesis by
A2,
Def25;
end;
theorem ::
MMLQUERY:59
for A be
FinSequence of (
bool X) holds n
<= m implies (
ROUGH (A,m))
c= (
ROUGH (A,n))
proof
let A be
FinSequence of (
bool X);
assume
A1: n
<= m;
let z be
object;
assume
A2: z
in (
ROUGH (A,m));
then z
in { x : m
<= (
#occurrences (x,A)) } by
Def24;
then
consider a such that
A3: z
= a & m
<= (
#occurrences (a,A));
n
<= (
#occurrences (a,A)) by
A1,
A3,
XXREAL_0: 2;
then z
in { x : n
<= (
#occurrences (x,A)) } by
A3;
hence z
in (
ROUGH (A,n)) by
A2,
Def24;
end;
theorem ::
MMLQUERY:60
for A be
FinSequence of (
bool X) holds for n1,n2,m1,m2 be
Nat st n1
<= m1 & n2
<= m2 holds (
ROUGH (A,m1,n2))
c= (
ROUGH (A,n1,m2))
proof
let A be
FinSequence of (
bool X);
let n1,n2,m1,m2 be
Nat;
assume
A1: n1
<= m1;
assume
A2: n2
<= m2;
let z be
object;
assume
A3: z
in (
ROUGH (A,m1,n2));
then z
in { x : m1
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= n2 } by
Def25;
then
consider a such that
A4: z
= a & m1
<= (
#occurrences (a,A)) & (
#occurrences (a,A))
<= n2;
n1
<= (
#occurrences (a,A)) & (
#occurrences (a,A))
<= m2 by
A1,
A2,
A4,
XXREAL_0: 2;
then z
in { x : n1
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= m2 } by
A4;
hence z
in (
ROUGH (A,n1,m2)) by
A3,
Def25;
end;
theorem ::
MMLQUERY:61
for A be
FinSequence of (
bool X) holds (
ROUGH (A,n,m))
c= (
ROUGH (A,n))
proof
let A be
FinSequence of (
bool X);
let z be
object;
assume
A1: z
in (
ROUGH (A,n,m));
then z
in { x : n
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= m } by
Def25;
then ex x st z
= x & n
<= (
#occurrences (x,A)) & (
#occurrences (x,A))
<= m;
then z
in { x : n
<= (
#occurrences (x,A)) };
hence z
in (
ROUGH (A,n)) by
A1,
Def24;
end;
theorem ::
MMLQUERY:62
Th62: for A be
FinSequence of (
bool X) st A
<>
{} holds (
ROUGH (A,(
len A)))
= (
meet (
rng A))
proof
let A be
FinSequence of (
bool X) such that
A1: A
<>
{} ;
thus (
ROUGH (A,(
len A)))
c= (
meet (
rng A))
proof
let z be
object;
assume z
in (
ROUGH (A,(
len A)));
then z
in { x : (
len A)
<= (
#occurrences (x,A)) } by
Def24;
then
consider x such that
A2: z
= x & (
len A)
<= (
#occurrences (x,A));
(
#occurrences (x,A))
<= (
len A) by
Th54;
hence thesis by
A1,
A2,
Th55,
XXREAL_0: 1;
end;
let z be
object;
assume
A3: z
in (
meet (
rng A));
then (
#occurrences (z,A))
= (
len A) by
Th55;
then z
in { x : (
len A)
<= (
#occurrences (x,A)) } by
A3;
hence thesis by
A3,
Def24;
end;
theorem ::
MMLQUERY:63
Th63: for A be
FinSequence of (
bool X) holds (
ROUGH (A,1))
= (
Union A)
proof
let A be
FinSequence of (
bool X);
thus (
ROUGH (A,1))
c= (
Union A)
proof
let z be
object;
assume z
in (
ROUGH (A,1));
then z
in { x : 1
<= (
#occurrences (x,A)) } by
Def24;
then
consider x such that
A1: z
= x & 1
<= (
#occurrences (x,A));
1
= (
0
+ 1);
then (
#occurrences (x,A))
>
0 by
A1,
NAT_1: 13;
then { i : i
in (
dom A) & x
in (A
. i) }
<>
{} ;
then
consider s be
object such that
A2: s
in { i : i
in (
dom A) & x
in (A
. i) } by
XBOOLE_0:def 1;
consider i such that
A3: s
= i & i
in (
dom A) & x
in (A
. i) by
A2;
thus thesis by
A1,
A3,
CARD_5: 2;
end;
let z be
object;
assume
A4: z
in (
Union A);
then
consider s be
object such that
A5: s
in (
dom A) & z
in (A
. s) by
CARD_5: 2;
s
in { i : i
in (
dom A) & z
in (A
. i) } by
A5;
then (
card
{s})
c= (
#occurrences (z,A)) by
CARD_1: 11,
ZFMISC_1: 31;
then (
Segm 1)
c= (
Segm (
#occurrences (z,A))) by
CARD_1: 30;
then 1
<= (
#occurrences (z,A)) by
NAT_1: 39;
then z
in { x : 1
<= (
#occurrences (x,A)) } by
A4;
hence thesis by
A4,
Def24;
end;
theorem ::
MMLQUERY:64
for L1,L2 be
List of X holds (
ROUGH (
<*L1, L2*>,2))
= (L1
AND L2)
proof
let L1,L2 be
List of X;
(
len
<*L1, L2*>)
= 2 & (
rng
<*L1, L2*>)
=
{L1, L2} & (
meet
{L1, L2})
= (L1
AND L2) by
FINSEQ_1: 44,
FINSEQ_2: 127,
SETFAM_1: 11;
hence (
ROUGH (
<*L1, L2*>,2))
= (L1
AND L2) by
Th62;
end;
theorem ::
MMLQUERY:65
for L1,L2 be
List of X holds (
ROUGH (
<*L1, L2*>,1))
= (L1
OR L2)
proof
let L1,L2 be
List of X;
(
len
<*L1, L2*>)
= 2 & (
rng
<*L1, L2*>)
=
{L1, L2} & (
union
{L1, L2})
= (L1
OR L2) & (
Union
<*L1, L2*>)
= (
union (
rng
<*L1, L2*>)) by
CARD_3:def 4,
FINSEQ_1: 44,
FINSEQ_2: 127,
ZFMISC_1: 75;
hence (
ROUGH (
<*L1, L2*>,1))
= (L1
OR L2) by
Th63;
end;
begin
definition
struct (
1-sorted)
ConstructorDB
(# the
carrier ->
set,
the
Constrs ->
List of the carrier,
the
ref-operation ->
Relation of the carrier, the Constrs #)
attr strict
strict;
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;
let S be
Subset of X;
let R be
Relation of X, S;
::
MMLQUERY:def27
func
@ R ->
Relation of X equals R;
coherence
proof
[:X, S:]
c=
[:X, X:] by
ZFMISC_1: 96;
hence thesis by
XBOOLE_1: 1;
end;
end
definition
let X be
ConstructorDB;
let a be
Element of X;
::
MMLQUERY:def28
func a
ref ->
List of X equals (a
. (
@ the
ref-operation of X));
coherence ;
::
MMLQUERY:def29
func a
occur ->
List of X equals (a
. ((
@ the
ref-operation of X)
~ ));
coherence ;
end
theorem ::
MMLQUERY:66
Th66: for X be
ConstructorDB holds for x,y be
Element of X holds x
in (y
ref ) iff y
in (x
occur )
proof
let X be
ConstructorDB;
let x,y be
Element of X;
hereby
assume x
in (y
ref );
then
[y, x]
in (
@ the
ref-operation of X) by
RELAT_1: 169;
then
[x, y]
in ((
@ the
ref-operation of X)
~ ) by
RELAT_1:def 7;
hence y
in (x
occur ) by
RELAT_1: 169;
end;
assume y
in (x
occur );
then
[x, y]
in ((
@ the
ref-operation of X)
~ ) by
RELAT_1: 169;
then
[y, x]
in (
@ the
ref-operation of X) by
RELAT_1:def 7;
hence x
in (y
ref ) by
RELAT_1: 169;
end;
definition
let X be
ConstructorDB;
::
MMLQUERY:def30
attr X is
ref-finite means
:
Def30: for x be
Element of X holds (x
ref ) is
finite;
end
registration
cluster
finite ->
ref-finite for
ConstructorDB;
coherence
proof
let X be
ConstructorDB;
assume
A1: the
carrier of X is
finite;
let x be
Element of X;
thus thesis by
A1;
end;
end
registration
cluster
finite non
empty for
ConstructorDB;
existence
proof
set X = the
finite non
empty
set;
set C = the
Subset of X;
set R = the
Relation of X, C;
take D =
ConstructorDB (# X, C, R #);
thus the
carrier of D is
finite non
empty;
end;
end
registration
let X be
ref-finite
ConstructorDB;
let x be
Element of X;
cluster (x
ref ) ->
finite;
coherence by
Def30;
end
definition
let X be
ConstructorDB;
let A be
FinSequence of the
Constrs of X;
::
MMLQUERY:def31
func
ATLEAST (A) ->
List of X equals
:
Def31: { x where x be
Element of X : (
rng A)
c= (x
ref ) } if the
carrier of X
<>
{} ;
consistency ;
coherence
proof
assume
A1: the
carrier of X
<>
{} ;
{ x where x be
Element of X : (
rng A)
c= (x
ref ) }
c= the
carrier of X
proof
let z be
object;
assume z
in { x where x be
Element of X : (
rng A)
c= (x
ref ) };
then ex x be
Element of X st z
= x & (
rng A)
c= (x
ref );
hence thesis by
A1;
end;
hence thesis;
end;
::
MMLQUERY:def32
func
ATMOST (A) ->
List of X equals
:
Def32: { x where x be
Element of X : (x
ref )
c= (
rng A) } if the
carrier of X
<>
{} ;
consistency ;
coherence
proof
assume
A2: the
carrier of X
<>
{} ;
{ x where x be
Element of X : (x
ref )
c= (
rng A) }
c= the
carrier of X
proof
let z be
object;
assume z
in { x where x be
Element of X : (x
ref )
c= (
rng A) };
then ex x be
Element of X st z
= x & (x
ref )
c= (
rng A);
hence thesis by
A2;
end;
hence thesis;
end;
::
MMLQUERY:def33
func
EXACTLY (A) ->
List of X equals
:
Def33: { x where x be
Element of X : (x
ref )
= (
rng A) } if the
carrier of X
<>
{} ;
consistency ;
coherence
proof
assume
A3: the
carrier of X
<>
{} ;
{ x where x be
Element of X : (x
ref )
= (
rng A) }
c= the
carrier of X
proof
let z be
object;
assume z
in { x where x be
Element of X : (x
ref )
= (
rng A) };
then ex x be
Element of X st z
= x & (x
ref )
= (
rng A);
hence thesis by
A3;
end;
hence thesis;
end;
let n be
Nat;
::
MMLQUERY:def34
func
ATLEAST- (A,n) ->
List of X equals
:
Def34: { x where x be
Element of X : (
card ((
rng A)
\ (x
ref )))
<= n } if the
carrier of X
<>
{} ;
consistency ;
coherence
proof
assume
A4: the
carrier of X
<>
{} ;
{ x where x be
Element of X : (
card ((
rng A)
\ (x
ref )))
<= n }
c= the
carrier of X
proof
let z be
object;
assume z
in { x where x be
Element of X : (
card ((
rng A)
\ (x
ref )))
<= n };
then ex x be
Element of X st z
= x & (
card ((
rng A)
\ (x
ref )))
<= n;
hence thesis by
A4;
end;
hence thesis;
end;
end
definition
let X be
ref-finite
ConstructorDB;
let A be
FinSequence of the
Constrs of X;
let n be
Nat;
::
MMLQUERY:def35
func
ATMOST+ (A,n) ->
List of X equals
:
Def35: { x where x be
Element of X : (
card ((x
ref )
\ (
rng A)))
<= n } if the
carrier of X
<>
{} ;
consistency ;
coherence
proof
assume
A1: the
carrier of X
<>
{} ;
{ x where x be
Element of X : (
card ((x
ref )
\ (
rng A)))
<= n }
c= the
carrier of X
proof
let z be
object;
assume z
in { x where x be
Element of X : (
card ((x
ref )
\ (
rng A)))
<= n };
then ex x be
Element of X st z
= x & (
card ((x
ref )
\ (
rng A)))
<= n;
hence thesis by
A1;
end;
hence thesis;
end;
let m be
Nat;
::
MMLQUERY:def36
func
EXACTLY+- (A,n,m) ->
List of X equals
:
Def36: { x where x be
Element of X : (
card ((x
ref )
\ (
rng A)))
<= n & (
card ((
rng A)
\ (x
ref )))
<= m } if the
carrier of X
<>
{} ;
consistency ;
coherence
proof
assume
A2: the
carrier of X
<>
{} ;
{ x where x be
Element of X : (
card ((x
ref )
\ (
rng A)))
<= n & (
card ((
rng A)
\ (x
ref )))
<= m }
c= the
carrier of X
proof
let z be
object;
assume z
in { x where x be
Element of X : (
card ((x
ref )
\ (
rng A)))
<= n & (
card ((
rng A)
\ (x
ref )))
<= m };
then ex x be
Element of X st z
= x & (
card ((x
ref )
\ (
rng A)))
<= n & (
card ((
rng A)
\ (x
ref )))
<= m;
hence thesis by
A2;
end;
hence thesis;
end;
end
reserve X for
ConstructorDB,
A for
FinSequence of the
Constrs of X,
x for
Element of X;
reserve Y for
ref-finite
ConstructorDB,
B for
FinSequence of the
Constrs of Y,
y for
Element of Y;
theorem ::
MMLQUERY:67
Th67: (
ATLEAST- (A,
0 ))
= (
ATLEAST A)
proof
per cases ;
suppose the
carrier of X
=
{} ;
then (
ATLEAST- (A,
0 ))
=
{} & (
ATLEAST A)
=
{} ;
hence thesis;
end;
suppose
A1: the
carrier of X
<>
{} ;
then
A2: (
ATLEAST- (A,
0 ))
= { x : (
card ((
rng A)
\ (x
ref )))
<=
0 } by
Def34;
A3: (
ATLEAST A)
= { x : (
rng A)
c= (x
ref ) } by
A1,
Def31;
thus (
ATLEAST- (A,
0 ))
c= (
ATLEAST A)
proof
let z be
object;
assume z
in (
ATLEAST- (A,
0 ));
then
consider x such that
A4: z
= x & (
card ((
rng A)
\ (x
ref )))
<=
0 by
A2;
((
rng A)
\ (x
ref ))
=
{} by
A4,
NAT_1: 3;
then (
rng A)
c= (x
ref ) by
XBOOLE_1: 37;
hence thesis by
A4,
A3;
end;
let z be
object;
assume z
in (
ATLEAST A);
then
consider x such that
A5: z
= x & (
rng A)
c= (x
ref ) by
A3;
((
rng A)
\ (x
ref ))
=
{} by
A5,
XBOOLE_1: 37;
then (
card ((
rng A)
\ (x
ref )))
=
0 ;
hence z
in (
ATLEAST- (A,
0 )) by
A2,
A5;
end;
end;
theorem ::
MMLQUERY:68
Th68: (
ATMOST+ (B,
0 ))
= (
ATMOST B)
proof
per cases ;
suppose the
carrier of Y
=
{} ;
then (
ATMOST+ (B,
0 ))
=
{} & (
ATMOST B)
=
{} ;
hence thesis;
end;
suppose
A1: the
carrier of Y
<>
{} ;
then
A2: (
ATMOST+ (B,
0 ))
= { y : (
card ((y
ref )
\ (
rng B)))
<=
0 } by
Def35;
A3: (
ATMOST B)
= { y : (y
ref )
c= (
rng B) } by
A1,
Def32;
thus (
ATMOST+ (B,
0 ))
c= (
ATMOST B)
proof
let z be
object;
assume z
in (
ATMOST+ (B,
0 ));
then
consider y such that
A4: z
= y & (
card ((y
ref )
\ (
rng B)))
<=
0 by
A2;
((y
ref )
\ (
rng B))
=
{} by
A4,
NAT_1: 3;
then (y
ref )
c= (
rng B) by
XBOOLE_1: 37;
hence thesis by
A4,
A3;
end;
let z be
object;
assume z
in (
ATMOST B);
then
consider y such that
A5: z
= y & (y
ref )
c= (
rng B) by
A3;
((y
ref )
\ (
rng B))
=
{} by
A5,
XBOOLE_1: 37;
then (
card ((y
ref )
\ (
rng B)))
=
0 ;
hence z
in (
ATMOST+ (B,
0 )) by
A2,
A5;
end;
end;
theorem ::
MMLQUERY:69
Th69: (
EXACTLY+- (B,
0 ,
0 ))
= (
EXACTLY B)
proof
per cases ;
suppose the
carrier of Y
=
{} ;
then (
EXACTLY+- (B,
0 ,
0 ))
=
{} & (
EXACTLY B)
=
{} ;
hence thesis;
end;
suppose
A1: the
carrier of Y
<>
{} ;
then
A2: (
EXACTLY+- (B,
0 ,
0 ))
= { y : (
card ((y
ref )
\ (
rng B)))
<=
0 & (
card ((
rng B)
\ (y
ref )))
<=
0 } by
Def36;
A3: (
EXACTLY B)
= { y : (y
ref )
= (
rng B) } by
A1,
Def33;
thus (
EXACTLY+- (B,
0 ,
0 ))
c= (
EXACTLY B)
proof
let z be
object;
assume z
in (
EXACTLY+- (B,
0 ,
0 ));
then
consider y such that
A4: z
= y & (
card ((y
ref )
\ (
rng B)))
<=
0 & (
card ((
rng B)
\ (y
ref )))
<=
0 by
A2;
((y
ref )
\ (
rng B))
=
{} & ((
rng B)
\ (y
ref ))
=
{} by
A4,
NAT_1: 3;
then (y
ref )
c= (
rng B) & (
rng B)
c= (y
ref ) by
XBOOLE_1: 37;
then (y
ref )
= (
rng B);
hence thesis by
A4,
A3;
end;
let z be
object;
assume z
in (
EXACTLY B);
then
consider y such that
A5: z
= y & (y
ref )
= (
rng B) by
A3;
((y
ref )
\ (
rng B))
=
{} & ((
rng B)
\ (y
ref ))
=
{} by
A5,
XBOOLE_1: 37;
then (
card ((y
ref )
\ (
rng B)))
=
0 & (
card ((
rng B)
\ (y
ref )))
=
0 ;
hence z
in (
EXACTLY+- (B,
0 ,
0 )) by
A2,
A5;
end;
end;
theorem ::
MMLQUERY:70
Th70: n
<= m implies (
ATLEAST- (A,n))
c= (
ATLEAST- (A,m))
proof
assume
A1: n
<= m;
let z be
object;
assume
A2: z
in (
ATLEAST- (A,n));
then z
in { x : (
card ((
rng A)
\ (x
ref )))
<= n } by
Def34;
then
consider x such that
A3: z
= x & (
card ((
rng A)
\ (x
ref )))
<= n;
(
card ((
rng A)
\ (x
ref )))
<= m by
A1,
A3,
XXREAL_0: 2;
then x
in { x1 where x1 be
Element of X : (
card ((
rng A)
\ (x1
ref )))
<= m };
hence thesis by
A2,
A3,
Def34;
end;
theorem ::
MMLQUERY:71
Th71: n
<= m implies (
ATMOST+ (B,n))
c= (
ATMOST+ (B,m))
proof
assume
A1: n
<= m;
let z be
object;
assume
A2: z
in (
ATMOST+ (B,n));
then z
in { y : (
card ((y
ref )
\ (
rng B)))
<= n } by
Def35;
then
consider y such that
A3: z
= y & (
card ((y
ref )
\ (
rng B)))
<= n;
(
card ((y
ref )
\ (
rng B)))
<= m by
A1,
A3,
XXREAL_0: 2;
then y
in { x1 where x1 be
Element of Y : (
card ((x1
ref )
\ (
rng B)))
<= m };
hence thesis by
A2,
A3,
Def35;
end;
theorem ::
MMLQUERY:72
Th72: for n1,n2,m1,m2 be
Nat st n1
<= m1 & n2
<= m2 holds (
EXACTLY+- (B,n1,n2))
c= (
EXACTLY+- (B,m1,m2))
proof
let n1,n2,m1,m2 be
Nat;
assume
A1: n1
<= m1 & n2
<= m2;
let z be
object;
assume
A2: z
in (
EXACTLY+- (B,n1,n2));
then z
in { y : (
card ((y
ref )
\ (
rng B)))
<= n1 & (
card ((
rng B)
\ (y
ref )))
<= n2 } by
Def36;
then
consider y such that
A3: z
= y & (
card ((y
ref )
\ (
rng B)))
<= n1 & (
card ((
rng B)
\ (y
ref )))
<= n2;
(
card ((y
ref )
\ (
rng B)))
<= m1 & (
card ((
rng B)
\ (y
ref )))
<= m2 by
A1,
A3,
XXREAL_0: 2;
then y
in { x1 where x1 be
Element of Y : (
card ((x1
ref )
\ (
rng B)))
<= m1 & (
card ((
rng B)
\ (x1
ref )))
<= m2 };
hence thesis by
A2,
A3,
Def36;
end;
theorem ::
MMLQUERY:73
(
ATLEAST A)
c= (
ATLEAST- (A,n))
proof
(
ATLEAST A)
= (
ATLEAST- (A,
0 )) &
0
<= n by
Th67,
NAT_1: 2;
hence thesis by
Th70;
end;
theorem ::
MMLQUERY:74
(
ATMOST B)
c= (
ATMOST+ (B,n))
proof
(
ATMOST B)
= (
ATMOST+ (B,
0 )) &
0
<= n by
Th68,
NAT_1: 2;
hence thesis by
Th71;
end;
theorem ::
MMLQUERY:75
(
EXACTLY B)
c= (
EXACTLY+- (B,n,m))
proof
(
EXACTLY B)
= (
EXACTLY+- (B,
0 ,
0 )) &
0
<= n &
0
<= m by
Th69,
NAT_1: 2;
hence thesis by
Th72;
end;
theorem ::
MMLQUERY:76
(
EXACTLY A)
= ((
ATLEAST A)
AND (
ATMOST A))
proof
thus (
EXACTLY A)
c= ((
ATLEAST A)
AND (
ATMOST A))
proof
let z be
object;
assume
A1: z
in (
EXACTLY A);
then z
in { x where x be
Element of X : (x
ref )
= (
rng A) } by
Def33;
then
consider x be
Element of X such that
A2: z
= x & (x
ref )
= (
rng A);
z
in { y where y be
Element of X : (
rng A)
c= (y
ref ) } by
A2;
then
A3: z
in (
ATLEAST A) by
A1,
Def31;
z
in { y where y be
Element of X : (y
ref )
c= (
rng A) } by
A2;
then z
in (
ATMOST A) by
A1,
Def32;
hence thesis by
A3,
XBOOLE_0:def 4;
end;
let z be
object;
assume
A4: z
in ((
ATLEAST A)
AND (
ATMOST A));
then
A5: z
in (
ATLEAST A) & z
in (
ATMOST A) by
XBOOLE_0:def 4;
then z
in { y where y be
Element of X : (y
ref )
c= (
rng A) } by
Def32;
then
consider a be
Element of X such that
A6: z
= a & (a
ref )
c= (
rng A);
z
in { y where y be
Element of X : (
rng A)
c= (y
ref ) } by
A5,
Def31;
then
consider b be
Element of X such that
A7: z
= b & (
rng A)
c= (b
ref );
z
= a & (a
ref )
= (
rng A) by
A6,
A7;
then z
in { y where y be
Element of X : (y
ref )
= (
rng A) };
hence thesis by
A4,
Def33;
end;
theorem ::
MMLQUERY:77
(
EXACTLY+- (B,n,m))
= ((
ATLEAST- (B,m))
AND (
ATMOST+ (B,n)))
proof
thus (
EXACTLY+- (B,n,m))
c= ((
ATLEAST- (B,m))
AND (
ATMOST+ (B,n)))
proof
let z be
object;
assume
A1: z
in (
EXACTLY+- (B,n,m));
then z
in { x where x be
Element of Y : (
card ((x
ref )
\ (
rng B)))
<= n & (
card ((
rng B)
\ (x
ref )))
<= m } by
Def36;
then
consider x be
Element of Y such that
A2: z
= x & (
card ((x
ref )
\ (
rng B)))
<= n & (
card ((
rng B)
\ (x
ref )))
<= m;
z
in { y : (
card ((
rng B)
\ (y
ref )))
<= m } by
A2;
then
A3: z
in (
ATLEAST- (B,m)) by
A1,
Def34;
z
in { y : (
card ((y
ref )
\ (
rng B)))
<= n } by
A2;
then z
in (
ATMOST+ (B,n)) by
A1,
Def35;
hence z
in ((
ATLEAST- (B,m))
AND (
ATMOST+ (B,n))) by
A3,
XBOOLE_0:def 4;
end;
let z be
object;
assume
A4: z
in ((
ATLEAST- (B,m))
AND (
ATMOST+ (B,n)));
then
A5: z
in (
ATLEAST- (B,m)) & z
in (
ATMOST+ (B,n)) by
XBOOLE_0:def 4;
then z
in { y : (
card ((y
ref )
\ (
rng B)))
<= n } by
Def35;
then
A6: ex y st z
= y & (
card ((y
ref )
\ (
rng B)))
<= n;
z
in { y : (
card ((
rng B)
\ (y
ref )))
<= m } by
A5,
Def34;
then ex y st z
= y & (
card ((
rng B)
\ (y
ref )))
<= m;
then z
in { y : (
card ((y
ref )
\ (
rng B)))
<= n & (
card ((
rng B)
\ (y
ref )))
<= m } by
A6;
hence thesis by
A4,
Def36;
end;
theorem ::
MMLQUERY:78
Th78: A
<>
{} implies (
ATLEAST A)
= (
meet { (x
occur ) : x
in (
rng A) })
proof
assume A
<>
{} ;
then (
rng A)
<>
{} by
RELAT_1: 41;
then
consider s be
object such that
A1: s
in (
rng A) by
XBOOLE_0:def 1;
s
in the
Constrs of X & the
Constrs of X
c= the
carrier of X by
A1;
then
reconsider s as
Element of X;
A2: (s
occur )
in { (x
occur ) : x
in (
rng A) } by
A1;
thus (
ATLEAST A)
c= (
meet { (x
occur ) : x
in (
rng A) })
proof
let z be
object;
assume z
in (
ATLEAST A);
then z
in { y where y be
Element of X : (
rng A)
c= (y
ref ) } by
Def31;
then
consider a be
Element of X such that
A3: z
= a & (
rng A)
c= (a
ref );
now
let Y be
set;
assume Y
in { (x
occur ) : x
in (
rng A) };
then
consider x such that
A4: Y
= (x
occur ) & x
in (
rng A);
thus z
in Y by
A3,
A4,
Th66;
end;
hence thesis by
A2,
SETFAM_1:def 1;
end;
let z be
object;
assume
A5: z
in (
meet { (x
occur ) : x
in (
rng A) });
then
A6: z
in (s
occur ) by
A2,
SETFAM_1:def 1;
then
reconsider z as
Element of X;
(
rng A)
c= (z
ref )
proof
let s be
object;
assume
A7: s
in (
rng A);
then s
in the
Constrs of X;
then
reconsider s as
Element of X;
(s
occur )
in { (x
occur ) : x
in (
rng A) } by
A7;
then z
in (s
occur ) by
A5,
SETFAM_1:def 1;
hence thesis by
Th66;
end;
then z
in { x : (
rng A)
c= (x
ref ) };
hence thesis by
A6,
Def31;
end;
theorem ::
MMLQUERY:79
for c1,c2 be
Element of X holds A
=
<*c1, c2*> implies (
ATLEAST A)
= ((c1
occur )
AND (c2
occur ))
proof
let c1,c2 be
Element of X;
assume
A1: A
=
<*c1, c2*>;
then
A2: (
rng A)
=
{c1, c2} by
FINSEQ_2: 127;
A3: { (x
occur ) : x
in (
rng A) }
=
{(c1
occur ), (c2
occur )}
proof
thus { (x
occur ) : x
in (
rng A) }
c=
{(c1
occur ), (c2
occur )}
proof
let z be
object;
assume z
in { (x
occur ) : x
in (
rng A) };
then
consider x such that
A4: z
= (x
occur ) & x
in (
rng A);
x
= c1 or x
= c2 by
A2,
A4,
TARSKI:def 2;
hence thesis by
A4,
TARSKI:def 2;
end;
let z be
object;
assume z
in
{(c1
occur ), (c2
occur )};
then
A5: z
= (c1
occur ) or z
= (c2
occur ) by
TARSKI:def 2;
c1
in (
rng A) & c2
in (
rng A) by
A2,
TARSKI:def 2;
hence thesis by
A5;
end;
thus (
ATLEAST A)
= (
meet { (x
occur ) : x
in (
rng A) }) by
A1,
Th78
.= ((c1
occur )
AND (c2
occur )) by
A3,
SETFAM_1: 11;
end;