EXCHSORT: Sorting by Exchanging

proof end;

cluster Relation-like Function-like FinSequence-like -> segmental for set ;

proof end;

end;

definition

let a be Ordinal;
let s be set ;

attr s is a -based means :: EXCHSORT:def 2
for b being Ordinal st b in proj1 s holds
( a in proj1 s & a c= b );

attr s is a -limited means :: EXCHSORT:def 3
a = sup (proj1 s);

end;

:: deftheorem defines -based EXCHSORT:def 2 :

:: deftheorem defines -limited EXCHSORT:def 3 :

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

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

proof end;

registration

cluster Relation-like Sequence-like Function-like -> 0 -based for set ;

coherence by ORDINAL3:8;

cluster Relation-like Function-like FinSequence-like -> 1 -based for set ;

proof end;

end;

theorem Th12: :: EXCHSORT:12

for f being Function holds f is inf (dom f) -based by ORDINAL2:14, ORDINAL2:17;

theorem :: EXCHSORT:13

for f being Function holds f is sup (dom f) -limited ;

theorem :: EXCHSORT:14

for a, b being Ordinal
for f being Function st f is b -limited & a in dom f holds
a in b by ORDINAL2:19;

definition

let f be Function;

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 ;

proof end;

uniqueness

proof end;

consistency ;

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 ;

proof end;

uniqueness ;
consistency ;

end;

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

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

definition

let f be Function;

func len- f -> Ordinal equals :: EXCHSORT:def 6
(limit- f) -^ (base- f);

end;

:: deftheorem defines len- EXCHSORT:def 6 :

theorem Th15: :: EXCHSORT:15

( base- {} = 0 & limit- {} = 0 & len- {} = 0 )

proof end;

theorem Th16: :: 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 by Th16;

theorem :: EXCHSORT:18

for a being Ordinal
for A being empty set holds A is a -based ;

registration

let a be Ordinal;
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 ;

proof end;

end;

definition

mode array is segmental Function;

end;

registration

let A be array;

cluster proj1 A -> 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 -> Sequence-like for set ;

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;
let X be set ;
mode array of a,X is a -defined array of X;

end;

theorem Th20: :: 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 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 )

proof end;

theorem Th24: :: EXCHSORT:24

for f being Sequence holds
( base- f = 0 & limit- f = dom f & len- f = dom f )

proof end;

registration

let a, b be Ordinal;
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 ;

proof end;

end;

registration

let a be Ordinal;
let x be set ;

cluster {[a,x]} -> segmental ;

proof end;

end;

registration

let a be Ordinal;
let x be Nat;

cluster {[a,x]} -> natural-valued for array;

proof end;

end;

registration

let a be Ordinal;
let x be Real;

cluster {[a,x]} -> real-valued for array;

proof end;

end;

registration

let a be Ordinal;
let X be non empty set ;
let x be Element of X;

cluster {[a,x]} -> X -valued for array;

proof end;

end;

registration

let a be Ordinal;
let x be set ;

cluster {[a,x]} -> a -based succ a -limited for array;

proof end;

end;

registration

let b be Ordinal;

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

proof end;

let X be non empty set ;

cluster Relation-like X -valued Function-like non empty finite segmental b -based for set ;

proof end;

end;

notation

let s be 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));

end;

:: deftheorem defines last EXCHSORT:def 7 :

registration

let A be Sequence;

identify A last with last A;

compatibility ;

end;

definition

let f be Function;

attr f is descending means :: EXCHSORT:def 8
for a, b being Ordinal st a in dom f & b in dom f & a in b holds
f . b c< f . a;

end;

:: deftheorem defines descending EXCHSORT:def 8 :

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

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

proof end;

theorem Th27: :: EXCHSORT:27

for f being Sequence st f is descending & f . 0 is finite holds
f is finite

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

proof end;

scheme :: EXCHSORT:sch 1
A{ F₁() -> Sequence, F₂( set ) -> set } :

F₁() is finite

provided

A1: F₂((F₁() . 0)) is finite and
A2: for a being Ordinal st succ a in dom F₁() & F₂((F₁() . a)) is finite holds
F₂((F₁() . (succ a))) c< F₂((F₁() . a))

proof end;

registration

let X be set ;
let f be X -defined Function;
let a, b be object ;

cluster Swap (f,a,b) -> X -defined ;

proof end;

end;

registration

let X be set ;
let f be X -valued Function;
let x, y be object ;

cluster Swap (f,x,y) -> X -valued ;

proof end;

end;

theorem Th29: :: 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 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

proof end;

theorem Th31: :: 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 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

proof end;

theorem Th33: :: EXCHSORT:33

for f being Function
for x, y, z being object st z <> x & z <> y holds
(Swap (f,x,y)) . z = f . z

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

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 Relation-like X -valued Function-like non empty onto for set ;

proof end;

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;

cluster Swap (f,x,y) -> onto ;

proof end;

end;

registration

let A be array;
let x, y be set ;

cluster Swap (A,x,y) -> 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 for array;

proof end;

end;

definition

let A be array;

mode permutation of A -> array means :Def9: :: EXCHSORT:def 9
ex f being Permutation of (dom A) st it = A * f;

proof end;

end;

:: deftheorem Def9 defines permutation EXCHSORT:def 9 :

theorem Th37: :: EXCHSORT:37

for A being array
for B being permutation of A holds
( dom B = dom A & rng B = rng A )

proof end;

theorem Th38: :: EXCHSORT:38

for A being array holds A is permutation of A

proof end;

theorem Th39: :: EXCHSORT:39

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

proof end;

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

proof end;

theorem Th41: :: EXCHSORT:41

for x, y, X 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 by Th41;

end;

registration

let X be non empty set ;
let x, y be Element of X;

cluster Swap ((id X),x,y) -> total onto ;

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

proof end;

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

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

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;

definition

let O be RelStr ;
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;

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

end;

:: deftheorem defines ascending EXCHSORT:def 10 :

:: deftheorem defines inversions EXCHSORT:def 11 :

registration

let O be RelStr ;

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

coherence ;
let A be empty array of O;

cluster inversions A -> empty ;

proof end;

end;

theorem Th45: :: 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

proof end;

end;

:: deftheorem defines inversions EXCHSORT:def 12 :

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

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

proof end;

registration

let O be non empty connected Poset;
let R be finite array of O;

cluster inversions R -> finite ;

proof end;

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

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

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

proof end;

registration

let O be non empty connected Poset;
let R be array of O;

cluster inversions R -> Relation-like ;

proof end;

end;

registration

let O be non empty connected Poset;
let R be array of O;

cluster inversions R -> asymmetric transitive for Relation;

proof end;

end;

definition

let O be non empty connected Poset;
let a, b be Element of O;
:: original: <
redefine pred a < b;
asymmetry by ORDERS_2:5;

end;

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

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

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

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

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

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

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

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

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

end;

:: deftheorem defines incl EXCHSORT:def 13 :

theorem Th59: :: EXCHSORT:59

for a, b, c being Ordinal holds
( c in (succ b) \ a iff ( a c= c & c c= b ) )

proof end;

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

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

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

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

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

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

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]

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]

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

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

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

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

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 ;

proof end;

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

proof end;

registration

let R be finite Function;
let x, y be set ;

cluster Swap (R,x,y) -> finite ;

proof end;

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)

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

proof end;

end;

:: deftheorem Def14 defines arr_computation EXCHSORT:def 14 :

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

proof end;

registration

let O be non empty connected Poset;
let R be array of O;
let a be Ordinal;

cluster Relation-like Function-like non empty finite segmental a -based for arr_computation of R;

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 ;

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 ;

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 ;

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 ;