:: Sorting by Exchanging
:: by Grzegorz Bancerek
::
:: Received October 18, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users


begin

theorem OM1: :: EXCHSORT:1
for a, b being ordinal number
for x being set holds
( x in (a +^ b) \ a iff ex c being ordinal number st
( x = a +^ c & c in b ) )
proof end;

defpred S1[ set , set , set , set ] means ( $3 <> $1 & $3 <> $2 & $4 <> $1 & $4 <> $2 );

defpred S2[ set , set , set , set ] means ( $3 in $1 & $4 = $1 );

defpred S3[ set , set , set , set ] means ( $3 in $1 & $4 = $2 );

defpred S4[ set , set , set , set ] means ( $3 = $1 & $4 in $2 );

defpred S5[ set , set , set , set ] means ( $3 = $1 & $4 = $2 );

defpred S6[ set , set , set , set ] means ( $3 = $1 & $2 in $4 );

defpred S7[ set , set , set , set ] means ( $1 in $3 & $4 = $2 );

defpred S8[ set , set , set , set ] means ( $3 = $2 & $2 in $4 );

theorem Eight: :: EXCHSORT:2
for a, b, c, d being ordinal number 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 )
proof end;

theorem :: EXCHSORT:3
for x, y being set st x nin y holds
(y \/ {x}) \ y = {x} by XBOOLE_1:88, ZFMISC_1:56;

theorem Lem2: :: EXCHSORT:4
for x being set holds (succ x) \ x = {x}
proof end;

theorem Lem3: :: EXCHSORT:5
for f being Function
for r being Relation
for x being set holds
( x in f .: r iff ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
proof end;

theorem Th008: :: EXCHSORT:6
for a, b being ordinal number st a \ b <> {} holds
( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a )
proof end;

theorem Th009: :: EXCHSORT:7
for a, b being ordinal number st not a \ b is empty & a \ b is finite holds
ex n being Nat st a = b +^ n
proof end;

begin

definition
let f be set ;
attr f is segmental means :SEG: :: EXCHSORT:def 1
ex a, b being ordinal number st proj1 f = a \ b;
end;

:: deftheorem SEG defines segmental EXCHSORT:def 1 :
for f being set holds
( f is segmental iff ex a, b being ordinal number st proj1 f = a \ b );

theorem :: EXCHSORT:8
for f, g being Function st dom f = dom g & f is segmental holds
g is segmental
proof end;

theorem OM2: :: EXCHSORT:9
for f being Function st f is segmental holds
for a, b, c being ordinal number st a c= b & b c= c & a in dom f & c in dom f holds
b in dom f
proof end;

registration
cluster T-Sequence-like Relation-like Function-like -> segmental set ;
coherence
for b1 being Function st b1 is T-Sequence-like holds
b1 is segmental
proof end;
cluster Relation-like Function-like FinSequence-like -> segmental set ;
coherence
for b1 being Function st b1 is FinSequence-like holds
b1 is segmental
proof end;
end;

definition
let a be ordinal number ;
let s be set ;
attr s is a -based means :AB: :: EXCHSORT:def 2
for b being ordinal number st b in proj1 s holds
( a in proj1 s & a c= b );
attr s is a -limited means :LI: :: EXCHSORT:def 3
a = sup (proj1 s);
end;

:: deftheorem AB defines -based EXCHSORT:def 2 :
for a being ordinal number
for s being set holds
( s is a -based iff for b being ordinal number st b in proj1 s holds
( a in proj1 s & a c= b ) );

:: deftheorem LI defines -limited EXCHSORT:def 3 :
for a being ordinal number
for s being set holds
( s is a -limited iff a = sup (proj1 s) );

theorem :: EXCHSORT:10
for a being ordinal number
for f being Function holds
( ( f is a -based & f is segmental ) iff ex b being ordinal number st
( dom f = b \ a & a c= b ) )
proof end;

theorem :: EXCHSORT:11
for b being ordinal number
for f being Function holds
( ( f is b -limited & not f is empty & f is segmental ) iff ex a being ordinal number st
( dom f = b \ a & a in b ) )
proof end;

registration
cluster T-Sequence-like Relation-like Function-like -> 0 -based set ;
coherence
for b1 being Function st b1 is T-Sequence-like holds
b1 is 0 -based
proof end;
cluster Relation-like Function-like FinSequence-like -> 1 -based set ;
coherence
for b1 being Function st b1 is FinSequence-like holds
b1 is 1 -based
proof end;
end;

theorem Th003: :: EXCHSORT:12
for f being Function holds f is inf (dom f) -based
proof end;

theorem :: EXCHSORT:13
for f being Function holds f is sup (dom f) -limited by LI;

theorem :: EXCHSORT:14
for b, a being ordinal number
for f being Function st f is b -limited & a in dom f holds
a in b
proof end;

definition
let f be Function;
func base- f -> ordinal number means :BA: :: EXCHSORT:def 4
f is it -based if ex a being ordinal number st a in dom f
otherwise it = 0 ;
existence
( ( ex a being ordinal number st a in dom f implies ex b1 being ordinal number st f is b1 -based ) & ( ( for a being ordinal number holds not a in dom f ) implies ex b1 being ordinal number st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being ordinal number holds
( ( ex a being ordinal number st a in dom f & f is b1 -based & f is b2 -based implies b1 = b2 ) & ( ( for a being ordinal number holds not a in dom f ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being ordinal number holds verum
;
func limit- f -> ordinal number means :LIM: :: EXCHSORT:def 5
f is it -limited if ex a being ordinal number st a in dom f
otherwise it = 0 ;
existence
( ( ex a being ordinal number st a in dom f implies ex b1 being ordinal number st f is b1 -limited ) & ( ( for a being ordinal number holds not a in dom f ) implies ex b1 being ordinal number st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being ordinal number holds
( ( ex a being ordinal number st a in dom f & f is b1 -limited & f is b2 -limited implies b1 = b2 ) & ( ( for a being ordinal number holds not a in dom f ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being ordinal number holds verum
;
end;

:: deftheorem BA defines base- EXCHSORT:def 4 :
for f being Function
for b2 being ordinal number holds
( ( ex a being ordinal number st a in dom f implies ( b2 = base- f iff f is b2 -based ) ) & ( ( for a being ordinal number holds not a in dom f ) implies ( b2 = base- f iff b2 = 0 ) ) );

:: deftheorem LIM defines limit- EXCHSORT:def 5 :
for f being Function
for b2 being ordinal number holds
( ( ex a being ordinal number st a in dom f implies ( b2 = limit- f iff f is b2 -limited ) ) & ( ( for a being ordinal number holds not a in dom f ) implies ( b2 = limit- f iff b2 = 0 ) ) );

definition
let f be Function;
func len- f -> ordinal number equals :: EXCHSORT:def 6
(limit- f) -^ (base- f);
coherence
(limit- f) -^ (base- f) is ordinal number
;
end;

:: deftheorem defines len- EXCHSORT:def 6 :
for f being Function holds len- f = (limit- f) -^ (base- f);

theorem EE: :: EXCHSORT:15
( base- {} = 0 & limit- {} = 0 & len- {} = 0 )
proof end;

theorem Th005: :: EXCHSORT:16
for f being Function holds limit- f = sup (dom f)
proof end;

theorem :: EXCHSORT:17
for f being Function holds f is limit- f -limited
proof end;

theorem Th002: :: EXCHSORT:18
for a being ordinal number
for A being empty set holds A is a -based
proof end;

registration
let a be ordinal number ;
let X, Y be set ;
cluster empty T-Sequence-like Relation-like Y -defined X -valued Function-like finite segmental a -based 0 -based set ;
existence
ex b1 being T-Sequence st
( b1 is Y -defined & b1 is X -valued & b1 is a -based & b1 is segmental & b1 is finite & b1 is empty )
proof end;
end;

definition
mode array is segmental Function;
end;

registration
let A be array;
cluster proj1 A -> ordinal-membered ;
coherence
dom A is ordinal-membered
proof end;
end;

theorem :: EXCHSORT:19
for f being array holds
( f is 0 -limited iff f is empty )
proof end;

registration
cluster Relation-like Function-like segmental 0 -based -> T-Sequence-like set ;
coherence
for b1 being array st b1 is 0 -based holds
b1 is T-Sequence-like
proof end;
end;

definition
let X be set ;
mode array of X is X -valued array;
end;

definition
let X be 1-sorted ;
mode array of X is array of the carrier of X;
end;

definition
let a be ordinal number ;
let X be set ;
mode array of a,X is a -defined array of X;
end;

theorem Th007: :: EXCHSORT:20
for f being Function holds base- f = inf (dom f)
proof end;

theorem :: EXCHSORT:21
for f being Function holds f is base- f -based
proof end;

theorem :: EXCHSORT:22
for A being array holds dom A = (limit- A) \ (base- A)
proof end;

theorem Th011: :: EXCHSORT:23
for a, b being ordinal number
for A being array st dom A = a \ b & not A is empty holds
( base- A = b & limit- A = a )
proof end;

theorem TT0: :: EXCHSORT:24
for f being T-Sequence holds
( base- f = 0 & limit- f = dom f & len- f = dom f )
proof end;

registration
let a, b be ordinal number ;
let X be set ;
cluster Relation-like a -defined X -valued Function-like complex-valued real-valued integer-valued natural-valued finite segmental b -based set ;
existence
ex b1 being array of a,X st
( b1 is b -based & b1 is natural-valued & b1 is integer-valued & b1 is real-valued & b1 is complex-valued & b1 is finite )
proof end;
end;

registration
let a be ordinal number ;
let x be set ;
cluster {[a,x]} -> segmental ;
coherence
{[a,x]} is segmental
proof end;
end;

registration
let a be ordinal number ;
let x be natural number ;
cluster {[a,x]} -> natural-valued array;
coherence
for b1 being array st b1 = {[a,x]} holds
b1 is natural-valued
proof end;
end;

registration
let a be ordinal number ;
let x be real number ;
cluster {[a,x]} -> real-valued array;
coherence
for b1 being array st b1 = {[a,x]} holds
b1 is real-valued
proof end;
end;

registration
let a be ordinal number ;
let X be non empty set ;
let x be Element of X;
cluster {[a,x]} -> X -valued array;
coherence
for b1 being array st b1 = {[a,x]} holds
b1 is X -valued
proof end;
end;

registration
let a be ordinal number ;
let x be set ;
cluster {[a,x]} -> a -based succ a -limited array;
coherence
for b1 being array st b1 = {[a,x]} holds
( b1 is a -based & b1 is succ a -limited )
proof end;
end;

registration
let b be ordinal number ;
cluster non empty Relation-like Function-like complex-valued real-valued integer-valued natural-valued finite segmental b -based set ;
existence
ex b1 being array st
( not b1 is empty & b1 is b -based & b1 is natural-valued & b1 is integer-valued & b1 is real-valued & b1 is complex-valued & b1 is finite )
proof end;
let X be non empty set ;
cluster non empty Relation-like X -valued Function-like finite segmental b -based set ;
existence
ex b1 being array st
( not b1 is empty & b1 is b -based & b1 is finite & b1 is X -valued )
proof end;
end;

notation
let s be T-Sequence;
synonym s last for last s;
end;

definition
let A be array;
func last A -> set equals :: EXCHSORT:def 7
A . (union (dom A));
coherence
A . (union (dom A)) is set
;
end;

:: deftheorem defines last EXCHSORT:def 7 :
for A being array holds last A = A . (union (dom A));

registration
let A be T-Sequence;
identify A last with last A;
compatibility
A last = last A
;
end;

begin

definition
let f be Function;
attr f is descending means :DSC: :: EXCHSORT:def 8
for a, b being ordinal number st a in dom f & b in dom f & a in b holds
f . b c< f . a;
end;

:: deftheorem DSC defines descending EXCHSORT:def 8 :
for f being Function holds
( f is descending iff for a, b being ordinal number 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 number st a in dom f & succ a in dom f holds
f . (succ a) c< f . a ) holds
f is descending
proof end;

theorem DSC2: :: EXCHSORT:26
for f being array st len- f = omega & ( for a being ordinal number st a in dom f & succ a in dom f holds
f . (succ a) c< f . a ) holds
f is descending
proof end;

theorem TD1: :: EXCHSORT:27
for f being T-Sequence st f is descending & f . 0 is finite holds
f is finite
proof end;

theorem :: EXCHSORT:28
for f being T-Sequence st f is descending & f . 0 is finite & ( for a being ordinal number st f . a <> {} holds
succ a in dom f ) holds
last f = {}
proof end;

scheme :: EXCHSORT:sch 1
A{ F1() -> T-Sequence, F2( set ) -> set } :
F1() is finite
provided
C1: F2((F1() . 0)) is finite and
C2: for a being ordinal number st succ a in dom F1() & F2((F1() . a)) is finite holds
F2((F1() . (succ a))) c< F2((F1() . a))
proof end;

begin

registration
let X be set ;
let f be X -defined Function;
let a, b be set ;
cluster Swap (f,a,b) -> X -defined ;
coherence
Swap (f,a,b) is X -defined
proof end;
end;

registration
let X be set ;
let f be X -valued Function;
let x, y be set ;
cluster Swap (f,x,y) -> X -valued ;
coherence
Swap (f,x,y) is X -valued
proof end;
end;

theorem TSa: :: EXCHSORT:29
for x, y being set
for f being Function st x in dom f & y in dom f holds
(Swap (f,x,y)) . x = f . y
proof end;

theorem TSa2: :: EXCHSORT:30
for X, x, y 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
proof end;

theorem TSb: :: EXCHSORT:31
for x, y being set
for f being Function st x in dom f & y in dom f holds
(Swap (f,x,y)) . y = f . x
proof end;

theorem TSb2: :: EXCHSORT:32
for X, x, y 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
proof end;

theorem TSc: :: EXCHSORT:33
for z, x, y being set
for f being Function st z <> x & z <> y holds
(Swap (f,x,y)) . z = f . z
proof end;

theorem TSc2: :: EXCHSORT:34
for X, z, x, y 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
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)
proof end;

registration
let X be non empty set ;
cluster non empty Relation-like X -valued Function-like onto set ;
existence
ex b1 being non empty X -valued Function st b1 is onto
proof end;
end;

registration
let X be non empty set ;
let f be non empty X -valued onto Function;
let x, y be Element of dom f;
cluster Swap (f,x,y) -> onto ;
coherence
Swap (f,x,y) is onto
proof end;
end;

registration
let A be array;
let x, y be set ;
cluster Swap (A,x,y) -> segmental ;
coherence
Swap (A,x,y) is segmental
proof end;
end;

theorem :: EXCHSORT:36
for x, y being set
for A being array st x in dom A & y in dom A holds
Swap ((Swap (A,x,y)),x,y) = A
proof end;

registration
let A be real-valued array;
let x, y be set ;
cluster Swap (A,x,y) -> real-valued array;
coherence
for b1 being array st b1 = Swap (A,x,y) holds
b1 is real-valued
proof end;
end;

begin

definition
let A be array;
mode permutation of A -> array means :PERM: :: EXCHSORT:def 9
ex f being Permutation of (dom A) st it = A * f;
existence
ex b1 being array ex f being Permutation of (dom A) st b1 = A * f
proof end;
end;

:: deftheorem PERM defines permutation EXCHSORT:def 9 :
for A, b2 being array holds
( b2 is permutation of A iff ex f being Permutation of (dom A) st b2 = A * f );

theorem ThDom: :: EXCHSORT:37
for A being array
for B being permutation of A holds
( dom B = dom A & rng B = rng A )
proof end;

theorem ThRef: :: EXCHSORT:38
for A being array holds A is permutation of A
proof end;

theorem ThSym: :: EXCHSORT:39
for A, B being array st A is permutation of B holds
B is permutation of A
proof end;

theorem ThTr: :: 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
proof end;

theorem Th11: :: EXCHSORT:41
for X, x, y being set holds Swap ((id X),x,y) is one-to-one
proof end;

registration
let X be non empty set ;
let x, y be Element of X;
cluster Swap ((id X),x,y) -> X -defined X -valued one-to-one ;
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 Th11;
end;

registration
let X be non empty set ;
let x, y be Element of X;
cluster Swap ((id X),x,y) -> total onto ;
coherence
( Swap ((id X),x,y) is onto & Swap ((id X),x,y) is total )
proof end;
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
proof end;
end;

theorem Th12: :: EXCHSORT:42
for x, X, y 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
proof end;

theorem Th13: :: 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) )
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) )
proof end;

begin

definition
let O be RelStr ;
let A be array of O;
attr A is ascending means :: EXCHSORT:def 10
for a, b being ordinal number 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 ) } is set
;
end;

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

registration
let O be RelStr ;
cluster empty Relation-like the carrier of O -valued Function-like segmental -> empty ascending set ;
coherence
for b1 being empty array of O holds b1 is ascending
proof end;
let A be empty array of O;
cluster inversions A -> empty ;
coherence
inversions A is empty
proof end;
end;

theorem LemO: :: EXCHSORT:45
for O being non empty connected Poset
for x, y being Element of O holds
( x > y iff not x <= y )
proof end;

definition
let O be non empty connected Poset;
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
for b1 being set holds
( b1 = inversions R iff b1 = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } )
proof end;
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 ) } ;

theorem TW0: :: EXCHSORT:46
for x, y being set
for O being non empty connected Poset
for R being array of O 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 TW1: :: EXCHSORT:47
for O being non empty connected Poset
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;
cluster inversions R -> finite ;
coherence
inversions R is finite
proof end;
end;

theorem SORT: :: EXCHSORT:48
for O being non empty connected Poset
for R being array of O holds
( R is ascending iff inversions R = {} )
proof end;

theorem TW2: :: 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
proof end;

theorem TW3: :: 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
proof end;

registration
let O be non empty connected Poset;
let R be array of O;
cluster inversions R -> Relation-like ;
coherence
inversions R is Relation-like
proof end;
end;

registration
let O be non empty connected Poset;
let R be array of O;
cluster inversions R -> asymmetric transitive Relation;
coherence
for b1 being Relation st b1 = inversions R holds
( b1 is asymmetric & b1 is transitive )
proof end;
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 a < b holds
not b < a
by ORDERS_2:29;
end;

theorem TC5: :: 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))
proof end;

theorem TC1: :: 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)) )
proof end;

theorem TC2: :: 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)) )
proof end;

theorem TC3: :: 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)) ) )
proof end;

theorem TC4: :: 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
proof end;

theorem TC8: :: 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
proof end;

theorem TC6: :: 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
proof end;

theorem TC7: :: 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)) )
proof end;

definition
let O be non empty connected Poset;
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}:])) is Function
;
end;

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

theorem TT: :: EXCHSORT:59
for c, b, a being ordinal number holds
( c in (succ b) \ a iff ( a c= c & c c= b ) )
proof end;

theorem FF1: :: EXCHSORT:60
for O being non empty connected Poset
for T being non empty array of O
for q, p being Element of dom T holds (succ q) \ p c= dom T
proof end;

theorem FF2: :: 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):] )
proof end;

theorem FF3: :: EXCHSORT:62
for O being non empty connected Poset
for T being non empty array of O
for p, r, q 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 FF5: :: EXCHSORT:63
for f being Function
for O being non empty connected Poset
for T being non empty array of O
for r, p, s, q 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 FF6: :: EXCHSORT:64
for f being Function
for O being non empty connected Poset
for T being non empty array of O
for r, p, q 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 FF7: :: EXCHSORT:65
for f being Function
for O being non empty connected Poset
for T being non empty array of O
for q, r, p 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 Case5: :: 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]
proof end;

theorem Case1: :: 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]
proof end;

theorem Case23: :: EXCHSORT:68
for O being non empty connected Poset
for T being non empty array of O
for r, p, q 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 Case47: :: EXCHSORT:69
for O being non empty connected Poset
for T being non empty array of O
for p, s, q 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 Case68: :: 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] )
proof end;

O2O: 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 one2one: :: 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
proof end;

registration
let O be non empty connected Poset;
let R be array of O;
let x, y, z be set ;
cluster ((R,x,y) incl) .: z -> Relation-like ;
coherence
((R,x,y) incl) .: z is Relation-like
proof end;
end;

begin

theorem MAIN1: :: 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
proof end;

registration
let R be finite Function;
let x, y be set ;
cluster Swap (R,x,y) -> finite ;
coherence
Swap (R,x,y) is finite
proof end;
end;

theorem MAIN3: :: 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)
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)
proof end;

definition
let O be non empty connected Poset;
let R be array of O;
mode arr_computation of R -> non empty array means :COMP: :: EXCHSORT:def 14
( it . (base- it) = R & ( for a being ordinal number st a in dom it holds
it . a is array of O ) & ( for a being ordinal number 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
ex b1 being non empty array st
( b1 . (base- b1) = R & ( for a being ordinal number st a in dom b1 holds
b1 . a is array of O ) & ( for a being ordinal number st a in dom b1 & succ a in dom b1 holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & b1 . a = R & b1 . (succ a) = Swap (R,x,y) ) ) )
proof end;
end;

:: deftheorem COMP defines arr_computation EXCHSORT:def 14 :
for O being non empty connected Poset
for R being array of O
for b3 being non empty array holds
( b3 is arr_computation of R iff ( b3 . (base- b3) = R & ( for a being ordinal number st a in dom b3 holds
b3 . a is array of O ) & ( for a being ordinal number st a in dom b3 & succ a in dom b3 holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & b3 . a = R & b3 . (succ a) = Swap (R,x,y) ) ) ) );

theorem TC0: :: EXCHSORT:75
for a being ordinal number
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 number ;
cluster non empty Relation-like Function-like finite segmental a -based arr_computation of R;
existence
ex b1 being arr_computation of R st
( b1 is a -based & b1 is finite )
proof end;
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 ;
cluster C . x -> Relation-like Function-like segmental ;
coherence
( C . x is segmental & C . x is Function-like & C . x is Relation-like )
proof end;
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 ;
cluster C . x -> the carrier of O -valued ;
coherence
C . x is the carrier of O -valued
proof end;
end;

registration
let O be non empty connected Poset;
let R be array of O;
let C be arr_computation of R;
cluster last C -> Relation-like Function-like segmental ;
coherence
( last C is segmental & last C is Relation-like & last C is Function-like )
;
end;

registration
let O be non empty connected Poset;
let R be array of O;
let C be arr_computation of R;
cluster last C -> the carrier of O -valued ;
coherence
last C is the carrier of O -valued
;
end;

definition
let O be non empty connected Poset;
let R be array of O;
let C be arr_computation of R;
attr C is complete means :COMPL: :: EXCHSORT:def 15
last C is ascending ;
end;

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

theorem MAIN4: :: 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
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 number st inversions (C . a) <> {} holds
succ a in dom C ) holds
C is complete
proof end;

theorem Th83: :: 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 number st a in dom C holds
C . a is permutation of R ) )
proof end;

begin

theorem Lem3: :: EXCHSORT:79
for X being set
for A being finite 0 -based array of X st A <> {} holds
last A in X
proof end;

theorem Lem4: :: EXCHSORT:80
for x being set holds last <%x%> = x
proof end;

theorem Lem5: :: EXCHSORT:81
for x being set
for A being finite 0 -based array holds last (A ^ <%x%>) = x
proof end;

registration
let X be set ;
cluster -> X -valued Element of X ^omega ;
coherence
for b1 being Element of X ^omega holds b1 is X -valued
by AFINSQ_1:46;
end;

scheme :: EXCHSORT:sch 2
A{ F1( set ) -> set , F2() -> non empty set , P1[ set , set ], F3() -> set } :
ex f being non empty finite 0 -based array ex k being Element of F2() st
( k = last f & F1(k) = {} & f . 0 = F3() & ( for a being ordinal number st succ a in dom f holds
ex x, y being Element of F2() st
( x = f . a & y = f . (succ a) & P1[x,y] ) ) )
provided
A0: F3() in F2() and
A1: F1(F3()) is finite and
A2: for x being Element of F2() st F1(x) <> {} holds
ex y being Element of F2() st
( P1[x,y] & F1(y) c< F1(x) )
proof end;

theorem ThF: :: EXCHSORT:82
for A being array
for B being permutation of A holds B in Funcs ((dom A),(rng A))
proof end;

registration
let A be real-valued array;
cluster -> real-valued permutation of A;
coherence
for b1 being permutation of A holds b1 is real-valued
proof end;
end;

registration
let a be ordinal number ;
let X be non empty set ;
cluster -> T-Sequence-like Element of Funcs (a,X);
coherence
for b1 being Element of Funcs (a,X) holds b1 is T-Sequence-like
proof end;
end;

registration
let X be set ;
let Y be real-membered non empty set ;
cluster -> real-valued Element of Funcs (X,Y);
coherence
for b1 being Element of Funcs (X,Y) holds b1 is real-valued
;
end;

registration
let X be set ;
let A be array of X;
cluster -> X -valued permutation of A;
coherence
for b1 being permutation of A holds b1 is X -valued
proof end;
end;

registration
let X, Z be set ;
let Y be Subset of Z;
cluster -> Z -valued Element of Funcs (X,Y);
coherence
for b1 being Element of Funcs (X,Y) holds b1 is Z -valued
proof end;
end;

theorem :: EXCHSORT:83
for X, Y being set
for r being b1 -defined b2 -valued Relation holds r is Relation of X,Y
proof end;

theorem Lem1: :: EXCHSORT:84
for a being finite Ordinal
for x being set holds
( not x in a or x = 0 or ex b being ordinal number st x = succ b )
proof end;

theorem ThComp: :: 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
proof end;

theorem ThSort: :: 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
proof end;

registration
let O be non empty connected Poset;
let A be finite 0 -based array of O;
cluster Relation-like the carrier of O -valued Function-like segmental ascending permutation of A;
existence
ex b1 being permutation of A st b1 is ascending
proof end;
end;