:: Sorting by Exchanging :: by Grzegorz Bancerek :: :: Received October 18, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin theorem Th1: :: 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 ) ) proofend; 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 Th2: :: 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 ) proofend; theorem :: EXCHSORT:3 for x, y being set st x nin y holds (y \/ {x}) \ y = {x} by XBOOLE_1:88, ZFMISC_1:50; theorem Th4: :: EXCHSORT:4 for x being set holds (succ x) \ x = {x} proofend; theorem Th5: :: 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 ) ) proofend; theorem Th6: :: 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 ) proofend; theorem Th7: :: 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 proofend; begin definition let f be set ; attrf is segmental means :Def1: :: EXCHSORT:def 1 ex a, b being ordinal number st proj1 f = a \ b; end; :: deftheorem Def1 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 proofend; theorem Th9: :: 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 proofend; registration cluster T-Sequence-like Relation-like Function-like -> segmental for set ; coherence for b1 being Function st b1 is T-Sequence-like holds b1 is segmental proofend; cluster Relation-like Function-like FinSequence-like -> segmental for set ; coherence for b1 being Function st b1 is FinSequence-like holds b1 is segmental proofend; end; definition let a be ordinal number ; let s be set ; attrs is a -based means :Def2: :: EXCHSORT:def 2 for b being ordinal number st b in proj1 s holds ( a in proj1 s & a c= b ); attrs is a -limited means :Def3: :: EXCHSORT:def 3 a = sup (proj1 s); end; :: deftheorem Def2 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 Def3 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 ) ) proofend; 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 ) ) proofend; registration cluster T-Sequence-like Relation-like Function-like -> 0 -based for set ; coherence for b1 being Function st b1 is T-Sequence-like holds b1 is 0 -based proofend; cluster Relation-like Function-like FinSequence-like -> 1 -based for set ; coherence for b1 being Function st b1 is FinSequence-like holds b1 is 1 -based proofend; end; theorem Th12: :: EXCHSORT:12 for f being Function holds f is inf (dom f) -based proofend; theorem :: EXCHSORT:13 for f being Function holds f is sup (dom f) -limited by Def3; 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 proofend; definition let f be Function; func base- f -> ordinal number means :Def4: :: 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 ) ) proofend; 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 ) ) proofend; consistency for b1 being ordinal number holds verum ; func limit- f -> ordinal number means :Def5: :: 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 ) ) proofend; 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 ) ) proofend; consistency for b1 being ordinal number holds verum ; end; :: deftheorem Def4 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 Def5 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 Th15: :: EXCHSORT:15 ( base- {} = 0 & limit- {} = 0 & len- {} = 0 ) proofend; theorem Th16: :: EXCHSORT:16 for f being Function holds limit- f = sup (dom f) proofend; theorem :: EXCHSORT:17 for f being Function holds f is limit- f -limited proofend; theorem Th18: :: EXCHSORT:18 for a being ordinal number for A being empty set holds A is a -based proofend; 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 for 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 ) proofend; end; definition mode array is segmental Function; end; registration let A be array; cluster proj1 A -> ordinal-membered ; coherence dom A is ordinal-membered proofend; end; theorem :: EXCHSORT:19 for f being array holds ( f is 0 -limited iff f is empty ) proofend; registration cluster Relation-like Function-like segmental 0 -based -> T-Sequence-like for set ; coherence for b1 being array st b1 is 0 -based holds b1 is T-Sequence-like proofend; 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 Th20: :: EXCHSORT:20 for f being Function holds base- f = inf (dom f) proofend; theorem :: EXCHSORT:21 for f being Function holds f is base- f -based proofend; theorem :: EXCHSORT:22 for A being array holds dom A = (limit- A) \ (base- A) proofend; theorem Th23: :: 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 ) proofend; theorem Th24: :: EXCHSORT:24 for f being T-Sequence holds ( base- f = 0 & limit- f = dom f & len- f = dom f ) proofend; registration let a, b be ordinal number ; 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 b1 being array of a,X st ( b1 is b -based & b1 is natural-valued & b1 is INT -valued & b1 is real-valued & b1 is complex-valued & b1 is finite ) proofend; end; registration let a be ordinal number ; let x be set ; cluster{[a,x]} -> segmental ; coherence {[a,x]} is segmental proofend; end; registration let a be ordinal number ; let x be Nat; cluster{[a,x]} -> natural-valued for array; coherence for b1 being array st b1 = {[a,x]} holds b1 is natural-valued proofend; end; registration let a be ordinal number ; let x be real number ; cluster{[a,x]} -> real-valued for array; coherence for b1 being array st b1 = {[a,x]} holds b1 is real-valued proofend; end; registration let a be ordinal number ; let X be non empty set ; let x be Element of X; cluster{[a,x]} -> X -valued for array; coherence for b1 being array st b1 = {[a,x]} holds b1 is X -valued proofend; end; registration let a be ordinal number ; let x be set ; cluster{[a,x]} -> a -based succ a -limited for array; coherence for b1 being array st b1 = {[a,x]} holds ( b1 is a -based & b1 is succ a -limited ) proofend; end; registration let b be ordinal number ; cluster non empty Relation-like INT -valued Function-like complex-valued real-valued natural-valued finite segmental b -based for set ; existence ex b1 being array st ( not b1 is empty & b1 is b -based & b1 is natural-valued & b1 is INT -valued & b1 is real-valued & b1 is complex-valued & b1 is finite ) proofend; let X be non empty set ; cluster non empty Relation-like X -valued Function-like finite segmental b -based for set ; existence ex b1 being array st ( not b1 is empty & b1 is b -based & b1 is finite & b1 is X -valued ) proofend; 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; identifyA last with last A; compatibility A last = last A ; end; begin definition let f be Function; attrf is descending means :Def8: :: 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 Def8 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 proofend; theorem Th26: :: 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 proofend; theorem Th27: :: EXCHSORT:27 for f being T-Sequence st f is descending & f . 0 is finite holds f is finite proofend; 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 = {} proofend; scheme :: EXCHSORT:sch 1 A{ F1() -> T-Sequence, F2( set ) -> set } : F1() is finite provided A1: F2((F1() . 0)) is finite and A2: 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)) proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th30: :: 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 proofend; 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 proofend; theorem Th32: :: 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 proofend; theorem Th33: :: 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 proofend; theorem Th34: :: 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 proofend; 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) proofend; registration let X be non empty set ; cluster non empty Relation-like X -valued Function-like onto for set ; existence ex b1 being non empty X -valued Function st b1 is onto proofend; 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 proofend; end; registration let A be array; let x, y be set ; cluster Swap (A,x,y) -> segmental ; coherence Swap (A,x,y) is segmental proofend; 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 proofend; registration let A be real-valued array; let x, y be set ; cluster Swap (A,x,y) -> real-valued for array; coherence for b1 being array st b1 = Swap (A,x,y) holds b1 is real-valued proofend; end; begin 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; existence ex b1 being array ex f being Permutation of (dom A) st b1 = A * f proofend; end; :: deftheorem Def9 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 Th37: :: EXCHSORT:37 for A being array for B being permutation of A holds ( dom B = dom A & rng B = rng A ) proofend; theorem Th38: :: EXCHSORT:38 for A being array holds A is permutation of A proofend; theorem Th39: :: EXCHSORT:39 for A, B being array st A is permutation of B holds B is permutation of A proofend; 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 proofend; theorem Th41: :: EXCHSORT:41 for X, x, y being set holds Swap ((id X),x,y) is one-to-one proofend; 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 Th41; 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 ) proofend; 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 proofend; end; theorem Th42: :: 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 proofend; 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) ) proofend; 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) ) proofend; begin definition let O be RelStr ; let A be array of O; attrA 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 for set ; coherence for b1 being empty array of O holds b1 is ascending proofend; let A be empty array of O; cluster inversions A -> empty ; coherence inversions A is empty proofend; 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 ) proofend; 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 ) } ) proofend; 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 Th46: :: 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 ) ) proofend; 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):] proofend; registration let O be non empty connected Poset; let R be finite array of O; cluster inversions R -> finite ; coherence inversions R is finite proofend; 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 = {} ) proofend; 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 proofend; 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 proofend; 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 proofend; end; registration let O be non empty connected Poset; let R be array of O; cluster inversions R -> asymmetric transitive for Relation; coherence for b1 being Relation st b1 = inversions R holds ( b1 is asymmetric & b1 is transitive ) proofend; end; definition let O be non empty connected Poset; let a, b be Element of O; :: original:< redefine preda < b; asymmetry for a, b being Element of O st R71(O,b1,b2) holds not R71(O,b2,b1) 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)) proofend; 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)) ) proofend; 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)) ) proofend; 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)) ) ) proofend; 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 proofend; 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 proofend; 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 proofend; 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)) ) proofend; 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 Th59: :: EXCHSORT:59 for c, b, a being ordinal number holds ( c in (succ b) \ a iff ( a c= c & c c= b ) ) proofend; theorem Th60: :: 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 proofend; 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):] ) proofend; theorem Th62: :: 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] ) proofend; theorem Th63: :: 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)] proofend; theorem Th64: :: 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)] ) proofend; theorem Th65: :: 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)] ) proofend; 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] proofend; 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] proofend; theorem Th68: :: 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] ) proofend; theorem Th69: :: 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] ) proofend; 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] ) proofend; 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 ) proofend; 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 proofend; 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 proofend; end; begin 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 proofend; registration let R be finite Function; let x, y be set ; cluster Swap (R,x,y) -> finite ; coherence Swap (R,x,y) is finite proofend; 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) proofend; 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) proofend; 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 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) ) ) ) proofend; end; :: deftheorem Def14 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 Th75: :: 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 proofend; 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 for arr_computation of R; existence ex b1 being arr_computation of R st ( b1 is a -based & b1 is finite ) proofend; 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 ; clusterC . x -> Relation-like Function-like segmental ; coherence ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) proofend; 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 ; clusterC . x -> the carrier of O -valued ; coherence C . x is the carrier of O -valued proofend; 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; attrC is complete means :Def15: :: EXCHSORT:def 15 last C is ascending ; end; :: deftheorem Def15 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 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 proofend; 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 proofend; 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 number st a in dom C holds C . a is permutation of R ) ) proofend; begin theorem Th79: :: EXCHSORT:79 for X being set for A being finite 0 -based array of X st A <> {} holds last A in X proofend; theorem Th80: :: EXCHSORT:80 for x being set holds last <%x%> = x proofend; theorem Th81: :: EXCHSORT:81 for x being set for A being finite 0 -based array holds last (A ^ <%x%>) = x proofend; registration let X be set ; cluster -> X -valued for Element of X ^omega ; coherence for b1 being Element of X ^omega holds b1 is X -valued by AFINSQ_1:42; 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 A1: F3() in F2() and A2: F1(F3()) is finite and A3: 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) ) proofend; theorem Th82: :: EXCHSORT:82 for A being array for B being permutation of A holds B in Funcs ((dom A),(rng A)) proofend; registration let A be real-valued array; cluster -> real-valued for permutation of A; coherence for b1 being permutation of A holds b1 is real-valued proofend; end; registration let a be ordinal number ; let X be non empty set ; cluster -> T-Sequence-like for Element of Funcs (a,X); coherence for b1 being Element of Funcs (a,X) holds b1 is T-Sequence-like proofend; end; registration let X be set ; let Y be real-membered non empty set ; cluster -> real-valued for 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 for permutation of A; coherence for b1 being permutation of A holds b1 is X -valued proofend; end; registration let X, Z be set ; let Y be Subset of Z; cluster -> Z -valued for Element of Funcs (X,Y); coherence for b1 being Element of Funcs (X,Y) holds b1 is Z -valued proofend; end; theorem :: EXCHSORT:83 for X, Y being set for r being b1 -defined b2 -valued Relation holds r is Relation of X,Y proofend; 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 number st x = succ b ) proofend; 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 proofend; 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 proofend; 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 for permutation of A; existence ex b1 being permutation of A st b1 is ascending proofend; end;