:: by Grzegorz Bancerek

::

:: Received October 18, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

theorem Th1: :: EXCHSORT:1

for a, b being Ordinal

for x being set holds

( x in (a +^ b) \ a iff ex c being Ordinal st

( x = a +^ c & c in b ) )

for x being set holds

( x in (a +^ b) \ a iff ex c being Ordinal st

( x = a +^ c & c in b ) )

proof end;

defpred S

defpred S

defpred S

defpred S

defpred S

defpred S

defpred S

defpred S

theorem Th2: :: EXCHSORT:2

for a, b, c, d being Ordinal st a in b & c in d & not ( c <> a & c <> b & d <> a & d <> b ) & not ( c in a & d = a ) & not ( c in a & d = b ) & not ( c = a & d in b ) & not ( c = a & d = b ) & not ( c = a & b in d ) & not ( a in c & d = b ) holds

( c = b & b in d )

( c = b & b in d )

proof end;

theorem :: EXCHSORT:3

theorem Th5: :: EXCHSORT:5

for f being Function

for r being Relation

for x being object holds

( x in f .: r iff ex y, z being object st

( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )

for r being Relation

for x being object holds

( x in f .: r iff ex y, z being object st

( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )

proof end;

theorem Th6: :: EXCHSORT:6

for a, b being Ordinal st a \ b <> {} holds

( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a )

( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a )

proof end;

:: deftheorem Def1 defines segmental EXCHSORT:def 1 :

for f being set holds

( f is segmental iff ex a, b being Ordinal st proj1 f = a \ b );

for f being set holds

( f is segmental iff ex a, b being Ordinal st proj1 f = a \ b );

theorem :: EXCHSORT:8

theorem Th9: :: EXCHSORT:9

for f being Function st f is segmental holds

for a, b, c being Ordinal st a c= b & b c= c & a in dom f & c in dom f holds

b in dom f

for a, b, c being Ordinal st a c= b & b c= c & a in dom f & c in dom f holds

b in dom f

proof end;

registration

coherence

for b_{1} being Function st b_{1} is Sequence-like holds

b_{1} is segmental

for b_{1} being Function st b_{1} is FinSequence-like holds

b_{1} is segmental

end;
for b

b

proof end;

coherence for b

b

proof end;

definition

let a be Ordinal;

let s be set ;

end;
let s be set ;

:: deftheorem defines -based EXCHSORT:def 2 :

for a being Ordinal

for s being set holds

( s is a -based iff for b being Ordinal st b in proj1 s holds

( a in proj1 s & a c= b ) );

for a being Ordinal

for s being set holds

( s is a -based iff for b being Ordinal st b in proj1 s holds

( a in proj1 s & a c= b ) );

:: deftheorem defines -limited EXCHSORT:def 3 :

for a being Ordinal

for s being set holds

( s is a -limited iff a = sup (proj1 s) );

for a being Ordinal

for s being set holds

( s is a -limited iff a = sup (proj1 s) );

theorem :: EXCHSORT:10

for a being Ordinal

for f being Function holds

( ( f is a -based & f is segmental ) iff ex b being Ordinal st

( dom f = b \ a & a c= b ) )

for f being Function holds

( ( f is a -based & f is segmental ) iff ex b being Ordinal st

( dom f = b \ a & a c= b ) )

proof end;

theorem :: EXCHSORT:11

for b being Ordinal

for f being Function holds

( ( f is b -limited & not f is empty & f is segmental ) iff ex a being Ordinal st

( dom f = b \ a & a in b ) )

for f being Function holds

( ( f is b -limited & not f is empty & f is segmental ) iff ex a being Ordinal st

( dom f = b \ a & a in b ) )

proof end;

registration

coherence

for b_{1} being Function st b_{1} is Sequence-like holds

b_{1} is 0 -based
by ORDINAL3:8;

coherence

for b_{1} being Function st b_{1} is FinSequence-like holds

b_{1} is 1 -based

end;
for b

b

coherence

for b

b

proof end;

theorem :: EXCHSORT:14

definition

let f be Function;

( ( ex a being Ordinal st a in dom f implies ex b_{1} being Ordinal st f is b_{1} -based ) & ( ( for a being Ordinal holds not a in dom f ) implies ex b_{1} being Ordinal st b_{1} = 0 ) )

for b_{1}, b_{2} being Ordinal holds

( ( ex a being Ordinal st a in dom f & f is b_{1} -based & f is b_{2} -based implies b_{1} = b_{2} ) & ( ( for a being Ordinal holds not a in dom f ) & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Ordinal holds verum
;

( ( ex a being Ordinal st a in dom f implies ex b_{1} being Ordinal st f is b_{1} -limited ) & ( ( for a being Ordinal holds not a in dom f ) implies ex b_{1} being Ordinal st b_{1} = 0 ) )

for b_{1}, b_{2} being Ordinal holds

( ( ex a being Ordinal st a in dom f & f is b_{1} -limited & f is b_{2} -limited implies b_{1} = b_{2} ) & ( ( for a being Ordinal holds not a in dom f ) & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being Ordinal holds verum
;

end;
func base- f -> Ordinal means :Def4: :: EXCHSORT:def 4

f is it -based if ex a being Ordinal st a in dom f

otherwise it = 0 ;

existence f is it -based if ex a being Ordinal st a in dom f

otherwise it = 0 ;

( ( ex a being Ordinal st a in dom f implies ex b

proof end;

uniqueness for b

( ( ex a being Ordinal st a in dom f & f is b

proof end;

consistency for b

func limit- f -> Ordinal means :Def5: :: EXCHSORT:def 5

f is it -limited if ex a being Ordinal st a in dom f

otherwise it = 0 ;

existence f is it -limited if ex a being Ordinal st a in dom f

otherwise it = 0 ;

( ( ex a being Ordinal st a in dom f implies ex b

proof end;

uniqueness for b

( ( ex a being Ordinal st a in dom f & f is b

consistency

for b

:: deftheorem Def4 defines base- EXCHSORT:def 4 :

for f being Function

for b_{2} being Ordinal holds

( ( ex a being Ordinal st a in dom f implies ( b_{2} = base- f iff f is b_{2} -based ) ) & ( ( for a being Ordinal holds not a in dom f ) implies ( b_{2} = base- f iff b_{2} = 0 ) ) );

for f being Function

for b

( ( ex a being Ordinal st a in dom f implies ( b

:: deftheorem Def5 defines limit- EXCHSORT:def 5 :

for f being Function

for b_{2} being Ordinal holds

( ( ex a being Ordinal st a in dom f implies ( b_{2} = limit- f iff f is b_{2} -limited ) ) & ( ( for a being Ordinal holds not a in dom f ) implies ( b_{2} = limit- f iff b_{2} = 0 ) ) );

for f being Function

for b

( ( ex a being Ordinal st a in dom f implies ( b

:: deftheorem defines len- EXCHSORT:def 6 :

for f being Function holds len- f = (limit- f) -^ (base- f);

for f being Function holds len- f = (limit- f) -^ (base- f);

registration

let a be Ordinal;

let X, Y be set ;

ex b_{1} being Sequence st

( b_{1} is Y -defined & b_{1} is X -valued & b_{1} is a -based & b_{1} is segmental & b_{1} is finite & b_{1} is empty )

end;
let X, Y be set ;

cluster Relation-like Y -defined X -valued Sequence-like Function-like empty finite segmental a -based 0 -based for set ;

existence ex b

( b

proof end;

registration
end;

theorem Th23: :: EXCHSORT:23

for a, b being Ordinal

for A being array st dom A = a \ b & not A is empty holds

( base- A = b & limit- A = a )

for A being array st dom A = a \ b & not A is empty holds

( base- A = b & limit- A = a )

proof end;

registration

let a, b be Ordinal;

let X be set ;

ex b_{1} being array of a,X st

( b_{1} is b -based & b_{1} is natural-valued & b_{1} is INT -valued & b_{1} is real-valued & b_{1} is complex-valued & b_{1} is finite )

end;
let X be set ;

cluster Relation-like a -defined X -valued INT -valued Function-like complex-valued real-valued natural-valued finite segmental b -based for set ;

existence ex b

( b

proof end;

registration

let a be Ordinal;

let x be Nat;

coherence

for b_{1} being array st b_{1} = {[a,x]} holds

b_{1} is natural-valued

end;
let x be Nat;

coherence

for b

b

proof end;

registration

let a be Ordinal;

let x be Real;

coherence

for b_{1} being array st b_{1} = {[a,x]} holds

b_{1} is real-valued

end;
let x be Real;

coherence

for b

b

proof end;

registration

let a be Ordinal;

let X be non empty set ;

let x be Element of X;

coherence

for b_{1} being array st b_{1} = {[a,x]} holds

b_{1} is X -valued

end;
let X be non empty set ;

let x be Element of X;

coherence

for b

b

proof end;

registration

let a be Ordinal;

let x be set ;

coherence

for b_{1} being array st b_{1} = {[a,x]} holds

( b_{1} is a -based & b_{1} is succ a -limited )

end;
let x be set ;

coherence

for b

( b

proof end;

registration

let b be Ordinal;

ex b_{1} being array st

( not b_{1} is empty & b_{1} is b -based & b_{1} is natural-valued & b_{1} is INT -valued & b_{1} is real-valued & b_{1} is complex-valued & b_{1} is finite )

existence

ex b_{1} being array st

( not b_{1} is empty & b_{1} is b -based & b_{1} is finite & b_{1} is X -valued )

end;
cluster Relation-like INT -valued Function-like non empty complex-valued real-valued natural-valued finite segmental b -based for set ;

existence ex b

( not b

proof end;

let X be non empty set ;existence

ex b

( not b

proof end;

:: deftheorem defines descending EXCHSORT:def 8 :

for f being Function holds

( f is descending iff for a, b being Ordinal st a in dom f & b in dom f & a in b holds

f . b c< f . a );

for f being Function holds

( f is descending iff for a, b being Ordinal st a in dom f & b in dom f & a in b holds

f . b c< f . a );

theorem :: EXCHSORT:25

for f being finite array st ( for a being Ordinal st a in dom f & succ a in dom f holds

f . (succ a) c< f . a ) holds

f is descending

f . (succ a) c< f . a ) holds

f is descending

proof end;

theorem Th26: :: EXCHSORT:26

for f being array st len- f = omega & ( for a being Ordinal st a in dom f & succ a in dom f holds

f . (succ a) c< f . a ) holds

f is descending

f . (succ a) c< f . a ) holds

f is descending

proof end;

theorem :: EXCHSORT:28

for f being Sequence st f is descending & f . 0 is finite & ( for a being Ordinal st f . a <> {} holds

succ a in dom f ) holds

last f = {}

succ a in dom f ) holds

last f = {}

proof end;

registration

let X be set ;

let f be X -defined Function;

let a, b be object ;

coherence

Swap (f,a,b) is X -defined

end;
let f be X -defined Function;

let a, b be object ;

coherence

Swap (f,a,b) is X -defined

proof end;

registration

let X be set ;

let f be X -valued Function;

let x, y be object ;

coherence

Swap (f,x,y) is X -valued

end;
let f be X -valued Function;

let x, y be object ;

coherence

Swap (f,x,y) is X -valued

proof end;

theorem Th30: :: EXCHSORT:30

for x, y, X being set

for f being array of X st x in dom f & y in dom f holds

(Swap (f,x,y)) /. x = f /. y

for f being array of X st x in dom f & y in dom f holds

(Swap (f,x,y)) /. x = f /. y

proof end;

theorem Th32: :: EXCHSORT:32

for x, y, X being set

for f being array of X st x in dom f & y in dom f holds

(Swap (f,x,y)) /. y = f /. x

for f being array of X st x in dom f & y in dom f holds

(Swap (f,x,y)) /. y = f /. x

proof end;

theorem Th34: :: EXCHSORT:34

for x, y, z, X being set

for f being array of X st z in dom f & z <> x & z <> y holds

(Swap (f,x,y)) /. z = f /. z

for f being array of X st z in dom f & z <> x & z <> y holds

(Swap (f,x,y)) /. z = f /. z

proof end;

theorem :: EXCHSORT:35

for x, y being set

for f being Function st x in dom f & y in dom f holds

Swap (f,x,y) = Swap (f,y,x)

for f being Function st x in dom f & y in dom f holds

Swap (f,x,y) = Swap (f,y,x)

proof end;

registration

let X be non empty set ;

existence

ex b_{1} being X -valued non empty Function st b_{1} is onto

end;
existence

ex b

proof end;

registration

let X be non empty set ;

let f be X -valued non empty onto Function;

let x, y be Element of dom f;

coherence

Swap (f,x,y) is onto

end;
let f be X -valued non empty onto Function;

let x, y be Element of dom f;

coherence

Swap (f,x,y) is onto

proof end;

registration

let A be real-valued array;

let x, y be set ;

coherence

for b_{1} being array st b_{1} = Swap (A,x,y) holds

b_{1} is real-valued

end;
let x, y be set ;

coherence

for b

b

proof end;

definition

let A be array;

ex b_{1} being array ex f being Permutation of (dom A) st b_{1} = A * f

end;
mode permutation of A -> array means :Def9: :: EXCHSORT:def 9

ex f being Permutation of (dom A) st it = A * f;

existence ex f being Permutation of (dom A) st it = A * f;

ex b

proof end;

:: deftheorem Def9 defines permutation EXCHSORT:def 9 :

for A, b_{2} being array holds

( b_{2} is permutation of A iff ex f being Permutation of (dom A) st b_{2} = A * f );

for A, b

( b

theorem Th40: :: EXCHSORT:40

for A, B, C being array st A is permutation of B & B is permutation of C holds

A is permutation of C

A is permutation of C

proof end;

registration

let X be non empty set ;

let x, y be Element of X;

coherence

( Swap ((id X),x,y) is one-to-one & Swap ((id X),x,y) is X -valued & Swap ((id X),x,y) is X -defined ) by Th41;

end;
let x, y be Element of X;

coherence

( Swap ((id X),x,y) is one-to-one & Swap ((id X),x,y) is X -valued & Swap ((id X),x,y) is X -defined ) by Th41;

registration

let X be non empty set ;

let x, y be Element of X;

coherence

( Swap ((id X),x,y) is onto & Swap ((id X),x,y) is total )

end;
let x, y be Element of X;

coherence

( Swap ((id X),x,y) is onto & Swap ((id X),x,y) is total )

proof end;

definition

let X, Y be non empty set ;

let f be Function of X,Y;

let x, y be Element of X;

:: original: Swap

redefine func Swap (f,x,y) -> Function of X,Y;

coherence

Swap (f,x,y) is Function of X,Y

end;
let f be Function of X,Y;

let x, y be Element of X;

:: original: Swap

redefine func Swap (f,x,y) -> Function of X,Y;

coherence

Swap (f,x,y) is Function of X,Y

proof end;

theorem Th42: :: EXCHSORT:42

for x, y, X being set

for f being Function

for A being array st x in X & y in X & f = Swap ((id X),x,y) & X = dom A holds

Swap (A,x,y) = A * f

for f being Function

for A being array st x in X & y in X & f = Swap ((id X),x,y) & X = dom A holds

Swap (A,x,y) = A * f

proof end;

theorem Th43: :: EXCHSORT:43

for x, y being set

for A being array st x in dom A & y in dom A holds

( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) )

for A being array st x in dom A & y in dom A holds

( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) )

proof end;

theorem :: EXCHSORT:44

for x, y being set

for A, B being array st x in dom A & y in dom A & A is permutation of B holds

( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) )

for A, B being array st x in dom A & y in dom A & A is permutation of B holds

( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) )

proof end;

definition

let O be RelStr ;

let A be array of O;

{ [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b ) } is set ;

end;
let A be array of O;

attr A is ascending means :: EXCHSORT:def 10

for a, b being Ordinal st a in dom A & b in dom A & a in b holds

A /. a <= A /. b;

for a, b being Ordinal st a in dom A & b in dom A & a in b holds

A /. a <= A /. b;

func inversions A -> set equals :: EXCHSORT:def 11

{ [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b ) } ;

coherence { [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b ) } ;

{ [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b ) } is set ;

:: deftheorem defines ascending EXCHSORT:def 10 :

for O being RelStr

for A being array of O holds

( A is ascending iff for a, b being Ordinal st a in dom A & b in dom A & a in b holds

A /. a <= A /. b );

for O being RelStr

for A being array of O holds

( A is ascending iff for a, b being Ordinal st a in dom A & b in dom A & a in b holds

A /. a <= A /. b );

:: deftheorem defines inversions EXCHSORT:def 11 :

for O being RelStr

for A being array of O holds inversions A = { [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b ) } ;

for O being RelStr

for A being array of O holds inversions A = { [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b ) } ;

registration

let O be RelStr ;

for b_{1} being empty array of O holds b_{1} is ascending
;

let A be empty array of O;

coherence

inversions A is empty

end;
cluster Relation-like the carrier of O -valued Function-like empty segmental -> empty ascending for set ;

coherence for b

let A be empty array of O;

coherence

inversions A is empty

proof end;

definition

let O be non empty connected Poset;

let R be array of O;

for b_{1} being set holds

( b_{1} = inversions R iff b_{1} = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } )

end;
let R be array of O;

redefine func inversions R equals :: EXCHSORT:def 12

{ [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ;

compatibility { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ;

for b

( b

proof end;

:: deftheorem defines inversions EXCHSORT:def 12 :

for O being non empty connected Poset

for R being array of O holds inversions R = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ;

for O being non empty connected Poset

for R being array of O holds inversions R = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ;

theorem Th46: :: EXCHSORT:46

for O being non empty connected Poset

for R being array of O

for x being object

for y being set holds

( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )

for R being array of O

for x being object

for y being set holds

( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )

proof end;

theorem Th47: :: EXCHSORT:47

for O being non empty connected Poset

for R being array of O holds inversions R c= [:(dom R),(dom R):]

for R being array of O holds inversions R c= [:(dom R),(dom R):]

proof end;

registration

let O be non empty connected Poset;

let R be finite array of O;

coherence

inversions R is finite

end;
let R be finite array of O;

coherence

inversions R is finite

proof end;

theorem Th48: :: EXCHSORT:48

for O being non empty connected Poset

for R being array of O holds

( R is ascending iff inversions R = {} )

for R being array of O holds

( R is ascending iff inversions R = {} )

proof end;

theorem Th49: :: EXCHSORT:49

for x, y being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

[y,x] nin inversions R

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

[y,x] nin inversions R

proof end;

theorem Th50: :: EXCHSORT:50

for x, y, z being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & [y,z] in inversions R holds

[x,z] in inversions R

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & [y,z] in inversions R holds

[x,z] in inversions R

proof end;

registration

let O be non empty connected Poset;

let R be array of O;

coherence

inversions R is Relation-like

end;
let R be array of O;

coherence

inversions R is Relation-like

proof end;

registration

let O be non empty connected Poset;

let R be array of O;

coherence

for b_{1} being Relation st b_{1} = inversions R holds

( b_{1} is asymmetric & b_{1} is transitive )

end;
let R be array of O;

coherence

for b

( b

proof end;

definition

let O be non empty connected Poset;

let a, b be Element of O;

:: original: <

redefine pred a < b;

asymmetry

for a, b being Element of O st R72(O,b_{1},b_{2}) holds

not R72(O,b_{2},b_{1})
by ORDERS_2:5;

end;
let a, b be Element of O;

:: original: <

redefine pred a < b;

asymmetry

for a, b being Element of O st R72(O,b

not R72(O,b

theorem Th51: :: EXCHSORT:51

for x, y being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

[x,y] nin inversions (Swap (R,x,y))

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

[x,y] nin inversions (Swap (R,x,y))

proof end;

theorem Th52: :: EXCHSORT:52

for x, y, z, t being set

for O being non empty connected Poset

for R being array of O st x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y holds

( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) )

for O being non empty connected Poset

for R being array of O st x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y holds

( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) )

proof end;

theorem Th53: :: EXCHSORT:53

for x, y, z being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )

proof end;

theorem Th54: :: EXCHSORT:54

for x, y, z being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) )

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) )

proof end;

theorem Th55: :: EXCHSORT:55

for x, y, z being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & z in y & [x,z] in inversions (Swap (R,x,y)) holds

[x,z] in inversions R

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & z in y & [x,z] in inversions (Swap (R,x,y)) holds

[x,z] in inversions R

proof end;

theorem Th56: :: EXCHSORT:56

for x, y, z being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) holds

[z,y] in inversions R

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) holds

[z,y] in inversions R

proof end;

theorem Th57: :: EXCHSORT:57

for x, y, z being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & y in z & [x,z] in inversions (Swap (R,x,y)) holds

[y,z] in inversions R

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & y in z & [x,z] in inversions (Swap (R,x,y)) holds

[y,z] in inversions R

proof end;

theorem Th58: :: EXCHSORT:58

for x, y, z being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

( ( y in z & [x,z] in inversions R ) iff [y,z] in inversions (Swap (R,x,y)) )

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

( ( y in z & [x,z] in inversions R ) iff [y,z] in inversions (Swap (R,x,y)) )

proof end;

definition

let O be non empty connected Poset;

let R be array of O;

let x, y be set ;

[:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:])) is Function ;

end;
let R be array of O;

let x, y be set ;

func (R,x,y) incl -> Function equals :: EXCHSORT:def 13

[:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]));

coherence [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]));

[:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:])) is Function ;

:: deftheorem defines incl EXCHSORT:def 13 :

for O being non empty connected Poset

for R being array of O

for x, y being set holds (R,x,y) incl = [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]));

for O being non empty connected Poset

for R being array of O

for x, y being set holds (R,x,y) incl = [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]));

theorem Th60: :: EXCHSORT:60

for O being non empty connected Poset

for T being non empty array of O

for p, q being Element of dom T holds (succ q) \ p c= dom T

for T being non empty array of O

for p, q being Element of dom T holds (succ q) \ p c= dom T

proof end;

theorem Th61: :: EXCHSORT:61

for O being non empty connected Poset

for T being non empty array of O

for p, q being Element of dom T holds

( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] )

for T being non empty array of O

for p, q being Element of dom T holds

( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] )

proof end;

theorem Th62: :: EXCHSORT:62

for O being non empty connected Poset

for T being non empty array of O

for p, q, r being Element of dom T st p c= r & r c= q holds

( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )

for T being non empty array of O

for p, q, r being Element of dom T st p c= r & r c= q holds

( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )

proof end;

theorem Th63: :: EXCHSORT:63

for f being Function

for O being non empty connected Poset

for T being non empty array of O

for p, q, r, s being Element of dom T st r <> p & s <> q & f = Swap ((id (dom T)),p,q) holds

((T,p,q) incl) . (r,s) = [(f . r),(f . s)]

for O being non empty connected Poset

for T being non empty array of O

for p, q, r, s being Element of dom T st r <> p & s <> q & f = Swap ((id (dom T)),p,q) holds

((T,p,q) incl) . (r,s) = [(f . r),(f . s)]

proof end;

theorem Th64: :: EXCHSORT:64

for f being Function

for O being non empty connected Poset

for T being non empty array of O

for p, q, r being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds

( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )

for O being non empty connected Poset

for T being non empty array of O

for p, q, r being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds

( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )

proof end;

theorem Th65: :: EXCHSORT:65

for f being Function

for O being non empty connected Poset

for T being non empty array of O

for p, q, r being Element of dom T st q in r & f = Swap ((id (dom T)),p,q) holds

( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )

for O being non empty connected Poset

for T being non empty array of O

for p, q, r being Element of dom T st q in r & f = Swap ((id (dom T)),p,q) holds

( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )

proof end;

theorem Th66: :: EXCHSORT:66

for O being non empty connected Poset

for T being non empty array of O

for p, q being Element of dom T st p in q holds

((T,p,q) incl) . (p,q) = [p,q]

for T being non empty array of O

for p, q being Element of dom T st p in q holds

((T,p,q) incl) . (p,q) = [p,q]

proof end;

theorem Th67: :: EXCHSORT:67

for O being non empty connected Poset

for T being non empty array of O

for p, q, r, s being Element of dom T st p in q & r <> p & r <> q & s <> p & s <> q holds

((T,p,q) incl) . (r,s) = [r,s]

for T being non empty array of O

for p, q, r, s being Element of dom T st p in q & r <> p & r <> q & s <> p & s <> q holds

((T,p,q) incl) . (r,s) = [r,s]

proof end;

theorem Th68: :: EXCHSORT:68

for O being non empty connected Poset

for T being non empty array of O

for p, q, r being Element of dom T st r in p & p in q holds

( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] )

for T being non empty array of O

for p, q, r being Element of dom T st r in p & p in q holds

( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] )

proof end;

theorem Th69: :: EXCHSORT:69

for O being non empty connected Poset

for T being non empty array of O

for p, q, s being Element of dom T st p in s & s in q holds

( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] )

for T being non empty array of O

for p, q, s being Element of dom T st p in s & s in q holds

( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] )

proof end;

theorem Th70: :: EXCHSORT:70

for O being non empty connected Poset

for T being non empty array of O

for p, q, s being Element of dom T st p in q & q in s holds

( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] )

for T being non empty array of O

for p, q, s being Element of dom T st p in q & q in s holds

( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] )

proof end;

Lm1: for f being Function

for O being non empty connected Poset

for T being non empty array of O

for p, q being Element of dom T st p in q & f = (T,p,q) incl holds

for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds

( x1 = x2 & y1 = y2 )

proof end;

theorem Th71: :: EXCHSORT:71

for O being non empty connected Poset

for T being non empty array of O

for p, q being Element of dom T st p in q holds

((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one

for T being non empty array of O

for p, q being Element of dom T st p in q holds

((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one

proof end;

registration

let O be non empty connected Poset;

let R be array of O;

let x, y, z be set ;

coherence

((R,x,y) incl) .: z is Relation-like

end;
let R be array of O;

let x, y, z be set ;

coherence

((R,x,y) incl) .: z is Relation-like

proof end;

theorem Th72: :: EXCHSORT:72

for x, y being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R holds

((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R

proof end;

registration
end;

theorem Th73: :: EXCHSORT:73

for x, y being set

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & inversions R is finite holds

card (inversions (Swap (R,x,y))) in card (inversions R)

for O being non empty connected Poset

for R being array of O st [x,y] in inversions R & inversions R is finite holds

card (inversions (Swap (R,x,y))) in card (inversions R)

proof end;

theorem :: EXCHSORT:74

for x, y being set

for O being non empty connected Poset

for R being finite array of O st [x,y] in inversions R holds

card (inversions (Swap (R,x,y))) < card (inversions R)

for O being non empty connected Poset

for R being finite array of O st [x,y] in inversions R holds

card (inversions (Swap (R,x,y))) < card (inversions R)

proof end;

definition

let O be non empty connected Poset;

let R be array of O;

ex b_{1} being non empty array st

( b_{1} . (base- b_{1}) = R & ( for a being Ordinal st a in dom b_{1} holds

b_{1} . a is array of O ) & ( for a being Ordinal st a in dom b_{1} & succ a in dom b_{1} holds

ex R being array of O ex x, y being set st

( [x,y] in inversions R & b_{1} . a = R & b_{1} . (succ a) = Swap (R,x,y) ) ) )

end;
let R be array of O;

mode arr_computation of R -> non empty array means :Def14: :: EXCHSORT:def 14

( it . (base- it) = R & ( for a being Ordinal st a in dom it holds

it . a is array of O ) & ( for a being Ordinal st a in dom it & succ a in dom it holds

ex R being array of O ex x, y being set st

( [x,y] in inversions R & it . a = R & it . (succ a) = Swap (R,x,y) ) ) );

existence ( it . (base- it) = R & ( for a being Ordinal st a in dom it holds

it . a is array of O ) & ( for a being Ordinal st a in dom it & succ a in dom it holds

ex R being array of O ex x, y being set st

( [x,y] in inversions R & it . a = R & it . (succ a) = Swap (R,x,y) ) ) );

ex b

( b

b

ex R being array of O ex x, y being set st

( [x,y] in inversions R & b

proof end;

:: deftheorem Def14 defines arr_computation EXCHSORT:def 14 :

for O being non empty connected Poset

for R being array of O

for b_{3} being non empty array holds

( b_{3} is arr_computation of R iff ( b_{3} . (base- b_{3}) = R & ( for a being Ordinal st a in dom b_{3} holds

b_{3} . a is array of O ) & ( for a being Ordinal st a in dom b_{3} & succ a in dom b_{3} holds

ex R being array of O ex x, y being set st

( [x,y] in inversions R & b_{3} . a = R & b_{3} . (succ a) = Swap (R,x,y) ) ) ) );

for O being non empty connected Poset

for R being array of O

for b

( b

b

ex R being array of O ex x, y being set st

( [x,y] in inversions R & b

theorem Th75: :: EXCHSORT:75

for a being Ordinal

for O being non empty connected Poset

for R being array of O holds {[a,R]} is arr_computation of R

for O being non empty connected Poset

for R being array of O holds {[a,R]} is arr_computation of R

proof end;

registration

let O be non empty connected Poset;

let R be array of O;

let a be Ordinal;

existence

ex b_{1} being arr_computation of R st

( b_{1} is a -based & b_{1} is finite )

end;
let R be array of O;

let a be Ordinal;

existence

ex b

( b

proof end;

registration

let O be non empty connected Poset;

let R be array of O;

let C be arr_computation of R;

let x be set ;

coherence

( C . x is segmental & C . x is Function-like & C . x is Relation-like )

end;
let R be array of O;

let C be arr_computation of R;

let x be set ;

coherence

( C . x is segmental & C . x is Function-like & C . x is Relation-like )

proof end;

registration

let O be non empty connected Poset;

let R be array of O;

let C be arr_computation of R;

let x be set ;

coherence

C . x is the carrier of O -valued

end;
let R be array of O;

let C be arr_computation of R;

let x be set ;

coherence

C . x is the carrier of O -valued

proof end;

registration

let O be non empty connected Poset;

let R be array of O;

let C be arr_computation of R;

coherence

( last C is segmental & last C is Relation-like & last C is Function-like ) ;

end;
let R be array of O;

let C be arr_computation of R;

coherence

( last C is segmental & last C is Relation-like & last C is Function-like ) ;

registration

let O be non empty connected Poset;

let R be array of O;

let C be arr_computation of R;

coherence

last C is the carrier of O -valued ;

end;
let R be array of O;

let C be arr_computation of R;

coherence

last C is the carrier of O -valued ;

definition
end;

:: deftheorem defines complete EXCHSORT:def 15 :

for O being non empty connected Poset

for R being array of O

for C being arr_computation of R holds

( C is complete iff last C is ascending );

for O being non empty connected Poset

for R being array of O

for C being arr_computation of R holds

( C is complete iff last C is ascending );

theorem Th76: :: EXCHSORT:76

for O being non empty connected Poset

for R being array of O

for C being 0 -based arr_computation of R st R is finite array of O holds

C is finite

for R being array of O

for C being 0 -based arr_computation of R st R is finite array of O holds

C is finite

proof end;

theorem :: EXCHSORT:77

for O being non empty connected Poset

for R being array of O

for C being 0 -based arr_computation of R st R is finite array of O & ( for a being Ordinal st inversions (C . a) <> {} holds

succ a in dom C ) holds

C is complete

for R being array of O

for C being 0 -based arr_computation of R st R is finite array of O & ( for a being Ordinal st inversions (C . a) <> {} holds

succ a in dom C ) holds

C is complete

proof end;

theorem Th78: :: EXCHSORT:78

for O being non empty connected Poset

for R being array of O

for C being finite arr_computation of R holds

( last C is permutation of R & ( for a being Ordinal st a in dom C holds

C . a is permutation of R ) )

for R being array of O

for C being finite arr_computation of R holds

( last C is permutation of R & ( for a being Ordinal st a in dom C holds

C . a is permutation of R ) )

proof end;

registration

let X be set ;

coherence

for b_{1} being Element of X ^omega holds b_{1} is X -valued
by AFINSQ_1:42;

end;
coherence

for b

scheme :: EXCHSORT:sch 2

A{ F_{1}( set ) -> set , F_{2}() -> non empty set , P_{1}[ set , set ], F_{3}() -> set } :

A{ F

ex f being non empty finite 0 -based array ex k being Element of F_{2}() st

( k = last f & F_{1}(k) = {} & f . 0 = F_{3}() & ( for a being Ordinal st succ a in dom f holds

ex x, y being Element of F_{2}() st

( x = f . a & y = f . (succ a) & P_{1}[x,y] ) ) )

provided( k = last f & F

ex x, y being Element of F

( x = f . a & y = f . (succ a) & P

A1:
F_{3}() in F_{2}()
and

A2: F_{1}(F_{3}()) is finite
and

A3: for x being Element of F_{2}() st F_{1}(x) <> {} holds

ex y being Element of F_{2}() st

( P_{1}[x,y] & F_{1}(y) c< F_{1}(x) )

A2: F

A3: for x being Element of F

ex y being Element of F

( P

proof end;

registration

let A be real-valued array;

coherence

for b_{1} being permutation of A holds b_{1} is real-valued

end;
coherence

for b

proof end;

registration

let a be Ordinal;

let X be non empty set ;

coherence

for b_{1} being Element of Funcs (a,X) holds b_{1} is Sequence-like
by FUNCT_2:92;

end;
let X be non empty set ;

coherence

for b

registration

let X be set ;

let Y be real-membered non empty set ;

coherence

for b_{1} being Element of Funcs (X,Y) holds b_{1} is real-valued
;

end;
let Y be real-membered non empty set ;

coherence

for b

registration

let X be set ;

let A be array of X;

coherence

for b_{1} being permutation of A holds b_{1} is X -valued

end;
let A be array of X;

coherence

for b

proof end;

registration

let X, Z be set ;

let Y be Subset of Z;

coherence

for b_{1} being Element of Funcs (X,Y) holds b_{1} is Z -valued

end;
let Y be Subset of Z;

coherence

for b

proof end;

theorem Th84: :: EXCHSORT:84

for a being finite Ordinal

for x being set holds

( not x in a or x = 0 or ex b being Ordinal st x = succ b )

for x being set holds

( not x in a or x = 0 or ex b being Ordinal st x = succ b )

proof end;

theorem Th85: :: EXCHSORT:85

for O being non empty connected Poset

for A being non empty finite 0 -based array of O ex C being 0 -based arr_computation of A st C is complete

for A being non empty finite 0 -based array of O ex C being 0 -based arr_computation of A st C is complete

proof end;

theorem Th86: :: EXCHSORT:86

for O being non empty connected Poset

for A being non empty finite 0 -based array of O ex B being permutation of A st B is ascending

for A being non empty finite 0 -based array of O ex B being permutation of A st B is ascending

proof end;

registration

let O be non empty connected Poset;

let A be finite 0 -based array of O;

ex b_{1} being permutation of A st b_{1} is ascending

end;
let A be finite 0 -based array of O;

cluster Relation-like the carrier of O -valued Function-like segmental ascending for permutation of A;

existence ex b

proof end;