MMLQUER2: The Semantics of MML Query -- Ordering

proof end;

end;

registration

let R1, R2 be antisymmetric Relation;

cluster R1 \, R2 -> antisymmetric ;

proof end;

end;

definition

let X be set ;
let R be Relation of X;

attr R is beta-transitive means :Def4: :: MMLQUER2:def 4
for x, y being Element of X st x,y nin R holds
for z being Element of X st x,z in R holds
y,z in R;

end;

:: deftheorem Def4 defines beta-transitive MMLQUER2:def 4 :

registration

let X be set ;

cluster connected transitive total -> beta-transitive for Element of bool [:X,X:];

proof end;

end;

registration

let X be set ;

cluster Relation-like X -defined X -valued reflexive antisymmetric connected transitive total for Element of bool [:X,X:];

proof end;

end;

registration

let X be set ;
let R1 be transitive beta-transitive Relation of X;
let R2 be transitive Relation of X;

cluster R1 \, R2 -> transitive ;

proof end;

end;

registration

let X be set ;
let R1 be Relation of X;
let R2 be reflexive total Relation of X;

cluster R1 \, R2 -> reflexive total for Relation of X;

proof end;

end;

registration

let X be set ;
let R1 be Relation of X;
let R2 be reflexive connected total Relation of X;

cluster R1 \, R2 -> connected ;

proof end;

end;

theorem :: MMLQUER2:12

for R, R1, R2 being Relation holds (R \, R1) \, R2 = R \, (R1 \, R2)

proof end;

theorem :: MMLQUER2:13

for X being set
for R being reflexive connected total Relation of X
for R2 being Relation of X holds R \, R2 = R

proof end;

definition

let X be set ;
let f be Function of X,NAT;

func value_of f -> Relation of X means :Def5: :: MMLQUER2:def 5
for x, y being set holds
( x,y in it iff ( x in X & y in X & f . x < f . y ) );

proof end;

proof end;

end;

:: deftheorem Def5 defines value_of MMLQUER2:def 5 :

registration

let X be set ;
let f be Function of X,NAT;

cluster value_of f -> antisymmetric transitive beta-transitive ;

proof end;

end;

definition

let X be finite set ;
let O be Operation of X;

func number_of O -> Function of X,NAT means :Def6: :: MMLQUER2:def 6
for x being Element of X holds it . x = card (x . O);

proof end;

proof end;

end;

:: deftheorem Def6 defines number_of MMLQUER2:def 6 :

theorem :: MMLQUER2:14

for X being finite set
for O being Operation of X
for x, y being Element of X holds
( x,y in value_of (number_of O) iff card (x . O) < card (y . O) )

proof end;

definition

let X be set ;
let O be Operation of X;

func first O -> Relation of X means :Def7: :: MMLQUER2:def 7
for x, y being Element of X holds
( x,y in it iff ( x . O <> {} & y . O = {} ) );

proof end;

proof end;

end;

:: deftheorem Def7 defines first MMLQUER2:def 7 :

registration

let X be set ;
let O be Operation of X;

cluster first O -> antisymmetric transitive beta-transitive ;

proof end;

end;

definition

let A be FinSequence;
let x be object ;

func A <- x -> set equals :: MMLQUER2:def 8
meet (A " {x});

coherence ;

end;

:: deftheorem defines <- MMLQUER2:def 8 :

registration

let A be FinSequence;
let x be set ;

cluster A <- x -> natural ;

proof end;

end;

theorem :: MMLQUER2:15

for x being set
for A being FinSequence st x nin rng A holds
A <- x = 0

proof end;

theorem Th16: :: MMLQUER2:16

for x being set
for A being FinSequence st x in rng A holds
( A <- x in dom A & x = A . (A <- x) )

proof end;

theorem :: MMLQUER2:17

for x being set
for A being FinSequence st A <- x = 0 holds
x nin rng A

proof end;

definition

let X be set ;
let A be FinSequence;
let f be Function;

func resource (X,A,f) -> Relation of X means :Def9: :: MMLQUER2:def 9
for x, y being set holds
( x,y in it iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) );

proof end;

proof end;

end;

:: deftheorem Def9 defines resource MMLQUER2:def 9 :

registration

let X be set ;
let A be FinSequence;
let f be Function;

cluster resource (X,A,f) -> antisymmetric transitive beta-transitive ;

proof end;

end;

definition

let X be set ;
let R be Relation of X;
let n be Nat;
:: original: iter
redefine func iter (R,n) -> Relation of X;
coherence

proof end;

end;

theorem Th18: :: MMLQUER2:18

for X being set
for R being Relation
for n, m being Nat st (iter (R,n)) .: X = {} & m >= n holds
(iter (R,m)) .: X = {}

proof end;

theorem Th19: :: MMLQUER2:19

for X being set
for R being Relation st ( for n being Nat holds (iter (R,n)) .: X <> {} ) & X is finite holds
ex x being set st
( x in X & ( for n being Nat holds Im ((iter (R,n)),x) <> {} ) )

proof end;

theorem Th20: :: MMLQUER2:20

for X being set
for R being Relation st R is co-well_founded & R is irreflexive & X is finite & R is finite holds
ex n being Nat st (iter (R,n)) .: X = {}

proof end;

definition

let X be set ;
let O be Operation of X;
assume A1: ( O is co-well_founded & O is irreflexive & O is finite ) ;

func iteration_of O -> Relation of X means :Def10: :: MMLQUER2:def 10
ex f being Function of X,NAT st
( it = value_of f & ( for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ) );

proof end;

proof end;

end;

:: deftheorem Def10 defines iteration_of MMLQUER2:def 10 :

registration

cluster empty Relation-like -> irreflexive co-well_founded for set ;

proof end;

end;

registration

let X be set ;

cluster empty Relation-like X -defined X -valued for Element of bool [:X,X:];

proof end;

end;

registration

let X be set ;
let O be irreflexive finite co-well_founded Operation of X;

cluster iteration_of O -> antisymmetric transitive beta-transitive ;

proof end;

end;

registration

let X be finite set ;

cluster reflexive antisymmetric transitive total -> well_founded for Element of bool [:X,X:];

proof end;

end;

registration

let X be finite set ;

cluster reflexive antisymmetric connected transitive total -> connected well-ordering for Element of bool [:X,X:];

coherence ;

end;

definition

let X be set ;
let R be connected Order of X;
let S be finite Subset of X;

func order (S,R) -> XFinSequence of X means :Def11: :: MMLQUER2:def 11
( rng it = S & it is one-to-one & ( for i, j being Nat st i in dom it & j in dom it holds
( i <= j iff it . i,it . j in R ) ) );

proof end;

proof end;

end;

:: deftheorem Def11 defines order MMLQUER2:def 11 :

theorem :: MMLQUER2:21

for X being set
for S1, S2 being finite Subset of X
for R being connected Order of X holds
( order ((S1 \/ S2),R) = (order (S1,R)) ^ (order (S2,R)) iff for x, y being set st x in S1 & y in S2 holds
( x <> y & x,y in R ) )

proof end;

definition

let X be finite set ;
let O be Operation of X;
let R be connected Order of X;

func value_of (O,R) -> Relation of X means :Def12: :: MMLQUER2:def 12
for x, y being Element of X holds
( x,y in it iff ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def12 defines value_of MMLQUER2:def 12 :

registration

let X be finite set ;
let O be Operation of X;
let R1 be connected Order of X;

cluster value_of (O,R1) -> antisymmetric transitive beta-transitive ;