:: by Grzegorz Bancerek

::

:: Received December 1, 2012

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

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

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

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;

definition

let R be Relation;

( R is transitive iff for x, y, z being set st x,y in R & y,z in R holds

x,z in R )

( R is antisymmetric iff for x, y being set st x,y in R & y,x in R holds

x = y )

end;
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 for x, y, z being set st x,y in R & y,z in R holds

x,z in R;

( 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 for x, y being set st x,y in R & y,x in R holds

x = y;

( R is antisymmetric iff for x, y being set st x,y in R & y,x in R holds

x = y )

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

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

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 )

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;

:: deftheorem defines \, MMLQUER2:def 3 :

for R1, R2 being Relation holds R1 \, R2 = R1 \/ (R2 \ (R1 ~));

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

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;

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

end;
let R1, R2 be Relation of X;

:: original: \,

redefine func R1 \, R2 -> Relation of X;

coherence

R1 \, R2 is Relation of X

proof end;

registration
end;

definition

let X be set ;

let R be Relation of X;

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

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;

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

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 b_{1} being Relation of X st b_{1} is connected & b_{1} is total & b_{1} is transitive holds

b_{1} is beta-transitive

end;
coherence

for b

b

proof end;

registration

let X be set ;

ex b_{1} being Order of X st b_{1} is connected

end;
cluster Relation-like X -defined X -valued reflexive antisymmetric connected transitive total for Order of ;

existence ex b

proof end;

registration

let X be set ;

let R1 be transitive beta-transitive Relation of X;

let R2 be transitive Relation of X;

coherence

R1 \, R2 is transitive

end;
let R1 be transitive beta-transitive Relation of X;

let R2 be transitive Relation of X;

coherence

R1 \, R2 is transitive

proof end;

registration

let X be set ;

let R1 be Relation of X;

let R2 be reflexive total Relation of X;

coherence

for b_{1} being Relation of X st b_{1} = R1 \, R2 holds

( b_{1} is total & b_{1} is reflexive )

end;
let R1 be Relation of X;

let R2 be reflexive total Relation of X;

coherence

for b

( b

proof end;

registration

let X be set ;

let R1 be Relation of X;

let R2 be reflexive connected total Relation of X;

coherence

R1 \, R2 is connected

end;
let R1 be Relation of X;

let R2 be reflexive connected total Relation of X;

coherence

R1 \, R2 is connected

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

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;

ex b_{1} being Relation of X st

for x, y being set holds

( x,y in b_{1} iff ( x in X & y in X & f . x < f . y ) )

for b_{1}, b_{2} being Relation of X st ( for x, y being set holds

( x,y in b_{1} iff ( x in X & y in X & f . x < f . y ) ) ) & ( for x, y being set holds

( x,y in b_{2} iff ( x in X & y in X & f . x < f . y ) ) ) holds

b_{1} = b_{2}

end;
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 for x, y being set holds

( x,y in it iff ( x in X & y in X & f . x < f . y ) );

ex b

for x, y being set holds

( x,y in b

proof end;

uniqueness for b

( x,y in b

( x,y in b

b

proof end;

:: deftheorem Def5 defines value_of MMLQUER2:def 5 :

for X being set

for f being Function of X,NAT

for b_{3} being Relation of X holds

( b_{3} = value_of f iff for x, y being set holds

( x,y in b_{3} iff ( x in X & y in X & f . x < f . y ) ) );

for X being set

for f being Function of X,NAT

for b

( b

( x,y in b

registration

let X be set ;

let f be Function of X,NAT;

coherence

( value_of f is antisymmetric & value_of f is transitive & value_of f is beta-transitive )

end;
let f be Function of X,NAT;

coherence

( value_of f is antisymmetric & value_of f is transitive & value_of f is beta-transitive )

proof end;

definition

let X be finite set ;

let O be Operation of X;

ex b_{1} being Function of X,NAT st

for x being Element of X holds b_{1} . x = card (x . O)

for b_{1}, b_{2} being Function of X,NAT st ( for x being Element of X holds b_{1} . x = card (x . O) ) & ( for x being Element of X holds b_{2} . x = card (x . O) ) holds

b_{1} = b_{2}

end;
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 for x being Element of X holds it . x = card (x . O);

ex b

for x being Element of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines number_of MMLQUER2:def 6 :

for X being finite set

for O being Operation of X

for b_{3} being Function of X,NAT holds

( b_{3} = number_of O iff for x being Element of X holds b_{3} . x = card (x . O) );

for X being finite set

for O being Operation of X

for b

( b

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

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;

ex b_{1} being Relation of X st

for x, y being Element of X holds

( x,y in b_{1} iff ( x . O <> {} & y . O = {} ) )

for b_{1}, b_{2} being Relation of X st ( for x, y being Element of X holds

( x,y in b_{1} iff ( x . O <> {} & y . O = {} ) ) ) & ( for x, y being Element of X holds

( x,y in b_{2} iff ( x . O <> {} & y . O = {} ) ) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of X holds

( x,y in it iff ( x . O <> {} & y . O = {} ) );

ex b

for x, y being Element of X holds

( x,y in b

proof end;

uniqueness for b

( x,y in b

( x,y in b

b

proof end;

:: deftheorem Def7 defines first MMLQUER2:def 7 :

for X being set

for O being Operation of X

for b_{3} being Relation of X holds

( b_{3} = first O iff for x, y being Element of X holds

( x,y in b_{3} iff ( x . O <> {} & y . O = {} ) ) );

for X being set

for O being Operation of X

for b

( b

( x,y in b

registration

let X be set ;

let O be Operation of X;

coherence

( first O is antisymmetric & first O is transitive & first O is beta-transitive )

end;
let O be Operation of X;

coherence

( first O is antisymmetric & first O is transitive & first O is beta-transitive )

proof end;

:: deftheorem defines <- MMLQUER2:def 8 :

for A being FinSequence

for x being object holds A <- x = meet (A " {x});

for A being FinSequence

for x being object holds A <- x = meet (A " {x});

definition

let X be set ;

let A be FinSequence;

let f be Function;

ex b_{1} being Relation of X st

for x, y being set holds

( x,y in b_{1} iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) )

for b_{1}, b_{2} being Relation of X st ( for x, y being set holds

( x,y in b_{1} 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 b_{2} iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) ) holds

b_{1} = b_{2}

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

ex b

for x, y being set holds

( x,y in b

proof end;

uniqueness for b

( x,y in b

( x,y in b

b

proof end;

:: deftheorem Def9 defines resource MMLQUER2:def 9 :

for X being set

for A being FinSequence

for f being Function

for b_{4} being Relation of X holds

( b_{4} = resource (X,A,f) iff for x, y being set holds

( x,y in b_{4} iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) );

for X being set

for A being FinSequence

for f being Function

for b

( b

( x,y in b

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 )

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

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

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

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

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

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

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

ex b_{1} being Relation of X ex f being Function of X,NAT st

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

for b_{1}, b_{2} being Relation of X st ex f being Function of X,NAT st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

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

ex b

( b

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 b

( b

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

( b

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

b

proof 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 b_{3} being Relation of X holds

( b_{3} = iteration_of O iff ex f being Function of X,NAT st

( b_{3} = 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))) = {} ) ) ) );

for X being set

for O being Operation of X st O is co-well_founded & O is irreflexive & O is finite holds

for b

( b

( b

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 b_{1} being Relation st b_{1} is empty holds

( b_{1} is irreflexive & b_{1} is co-well_founded )

end;
for b

( b

proof end;

registration
end;

registration

let X be set ;

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

coherence

( iteration_of O is antisymmetric & iteration_of O is transitive & iteration_of O is beta-transitive )

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

coherence

( iteration_of O is antisymmetric & iteration_of O is transitive & iteration_of O is beta-transitive )

proof end;

registration
end;

registration

let X be finite set ;

for b_{1} being connected Order of X holds b_{1} is well-ordering
;

end;
cluster reflexive antisymmetric connected transitive total -> connected well-ordering for Order of ;

coherence for b

definition

let X be set ;

let R be connected Order of X;

let S be finite Subset of X;

ex b_{1} being XFinSequence of X st

( rng b_{1} = S & b_{1} is one-to-one & ( for i, j being Nat st i in dom b_{1} & j in dom b_{1} holds

( i <= j iff b_{1} . i,b_{1} . j in R ) ) )

for b_{1}, b_{2} being XFinSequence of X st rng b_{1} = S & b_{1} is one-to-one & ( for i, j being Nat st i in dom b_{1} & j in dom b_{1} holds

( i <= j iff b_{1} . i,b_{1} . j in R ) ) & rng b_{2} = S & b_{2} is one-to-one & ( for i, j being Nat st i in dom b_{2} & j in dom b_{2} holds

( i <= j iff b_{2} . i,b_{2} . j in R ) ) holds

b_{1} = b_{2}

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

ex b

( rng b

( i <= j iff b

proof end;

uniqueness for b

( i <= j iff b

( i <= j iff b

b

proof 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 b_{4} being XFinSequence of X holds

( b_{4} = order (S,R) iff ( rng b_{4} = S & b_{4} is one-to-one & ( for i, j being Nat st i in dom b_{4} & j in dom b_{4} holds

( i <= j iff b_{4} . i,b_{4} . j in R ) ) ) );

for X being set

for R being connected Order of X

for S being finite Subset of X

for b

( b

( i <= j iff b

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

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;

ex b_{1} being Relation of X st

for x, y being Element of X holds

( x,y in b_{1} 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 b_{1}, b_{2} being Relation of X st ( for x, y being Element of X holds

( x,y in b_{1} 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 b_{2} 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

b_{1} = b_{2}

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

ex b

for x, y being Element of X holds

( x,y in b

proof end;

uniqueness for b

( x,y in b

( x,y in b

b

proof 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 b_{4} being Relation of X holds

( b_{4} = value_of (O,R) iff for x, y being Element of X holds

( x,y in b_{4} 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 being finite set

for O being Operation of X

for R being connected Order of X

for b

( b

( x,y in b

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 )

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