:: The Semantics of MML Query -- Ordering
:: by Grzegorz Bancerek
::
:: Copyright (c) 2012-2021 Association of Mizar Users

theorem :: MMLQUER2:1
for X being set
for R being Relation of X holds field R c= X
proof end;

theorem Th2: :: MMLQUER2:2
for X, x, y being set
for R being Relation of X st x,y in R holds
( x in X & y in X ) by ZFMISC_1:87;

theorem Th3: :: MMLQUER2:3
for X, Y being set holds (id X) .: Y = X /\ Y
proof end;

theorem Th4: :: MMLQUER2:4
for X being set
for R being Relation
for x, y being set holds
( [x,y] in R |_2 X iff ( x in X & y in X & [x,y] in R ) )
proof end;

theorem :: MMLQUER2:5
canceled;

::\$CT
theorem Th6: :: MMLQUER2:6
for X being set
for R being reflexive total Relation of X
for S being Subset of X holds R |_2 S is reflexive total Relation of S
proof end;

theorem :: MMLQUER2:7
canceled;

Th7: for f, g being Sequence holds rng (f ^ g) = (rng f) \/ (rng g)
by ORDINAL4:2;

definition
let R be Relation;
redefine attr R is transitive means :Def1: :: MMLQUER2:def 1
for x, y, z being set st x,y in R & y,z in R holds
x,z in R;
compatibility
( R is transitive iff for x, y, z being set st x,y in R & y,z in R holds
x,z in R )
proof end;
redefine attr R is antisymmetric means :Def2: :: MMLQUER2:def 2
for x, y being set st x,y in R & y,x in R holds
x = y;
compatibility
( R is antisymmetric iff for x, y being set st x,y in R & y,x in R holds
x = y )
proof end;
end;

:: deftheorem Def1 defines transitive MMLQUER2:def 1 :
for R being Relation holds
( R is transitive iff for x, y, z being set st x,y in R & y,z in R holds
x,z in R );

:: deftheorem Def2 defines antisymmetric MMLQUER2:def 2 :
for R being Relation holds
( R is antisymmetric iff for x, y being set st x,y in R & y,x in R holds
x = y );

theorem :: MMLQUER2:8
for X being non empty set
for R being connected total Relation of X
for x, y being Element of X holds
( not x <> y or x,y in R or y,x in R )
proof end;

definition
let R1, R2 be Relation;
func R1 \, R2 -> Relation equals :: MMLQUER2:def 3
R1 \/ (R2 \ (R1 ~));
coherence
R1 \/ (R2 \ (R1 ~)) is Relation
;
end;

:: deftheorem defines \, MMLQUER2:def 3 :
for R1, R2 being Relation holds R1 \, R2 = R1 \/ (R2 \ (R1 ~));

theorem Th9: :: MMLQUER2:9
for R1, R2 being Relation
for x, y being set holds
( x,y in R1 \, R2 iff ( x,y in R1 or ( y,x nin R1 & x,y in R2 ) ) )
proof end;

theorem Th10: :: MMLQUER2:10
for R1, R2 being Relation holds field (R1 \, R2) = (field R1) \/ (field R2)
proof end;

theorem Th11: :: MMLQUER2:11
for R1, R2 being Relation holds R1 \, R2 c= R1 \/ R2
proof end;

definition
let X be set ;
let R1, R2 be Relation of X;
:: original: \,
redefine func R1 \, R2 -> Relation of X;
coherence
R1 \, R2 is Relation of X
proof end;
end;

registration
let R1, R2 be reflexive Relation;
cluster R1 \, R2 -> reflexive ;
coherence
R1 \, R2 is reflexive
proof end;
end;

registration
let R1, R2 be antisymmetric Relation;
cluster R1 \, R2 -> antisymmetric ;
coherence
R1 \, R2 is 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 :
for X being set
for R being Relation of X holds
( R is beta-transitive iff 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 );

registration
let X be set ;
coherence
for b1 being Relation of X st b1 is connected & b1 is total & b1 is transitive holds
b1 is beta-transitive
proof end;
end;

registration
let X be set ;
existence
ex b1 being Order of X st b1 is connected
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 ;
coherence
R1 \, R2 is 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;
coherence
for b1 being Relation of X st b1 = R1 \, R2 holds
( b1 is total & b1 is reflexive )
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 ;
coherence
R1 \, R2 is 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 ) );
existence
ex b1 being Relation of X st
for x, y being set holds
( x,y in b1 iff ( x in X & y in X & f . x < f . y ) )
proof end;
uniqueness
for b1, b2 being Relation of X st ( for x, y being set holds
( x,y in b1 iff ( x in X & y in X & f . x < f . y ) ) ) & ( for x, y being set holds
( x,y in b2 iff ( x in X & y in X & f . x < f . y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines value_of MMLQUER2:def 5 :
for X being set
for f being Function of X,NAT
for b3 being Relation of X holds
( b3 = value_of f iff for x, y being set holds
( x,y in b3 iff ( x in X & y in X & f . x < f . y ) ) );

registration
let X be set ;
let f be Function of X,NAT;
coherence
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);
existence
ex b1 being Function of X,NAT st
for x being Element of X holds b1 . x = card (x . O)
proof end;
uniqueness
for b1, b2 being Function of X,NAT st ( for x being Element of X holds b1 . x = card (x . O) ) & ( for x being Element of X holds b2 . x = card (x . O) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines number_of MMLQUER2:def 6 :
for X being finite set
for O being Operation of X
for b3 being Function of X,NAT holds
( b3 = number_of O iff for x being Element of X holds b3 . x = card (x . O) );

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 () 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 = {} ) );
existence
ex b1 being Relation of X st
for x, y being Element of X holds
( x,y in b1 iff ( x . O <> {} & y . O = {} ) )
proof end;
uniqueness
for b1, b2 being Relation of X st ( for x, y being Element of X holds
( x,y in b1 iff ( x . O <> {} & y . O = {} ) ) ) & ( for x, y being Element of X holds
( x,y in b2 iff ( x . O <> {} & y . O = {} ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines first MMLQUER2:def 7 :
for X being set
for O being Operation of X
for b3 being Relation of X holds
( b3 = first O iff for x, y being Element of X holds
( x,y in b3 iff ( x . O <> {} & y . O = {} ) ) );

registration
let X be set ;
let O be Operation of X;
coherence
proof end;
end;

definition
let A be FinSequence;
let x be object ;
func A <- x -> set equals :: MMLQUER2:def 8
meet (A " {x});
coherence
meet (A " {x}) is set
;
end;

:: deftheorem defines <- MMLQUER2:def 8 :
for A being FinSequence
for x being object holds A <- x = meet (A " {x});

registration
let A be FinSequence;
let x be set ;
cluster A <- x -> natural ;
coherence
A <- x is 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 ) ) );
existence
ex b1 being Relation of X st
for x, y being set holds
( x,y in b1 iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) )
proof end;
uniqueness
for b1, b2 being Relation of X st ( for x, y being set holds
( x,y in b1 iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) ) & ( for x, y being set holds
( x,y in b2 iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines resource MMLQUER2:def 9 :
for X being set
for A being FinSequence
for f being Function
for b4 being Relation of X holds
( b4 = resource (X,A,f) iff for x, y being set holds
( x,y in b4 iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) );

registration
let X be set ;
let A be FinSequence;
let f be Function;
coherence
( resource (X,A,f) is antisymmetric & resource (X,A,f) is transitive & resource (X,A,f) is 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
iter (R,n) is Relation of X
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))) = {} ) ) );
existence
ex b1 being Relation of X ex f being Function of X,NAT st
( b1 = 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;
uniqueness
for b1, b2 being Relation of X st ex f being Function of X,NAT st
( b1 = 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))) = {} ) ) ) & ex f being Function of X,NAT st
( b2 = 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))) = {} ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines iteration_of MMLQUER2:def 10 :
for X being set
for O being Operation of X st O is co-well_founded & O is irreflexive & O is finite holds
for b3 being Relation of X holds
( b3 = iteration_of O iff ex f being Function of X,NAT st
( b3 = 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))) = {} ) ) ) );

registration
coherence
for b1 being Relation st b1 is empty holds
( b1 is irreflexive & b1 is co-well_founded )
proof end;
end;

registration
let X be set ;
existence
ex b1 being Operation of X st b1 is empty
proof end;
end;

registration
let X be set ;
let O be irreflexive finite co-well_founded Operation of X;
coherence
proof end;
end;

registration
let X be finite set ;
coherence
for b1 being Order of X holds b1 is well_founded
proof end;
end;

registration
let X be finite set ;
coherence
for b1 being connected Order of X holds b1 is well-ordering
;
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 ) ) );
existence
ex b1 being XFinSequence of X st
( rng b1 = S & b1 is one-to-one & ( for i, j being Nat st i in dom b1 & j in dom b1 holds
( i <= j iff b1 . i,b1 . j in R ) ) )
proof end;
uniqueness
for b1, b2 being XFinSequence of X st rng b1 = S & b1 is one-to-one & ( for i, j being Nat st i in dom b1 & j in dom b1 holds
( i <= j iff b1 . i,b1 . j in R ) ) & rng b2 = S & b2 is one-to-one & ( for i, j being Nat st i in dom b2 & j in dom b2 holds
( i <= j iff b2 . i,b2 . j in R ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines order MMLQUER2:def 11 :
for X being set
for R being connected Order of X
for S being finite Subset of X
for b4 being XFinSequence of X holds
( b4 = order (S,R) iff ( rng b4 = S & b4 is one-to-one & ( for i, j being Nat st i in dom b4 & j in dom b4 holds
( i <= j iff b4 . i,b4 . j in R ) ) ) );

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 ) ) ) );
existence
ex b1 being Relation of X st
for x, y being Element of X holds
( x,y in b1 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;
uniqueness
for b1, b2 being Relation of X st ( for x, y being Element of X holds
( x,y in b1 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 ) ) ) ) ) & ( for x, y being Element of X holds
( x,y in b2 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 ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines value_of MMLQUER2:def 12 :
for X being finite set
for O being Operation of X
for R being connected Order of X
for b4 being Relation of X holds
( b4 = value_of (O,R) iff for x, y being Element of X holds
( x,y in b4 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 ) ) ) ) );

registration
let X be finite set ;
let O be Operation of X;
let R1 be connected Order of X;
coherence
( value_of (O,R1) is antisymmetric & value_of (O,R1) is transitive & value_of (O,R1) is beta-transitive )
proof end;
end;