:: EXCHSORT semantic presentation 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 ) ) proof let a, b be ordinal number ; ::_thesis: for x being set holds ( x in (a +^ b) \ a iff ex c being ordinal number st ( x = a +^ c & c in b ) ) let x be set ; ::_thesis: ( x in (a +^ b) \ a iff ex c being ordinal number st ( x = a +^ c & c in b ) ) A1: ( x in (a +^ b) \ a iff ( a c= x & x in a +^ b ) ) by ORDINAL6:5; hereby ::_thesis: ( ex c being ordinal number st ( x = a +^ c & c in b ) implies x in (a +^ b) \ a ) assume A2: x in (a +^ b) \ a ; ::_thesis: ex d being set st ( x = a +^ d & d in b ) then reconsider c = x as Ordinal ; take d = c -^ a; ::_thesis: ( x = a +^ d & d in b ) thus x = a +^ d by A1, A2, ORDINAL3:def_5; ::_thesis: d in b hence d in b by A2, ORDINAL3:22; ::_thesis: verum end; given c being ordinal number such that A3: ( x = a +^ c & c in b ) ; ::_thesis: x in (a +^ b) \ a ( a c= x & x in a +^ b ) by A3, ORDINAL2:32, ORDINAL3:24; hence x in (a +^ b) \ a by ORDINAL6:5; ::_thesis: verum 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 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 ) proof let a, b, c, d be ordinal number ; ::_thesis: ( 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 ) implies ( c = b & b in d ) ) assume A1: ( a in b & c in d ) ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) percases ( c in a or c = a or ( a in c & c in b ) or c = b or b in c ) by ORDINAL1:14; suppose c in a ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum end; suppose c = a ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by ORDINAL1:14; ::_thesis: verum end; supposeA2: ( a in c & c in b ) ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) percases ( d in b or d = b or b in d ) by ORDINAL1:14; suppose d in b ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum end; suppose d = b ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A2; ::_thesis: verum end; suppose b in d ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum end; end; end; suppose c = b ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum end; suppose b in c ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) hence ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum end; end; end; 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} proof let x be set ; ::_thesis: (succ x) \ x = {x} ( succ x = x \/ {x} & x nin x ) ; hence (succ x) \ x = {x} by XBOOLE_1:88, ZFMISC_1:50; ::_thesis: verum end; 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 ) ) proof let f be Function; ::_thesis: 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 ) ) let r be Relation; ::_thesis: 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 ) ) let x be set ; ::_thesis: ( x in f .: r iff ex y, z being set st ( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) ) hereby ::_thesis: ( ex y, z being set st ( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) implies x in f .: r ) assume x in f .: r ; ::_thesis: ex y, z being set st ( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) then consider t being set such that A1: ( t in dom f & t in r & x = f . t ) by FUNCT_1:def_6; consider y, z being set such that A2: t = [y,z] by A1, RELAT_1:def_1; f . (y,z) = f . [y,z] ; hence ex y, z being set st ( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) by A1, A2; ::_thesis: verum end; thus ( ex y, z being set st ( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) implies x in f .: r ) by FUNCT_1:def_6; ::_thesis: verum end; 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 ) proof let a, b be ordinal number ; ::_thesis: ( a \ b <> {} implies ( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a ) ) assume A1: a \ b <> {} ; ::_thesis: ( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a ) set x = the Element of a \ b; A2: the Element of a \ b in a \ b by A1; A3: ( the Element of a \ b in a & the Element of a \ b nin b ) by A1, XBOOLE_0:def_5; then b c= the Element of a \ b by ORDINAL6:4; then ( b in a & b nin b ) by A3, ORDINAL1:12; then A4: b in a \ b by XBOOLE_0:def_5; hence inf (a \ b) c= b by ORDINAL2:14; :: according to XBOOLE_0:def_10 ::_thesis: ( b c= inf (a \ b) & sup (a \ b) = a & union (a \ b) = union a ) inf (a \ b) in a \ b by A2, ORDINAL2:17; then inf (a \ b) nin b by XBOOLE_0:def_5; hence b c= inf (a \ b) by ORDINAL6:4; ::_thesis: ( sup (a \ b) = a & union (a \ b) = union a ) A5: On (a \ b) = a \ b by ORDINAL6:2; thus sup (a \ b) c= a by A5, ORDINAL2:def_3; :: according to XBOOLE_0:def_10 ::_thesis: ( a c= sup (a \ b) & union (a \ b) = union a ) thus a c= sup (a \ b) ::_thesis: union (a \ b) = union a proof let c be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not c in a or c in sup (a \ b) ) assume A6: c in a ; ::_thesis: c in sup (a \ b) A7: b in sup (a \ b) by A4, ORDINAL2:19; percases ( c in b or c nin b ) ; suppose c in b ; ::_thesis: c in sup (a \ b) hence c in sup (a \ b) by A7, ORDINAL1:10; ::_thesis: verum end; suppose c nin b ; ::_thesis: c in sup (a \ b) then c in a \ b by A6, XBOOLE_0:def_5; hence c in sup (a \ b) by ORDINAL2:19; ::_thesis: verum end; end; end; thus union (a \ b) c= union a by ZFMISC_1:77; :: according to XBOOLE_0:def_10 ::_thesis: union a c= union (a \ b) for y being set st y in union a holds y in union (a \ b) proof let y be set ; ::_thesis: ( y in union a implies y in union (a \ b) ) assume y in union a ; ::_thesis: y in union (a \ b) then consider x being set such that A8: ( y in x & x in a ) by TARSKI:def_4; reconsider x = x as Ordinal by A8; percases ( x in b or b c= x ) by ORDINAL6:4; suppose x in b ; ::_thesis: y in union (a \ b) then y in b by A8, ORDINAL1:10; hence y in union (a \ b) by A4, TARSKI:def_4; ::_thesis: verum end; suppose b c= x ; ::_thesis: y in union (a \ b) then x in a \ b by A8, ORDINAL6:5; hence y in union (a \ b) by A8, TARSKI:def_4; ::_thesis: verum end; end; end; hence union a c= union (a \ b) by TARSKI:def_3; ::_thesis: verum end; 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 proof let a, b be ordinal number ; ::_thesis: ( not a \ b is empty & a \ b is finite implies ex n being Nat st a = b +^ n ) assume A1: ( not a \ b is empty & a \ b is finite ) ; ::_thesis: ex n being Nat st a = b +^ n set x = the Element of a \ b; A2: ( the Element of a \ b in a & the Element of a \ b nin b ) by A1, XBOOLE_0:def_5; then b c= the Element of a \ b by ORDINAL6:4; then consider c being ordinal number such that A3: ( a = b +^ c & c <> {} ) by A2, ORDINAL1:12, ORDINAL3:28; deffunc H1( Ordinal) -> set = b +^ \$1; consider f being T-Sequence such that A4: ( dom f = omega & ( for d being ordinal number st d in omega holds f . d = H1(d) ) ) from ORDINAL2:sch_2(); f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y ) assume A5: ( x in dom f & y in dom f & f . x = f . y & x <> y ) ; ::_thesis: contradiction then reconsider x = x, y = y as Element of omega by A4; A6: ( f . x = H1(x) & f . y = H1(y) ) by A4; ( x in y or y in x ) by A5, ORDINAL1:14; then ( b +^ x in b +^ y or b +^ y in b +^ x ) by ORDINAL2:32; hence contradiction by A5, A6; ::_thesis: verum end; then A7: omega , rng f are_equipotent by A4, WELLORD2:def_4; now__::_thesis:_not_omega_c=_c assume omega c= c ; ::_thesis: contradiction then A8: H1( omega ) c= a by A3, ORDINAL2:33; rng f c= a \ b proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in a \ b ) assume y in rng f ; ::_thesis: y in a \ b then consider x being set such that A9: ( x in dom f & y = f . x ) by FUNCT_1:def_3; reconsider x = x as Element of omega by A4, A9; A10: y = H1(x) by A4, A9; ( b c= H1(x) & H1(x) in H1( omega ) ) by ORDINAL2:32, ORDINAL3:24; then ( y nin b & y in a ) by A8, A10, ORDINAL6:4; hence y in a \ b by XBOOLE_0:def_5; ::_thesis: verum end; hence contradiction by A1, A7, CARD_1:38; ::_thesis: verum end; then c in omega by ORDINAL6:4; hence ex n being Nat st a = b +^ n by A3; ::_thesis: verum end; 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 proof let f, g be Function; ::_thesis: ( dom f = dom g & f is segmental implies g is segmental ) assume A1: dom f = dom g ; ::_thesis: ( not f is segmental or g is segmental ) given a, b being ordinal number such that A2: dom f = a \ b ; :: according to EXCHSORT:def_1 ::_thesis: g is segmental take a ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 g = a \ b take b ; ::_thesis: proj1 g = a \ b thus proj1 g = a \ b by A1, A2; ::_thesis: verum end; 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 proof let f be Function; ::_thesis: ( f is segmental implies 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 ) given x, y being Ordinal such that A1: dom f = x \ y ; :: according to EXCHSORT:def_1 ::_thesis: 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 let a, b, c be ordinal number ; ::_thesis: ( a c= b & b c= c & a in dom f & c in dom f implies b in dom f ) assume A2: ( a c= b & b c= c & a in dom f & c in dom f ) ; ::_thesis: b in dom f then ( y c= a & c in x ) by A1, ORDINAL6:5; then ( y c= b & b in x ) by A2, ORDINAL1:12, XBOOLE_1:1; hence b in dom f by A1, ORDINAL6:5; ::_thesis: verum end; 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 proof let f be Function; ::_thesis: ( f is T-Sequence-like implies f is segmental ) assume f is T-Sequence-like ; ::_thesis: f is segmental then reconsider f = f as T-Sequence ; take dom f ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 f = (dom f) \ b take 0 ; ::_thesis: proj1 f = (dom f) \ 0 thus proj1 f = (dom f) \ 0 ; ::_thesis: verum end; cluster Relation-like Function-like FinSequence-like -> segmental for set ; coherence for b1 being Function st b1 is FinSequence-like holds b1 is segmental proof let f be Function; ::_thesis: ( f is FinSequence-like implies f is segmental ) assume f is FinSequence-like ; ::_thesis: f is segmental then reconsider g = f as FinSequence ; take a = succ (len g); :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 f = a \ b take b = 1; ::_thesis: proj1 f = a \ b reconsider c = len g as Nat ; thus dom f c= a \ b :: according to XBOOLE_0:def_10 ::_thesis: a \ b c= proj1 f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in a \ b ) assume A1: x in dom f ; ::_thesis: x in a \ b then x in dom g ; then reconsider x = x as Nat ; x <= c by A1, FINSEQ_3:25; then A2: ( 1 <= x & x <= c ) by A1, FINSEQ_3:25; then ( succ 0 c= x & x c= c ) by NAT_1:39; then A3: ( 0 in x & x in a ) by ORDINAL1:21, ORDINAL1:22; not x in b by A2, CARD_1:49, TARSKI:def_1; hence x in a \ b by A3, XBOOLE_0:def_5; ::_thesis: verum end; reconsider d = a as Element of NAT by ORDINAL1:def_12; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a \ b or x in proj1 f ) assume A4: x in a \ b ; ::_thesis: x in proj1 f then A5: ( x in d & not x in b ) by XBOOLE_0:def_5; reconsider x = x as Nat by A4; ( x c= c & b c= x ) by A5, ORDINAL1:16, ORDINAL1:22; then ( 1 <= x & x <= c ) by NAT_1:39; hence x in proj1 f by FINSEQ_3:25; ::_thesis: verum end; 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 ) ) proof let a be ordinal number ; ::_thesis: 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 ) ) let f be Function; ::_thesis: ( ( f is a -based & f is segmental ) iff ex b being ordinal number st ( dom f = b \ a & a c= b ) ) thus ( f is a -based & f is segmental implies ex b being ordinal number st ( dom f = b \ a & a c= b ) ) ::_thesis: ( ex b being ordinal number st ( dom f = b \ a & a c= b ) implies ( f is a -based & f is segmental ) ) proof assume A1: for b being ordinal number st b in dom f holds ( a in dom f & a c= b ) ; :: according to EXCHSORT:def_2 ::_thesis: ( not f is segmental or ex b being ordinal number st ( dom f = b \ a & a c= b ) ) given c, d being ordinal number such that A2: dom f = c \ d ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st ( dom f = b \ a & a c= b ) set x = the Element of c \ d; percases ( dom f = {} or dom f <> {} ) ; suppose dom f = {} ; ::_thesis: ex b being ordinal number st ( dom f = b \ a & a c= b ) then a \ a = dom f by XBOOLE_1:37; hence ex b being ordinal number st ( dom f = b \ a & a c= b ) ; ::_thesis: verum end; suppose dom f <> {} ; ::_thesis: ex b being ordinal number st ( dom f = b \ a & a c= b ) then the Element of c \ d in dom f by A2; then a in dom f by A1; then A3: ( d c= a & a in c ) by A2, ORDINAL6:5; then d in c by ORDINAL1:12; then d in dom f by A2, ORDINAL6:5; then a c= d by A1; then ( a = d & a c= c ) by A3, ORDINAL1:def_2, XBOOLE_0:def_10; hence ex b being ordinal number st ( dom f = b \ a & a c= b ) by A2; ::_thesis: verum end; end; end; given b being ordinal number such that A4: ( dom f = b \ a & a c= b ) ; ::_thesis: ( f is a -based & f is segmental ) thus f is a -based ::_thesis: f is segmental proof let c be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( c in proj1 f implies ( a in proj1 f & a c= c ) ) assume A5: c in dom f ; ::_thesis: ( a in proj1 f & a c= c ) then ( a c= c & c in b ) by A4, ORDINAL6:5; then a in b by ORDINAL1:12; hence ( a in proj1 f & a c= c ) by A4, A5, ORDINAL6:5; ::_thesis: verum end; take b ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 f = b \ b take a ; ::_thesis: proj1 f = b \ a thus proj1 f = b \ a by A4; ::_thesis: verum 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 let b be ordinal number ; ::_thesis: 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 ) ) let f be Function; ::_thesis: ( ( 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 ) ) thus ( f is b -limited & not f is empty & f is segmental implies ex a being ordinal number st ( dom f = b \ a & a in b ) ) ::_thesis: ( ex a being ordinal number st ( dom f = b \ a & a in b ) implies ( f is b -limited & not f is empty & f is segmental ) ) proof assume A1: b = sup (dom f) ; :: according to EXCHSORT:def_3 ::_thesis: ( f is empty or not f is segmental or ex a being ordinal number st ( dom f = b \ a & a in b ) ) assume A2: not f is empty ; ::_thesis: ( not f is segmental or ex a being ordinal number st ( dom f = b \ a & a in b ) ) given c, d being ordinal number such that A3: dom f = c \ d ; :: according to EXCHSORT:def_1 ::_thesis: ex a being ordinal number st ( dom f = b \ a & a in b ) set x = the Element of c \ d; take a = d; ::_thesis: ( dom f = b \ a & a in b ) A4: b = c by A2, A1, A3, Th6; thus dom f = b \ a by A2, A1, A3, Th6; ::_thesis: a in b ( a c= the Element of c \ d & the Element of c \ d in b ) by A2, A3, A4, ORDINAL6:5; hence a in b by ORDINAL1:12; ::_thesis: verum end; given a being ordinal number such that A5: ( dom f = b \ a & a in b ) ; ::_thesis: ( f is b -limited & not f is empty & f is segmental ) a in dom f by A5, ORDINAL6:5; hence b = sup (dom f) by A5, Th6; :: according to EXCHSORT:def_3 ::_thesis: ( not f is empty & f is segmental ) thus not f is empty by A5, ORDINAL6:5; ::_thesis: f is segmental take b ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 f = b \ b take a ; ::_thesis: proj1 f = b \ a thus proj1 f = b \ a by A5; ::_thesis: verum end; 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 proof let f be Function; ::_thesis: ( f is T-Sequence-like implies f is 0 -based ) assume f is T-Sequence-like ; ::_thesis: f is 0 -based then reconsider g = f as T-Sequence ; let b be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( b in proj1 f implies ( 0 in proj1 f & 0 c= b ) ) assume b in dom f ; ::_thesis: ( 0 in proj1 f & 0 c= b ) then b in dom g ; hence ( 0 in proj1 f & 0 c= b ) by ORDINAL3:8; ::_thesis: verum end; 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 proof let f be Function; ::_thesis: ( f is FinSequence-like implies f is 1 -based ) assume f is FinSequence-like ; ::_thesis: f is 1 -based then reconsider g = f as FinSequence ; let b be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( b in proj1 f implies ( 1 in proj1 f & 1 c= b ) ) assume b in dom f ; ::_thesis: ( 1 in proj1 f & 1 c= b ) then A1: b in dom g ; then reconsider b = b as Nat ; A2: ( 1 <= b & b <= len g ) by A1, FINSEQ_3:25; then 1 <= len g by XXREAL_0:2; hence ( 1 in proj1 f & 1 c= b ) by A2, FINSEQ_3:25, NAT_1:39; ::_thesis: verum end; end; theorem Th12: :: EXCHSORT:12 for f being Function holds f is inf (dom f) -based proof let f be Function; ::_thesis: f is inf (dom f) -based set b = inf (dom f); let c be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( c in proj1 f implies ( inf (dom f) in proj1 f & inf (dom f) c= c ) ) assume c in dom f ; ::_thesis: ( inf (dom f) in proj1 f & inf (dom f) c= c ) hence ( inf (dom f) in dom f & inf (dom f) c= c ) by ORDINAL2:14, ORDINAL2:17; ::_thesis: verum end; 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 proof let b, a be ordinal number ; ::_thesis: for f being Function st f is b -limited & a in dom f holds a in b let f be Function; ::_thesis: ( f is b -limited & a in dom f implies a in b ) assume b = sup (dom f) ; :: according to EXCHSORT:def_3 ::_thesis: ( not a in dom f or a in b ) hence ( not a in dom f or a in b ) by ORDINAL2:19; ::_thesis: verum end; 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 ) ) proof set b = inf (dom f); hereby ::_thesis: ( ( for a being ordinal number holds not a in dom f ) implies ex b1 being ordinal number st b1 = 0 ) given a being ordinal number such that a in dom f ; ::_thesis: ex b being set st f is b -based take b = inf (dom f); ::_thesis: f is b -based thus f is b -based by Th12; ::_thesis: verum end; assume for a being ordinal number holds not a in dom f ; ::_thesis: ex b1 being ordinal number st b1 = 0 take 0 ; ::_thesis: 0 = 0 thus 0 = 0 ; ::_thesis: verum 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 let b, c be ordinal number ; ::_thesis: ( ( ex a being ordinal number st a in dom f & f is b -based & f is c -based implies b = c ) & ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) ) hereby ::_thesis: ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) given a being ordinal number such that A1: a in dom f ; ::_thesis: ( f is b -based & f is c -based implies b = c ) assume A2: ( f is b -based & f is c -based ) ; ::_thesis: b = c thus b = c ::_thesis: verum proof c in dom f by A1, A2, Def2; hence b c= c by A2, Def2; :: according to XBOOLE_0:def_10 ::_thesis: c c= b b in dom f by A1, A2, Def2; hence c c= b by A2, Def2; ::_thesis: verum end; end; thus ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) ; ::_thesis: verum end; 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 ) ) proof set b = sup (dom f); hereby ::_thesis: ( ( for a being ordinal number holds not a in dom f ) implies ex b1 being ordinal number st b1 = 0 ) given a being ordinal number such that a in dom f ; ::_thesis: ex b being set st f is b -limited take b = sup (dom f); ::_thesis: f is b -limited thus f is b -limited by Def3; ::_thesis: verum end; assume for a being ordinal number holds not a in dom f ; ::_thesis: ex b1 being ordinal number st b1 = 0 take 0 ; ::_thesis: 0 = 0 thus 0 = 0 ; ::_thesis: verum 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 let b, c be ordinal number ; ::_thesis: ( ( ex a being ordinal number st a in dom f & f is b -limited & f is c -limited implies b = c ) & ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) ) hereby ::_thesis: ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) given a being ordinal number such that a in dom f ; ::_thesis: ( f is b -limited & f is c -limited implies b = c ) assume A3: ( f is b -limited & f is c -limited ) ; ::_thesis: b = c thus b = sup (dom f) by A3, Def3 .= c by A3, Def3 ; ::_thesis: verum end; thus ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) ; ::_thesis: verum end; 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 ) proof for a being ordinal number holds not a in dom {} ; hence ( base- {} = 0 & limit- {} = 0 ) by Def4, Def5; ::_thesis: len- {} = 0 hence len- {} = 0 by ORDINAL3:56; ::_thesis: verum end; theorem Th16: :: EXCHSORT:16 for f being Function holds limit- f = sup (dom f) proof let f be Function; ::_thesis: limit- f = sup (dom f) percases ( for a being ordinal number holds a nin dom f or ex a being ordinal number st a in dom f ) ; supposeA1: for a being ordinal number holds a nin dom f ; ::_thesis: limit- f = sup (dom f) On (dom f) c= 0 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On (dom f) or x in 0 ) assume x in On (dom f) ; ::_thesis: x in 0 then ( x in dom f & x is ordinal ) by ORDINAL1:def_9; hence x in 0 by A1; ::_thesis: verum end; then sup (dom f) c= 0 by ORDINAL2:def_3; then sup (dom f) = 0 ; hence limit- f = sup (dom f) by A1, Def5; ::_thesis: verum end; supposeA2: ex a being ordinal number st a in dom f ; ::_thesis: limit- f = sup (dom f) f is sup (dom f) -limited by Def3; hence limit- f = sup (dom f) by A2, Def5; ::_thesis: verum end; end; end; theorem :: EXCHSORT:17 for f being Function holds f is limit- f -limited proof let f be Function; ::_thesis: f is limit- f -limited limit- f = sup (dom f) by Th16; hence f is limit- f -limited by Def3; ::_thesis: verum end; theorem Th18: :: EXCHSORT:18 for a being ordinal number for A being empty set holds A is a -based proof let a be ordinal number ; ::_thesis: for A being empty set holds A is a -based let A be empty set ; ::_thesis: A is a -based let b be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( b in proj1 A implies ( a in proj1 A & a c= b ) ) thus ( b in proj1 A implies ( a in proj1 A & a c= b ) ) ; ::_thesis: verum 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 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 ) proof take A = {} [:Y,X:]; ::_thesis: ( A is Y -defined & A is X -valued & A is a -based & A is segmental & A is finite & A is empty ) thus ( A is Y -defined & A is X -valued & A is a -based & A is segmental & A is finite & A is empty ) by Th18; ::_thesis: verum 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 consider a, b being ordinal number such that A1: dom A = a \ b by Def1; take a ; :: according to ORDINAL6:def_1 ::_thesis: dom A c= a thus dom A c= a by A1; ::_thesis: verum end; end; theorem :: EXCHSORT:19 for f being array holds ( f is 0 -limited iff f is empty ) proof let f be array; ::_thesis: ( f is 0 -limited iff f is empty ) thus ( f is 0 -limited implies f is empty ) ::_thesis: ( f is empty implies f is 0 -limited ) proof assume sup (dom f) = 0 ; :: according to EXCHSORT:def_3 ::_thesis: f is empty then dom f c= 0 by ORDINAL6:3; hence f is empty ; ::_thesis: verum end; assume f is empty ; ::_thesis: f is 0 -limited hence sup (dom f) = 0 by ORDINAL2:18; :: according to EXCHSORT:def_3 ::_thesis: verum end; 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 proof let s be array; ::_thesis: ( s is 0 -based implies s is T-Sequence-like ) assume A1: for b being ordinal number st b in proj1 s holds ( 0 in proj1 s & 0 c= b ) ; :: according to EXCHSORT:def_2 ::_thesis: s is T-Sequence-like consider c, a being ordinal number such that A2: dom s = c \ a by Def1; set x = the Element of c \ a; now__::_thesis:_(_c_\_a_<>_{}_implies_dom_s_=_c_) assume A3: c \ a <> {} ; ::_thesis: dom s = c then the Element of c \ a in c by XBOOLE_0:def_5; then 0 in dom s by A1, A2, A3; then 0 nin a by A2, XBOOLE_0:def_5; then a c= 0 by ORDINAL6:4; then a = 0 ; hence dom s = c by A2; ::_thesis: verum end; hence dom s is ordinal by A2; :: according to ORDINAL1:def_7 ::_thesis: verum 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 Th20: :: EXCHSORT:20 for f being Function holds base- f = inf (dom f) proof let f be Function; ::_thesis: base- f = inf (dom f) set A = f; set b = inf (dom f); A1: f is inf (dom f) -based by Th12; percases ( ex a being ordinal number st a in dom f or for a being ordinal number holds not a in dom f ) ; suppose ex a being ordinal number st a in dom f ; ::_thesis: base- f = inf (dom f) hence base- f = inf (dom f) by A1, Def4; ::_thesis: verum end; supposeA2: for a being ordinal number holds not a in dom f ; ::_thesis: base- f = inf (dom f) set x = the Element of On (dom f); now__::_thesis:_not_On_(dom_f)_<>_{} assume On (dom f) <> {} ; ::_thesis: contradiction then the Element of On (dom f) in dom f by ORDINAL1:def_9; hence contradiction by A2; ::_thesis: verum end; then inf (dom f) = 0 by SETFAM_1:def_1; hence base- f = inf (dom f) by A2, Def4; ::_thesis: verum end; end; end; theorem :: EXCHSORT:21 for f being Function holds f is base- f -based proof let f be Function; ::_thesis: f is base- f -based base- f = inf (dom f) by Th20; hence f is base- f -based by Th12; ::_thesis: verum end; theorem :: EXCHSORT:22 for A being array holds dom A = (limit- A) \ (base- A) proof let A be array; ::_thesis: dom A = (limit- A) \ (base- A) consider a, b being ordinal number such that A1: dom A = a \ b by Def1; A2: limit- A = sup (dom A) by Th16; A3: base- A = inf (dom A) by Th20; thus dom A c= (limit- A) \ (base- A) :: according to XBOOLE_0:def_10 ::_thesis: (limit- A) \ (base- A) c= dom A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom A or x in (limit- A) \ (base- A) ) assume x in dom A ; ::_thesis: x in (limit- A) \ (base- A) then A4: ( base- A c= x & x in limit- A ) by A2, A3, ORDINAL2:14, ORDINAL2:19; then ( x in base- A implies x in x ) ; hence x in (limit- A) \ (base- A) by A4, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (limit- A) \ (base- A) or x in dom A ) assume A5: x in (limit- A) \ (base- A) ; ::_thesis: x in dom A then reconsider x = x as Ordinal ; ex c being ordinal number st ( c in dom A & x c= c ) by A2, A5, ORDINAL2:21; then ( a = limit- A & b = base- A ) by A1, A2, A3, Th6; hence x in dom A by A1, A5; ::_thesis: verum end; 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 ) proof let a, b be ordinal number ; ::_thesis: for A being array st dom A = a \ b & not A is empty holds ( base- A = b & limit- A = a ) let A be array; ::_thesis: ( dom A = a \ b & not A is empty implies ( base- A = b & limit- A = a ) ) assume A1: ( dom A = a \ b & not A is empty ) ; ::_thesis: ( base- A = b & limit- A = a ) set x = the Element of dom A; dom A <> {} by A1; then A2: the Element of dom A in a \ b by A1; ( b c= the Element of dom A & the Element of dom A in a ) by A1, ORDINAL6:5; then A3: ( b in a & b nin b ) by ORDINAL1:12; then b in a \ b by XBOOLE_0:def_5; then A4: b in sup (dom A) by A1, ORDINAL2:19; A is b -based proof let c be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( c in proj1 A implies ( b in proj1 A & b c= c ) ) thus ( c in proj1 A implies ( b in proj1 A & b c= c ) ) by A1, A3, ORDINAL6:5; ::_thesis: verum end; hence base- A = b by Def4, A1, A2; ::_thesis: limit- A = a A5: a c= sup (dom A) proof let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in a or x in sup (dom A) ) assume A6: x in a ; ::_thesis: x in sup (dom A) percases ( x in b or x nin b ) ; suppose x in b ; ::_thesis: x in sup (dom A) hence x in sup (dom A) by A4, ORDINAL1:10; ::_thesis: verum end; suppose x nin b ; ::_thesis: x in sup (dom A) then x in a \ b by A6, XBOOLE_0:def_5; hence x in sup (dom A) by A1, ORDINAL2:19; ::_thesis: verum end; end; end; sup (dom A) c= sup a by A1, ORDINAL2:22; then sup (dom A) c= a by ORDINAL2:18; then a = sup (dom A) by A5, XBOOLE_0:def_10; hence limit- A = a by Th16; ::_thesis: verum end; theorem Th24: :: EXCHSORT:24 for f being T-Sequence holds ( base- f = 0 & limit- f = dom f & len- f = dom f ) proof let f be T-Sequence; ::_thesis: ( base- f = 0 & limit- f = dom f & len- f = dom f ) percases ( f = {} or f <> {} ) ; suppose f = {} ; ::_thesis: ( base- f = 0 & limit- f = dom f & len- f = dom f ) hence ( base- f = 0 & limit- f = dom f & len- f = dom f ) by Th15; ::_thesis: verum end; supposeA1: f <> {} ; ::_thesis: ( base- f = 0 & limit- f = dom f & len- f = dom f ) (dom f) \ 0 = dom f ; hence ( base- f = 0 & limit- f = dom f ) by A1, Th23; ::_thesis: len- f = dom f hence len- f = dom f by ORDINAL3:56; ::_thesis: verum end; end; end; 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 ) proof set A = the empty array of a,X; take the empty array of a,X ; ::_thesis: ( the empty array of a,X is b -based & the empty array of a,X is natural-valued & the empty array of a,X is INT -valued & the empty array of a,X is real-valued & the empty array of a,X is complex-valued & the empty array of a,X is finite ) thus ( the empty array of a,X is b -based & the empty array of a,X is natural-valued & the empty array of a,X is INT -valued & the empty array of a,X is real-valued & the empty array of a,X is complex-valued & the empty array of a,X is finite ) by Th18; ::_thesis: verum end; end; registration let a be ordinal number ; let x be set ; cluster{[a,x]} -> segmental ; coherence {[a,x]} is segmental proof take succ a ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 {[a,x]} = (succ a) \ b take a ; ::_thesis: proj1 {[a,x]} = (succ a) \ a thus dom {[a,x]} = {a} by FUNCT_5:12 .= (succ a) \ a by Th4 ; ::_thesis: verum end; 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 proof let A be array; ::_thesis: ( A = {[a,x]} implies A is natural-valued ) assume A = {[a,x]} ; ::_thesis: A is natural-valued then rng A = {x} by FUNCT_5:12; then rng A c= NAT by MEMBERED:6; hence A is natural-valued by VALUED_0:def_6; ::_thesis: verum end; 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 proof let A be array; ::_thesis: ( A = {[a,x]} implies A is real-valued ) assume A = {[a,x]} ; ::_thesis: A is real-valued then rng A = {x} by FUNCT_5:12; then rng A c= REAL by MEMBERED:3; hence A is real-valued by VALUED_0:def_3; ::_thesis: verum 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 for array; coherence for b1 being array st b1 = {[a,x]} holds b1 is X -valued proof let A be array; ::_thesis: ( A = {[a,x]} implies A is X -valued ) assume A = {[a,x]} ; ::_thesis: A is X -valued then rng A = {x} by FUNCT_5:12; hence rng A c= X by ZFMISC_1:31; :: according to RELAT_1:def_19 ::_thesis: verum end; 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 ) proof let s be array; ::_thesis: ( s = {[a,x]} implies ( s is a -based & s is succ a -limited ) ) assume A1: s = {[a,x]} ; ::_thesis: ( s is a -based & s is succ a -limited ) A2: dom s = {a} by A1, FUNCT_5:12; thus s is a -based ::_thesis: s is succ a -limited proof let b be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( b in proj1 s implies ( a in proj1 s & a c= b ) ) assume A3: b in proj1 s ; ::_thesis: ( a in proj1 s & a c= b ) thus ( a in proj1 s & a c= b ) by A3, A2, TARSKI:def_1; ::_thesis: verum end; sup (dom s) = succ a by A2, ORDINAL2:23; hence s is succ a -limited by Def3; ::_thesis: verum end; 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 ) proof set x = the Nat; reconsider A = {[b, the Nat]} as natural-valued array ; take A ; ::_thesis: ( not A is empty & A is b -based & A is natural-valued & A is INT -valued & A is real-valued & A is complex-valued & A is finite ) thus ( not A is empty & A is b -based & A is natural-valued & A is INT -valued & A is real-valued & A is complex-valued & A is finite ) ; ::_thesis: verum end; 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 ) proof set x = the Element of X; reconsider A = {[b, the Element of X]} as array of X ; take A ; ::_thesis: ( not A is empty & A is b -based & A is finite & A is X -valued ) thus ( not A is empty & A is b -based & A is finite & A is X -valued ) ; ::_thesis: verum 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; 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 proof let f be finite array; ::_thesis: ( ( for a being ordinal number st a in dom f & succ a in dom f holds f . (succ a) c< f . a ) implies f is descending ) assume A1: for a being ordinal number st a in dom f & succ a in dom f holds f . (succ a) c< f . a ; ::_thesis: f is descending let a be ordinal number ; :: according to EXCHSORT:def_8 ::_thesis: for b being ordinal number st a in dom f & b in dom f & a in b holds f . b c< f . a let b be ordinal number ; ::_thesis: ( a in dom f & b in dom f & a in b implies f . b c< f . a ) assume A2: ( a in dom f & b in dom f & a in b ) ; ::_thesis: f . b c< f . a consider c, d being ordinal number such that A3: dom f = c \ d by Def1; consider n being Nat such that A4: c = d +^ n by A2, A3, Th7; consider e1 being Ordinal such that A5: ( a = d +^ e1 & e1 in n ) by A2, A3, A4, Th1; consider e2 being Ordinal such that A6: ( b = d +^ e2 & e2 in n ) by A2, A3, A4, Th1; reconsider e1 = e1, e2 = e2 as Nat by A5, A6; reconsider se1 = succ e1 as Element of NAT by ORDINAL1:def_12; A7: succ a = d +^ (succ e1) by A5, ORDINAL2:28; e1 in e2 by A2, A5, A6, ORDINAL3:22; then succ e1 c= e2 by ORDINAL1:21; then succ e1 <= e2 by NAT_1:39; then consider k being Nat such that A8: e2 = se1 + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; deffunc H1( Ordinal) -> set = (succ a) +^ \$1; defpred S9[ Nat] means ( H1(\$1) in dom f implies f . H1(\$1) c< f . a ); H1( 0 ) = succ a by ORDINAL2:27; then A9: S9[ 0 ] by A1, A2; A10: for k being Nat st S9[k] holds S9[k + 1] proof let k be Nat; ::_thesis: ( S9[k] implies S9[k + 1] ) k + 1 = succ k by NAT_1:38; then A11: H1(k + 1) = succ H1(k) by ORDINAL2:28; then A12: ( H1(k) in H1(k + 1) & a in succ a ) by ORDINAL1:6; then A13: ( H1(k) c= H1(k + 1) & a c= succ a ) by ORDINAL1:def_2; succ a c= H1(k) by ORDINAL3:24; then A14: a c= H1(k) by A12, ORDINAL1:def_2; assume A15: ( S9[k] & H1(k + 1) in dom f ) ; ::_thesis: f . H1(k + 1) c< f . a then H1(k) in dom f by A2, A13, A14, Th9; then ( f . H1(k) c< f . a & f . H1(k + 1) c< f . H1(k) ) by A1, A11, A15; hence f . H1(k + 1) c< f . a by XBOOLE_1:56; ::_thesis: verum end; A16: for k being Nat holds S9[k] from NAT_1:sch_2(A9, A10); b = d +^ (se1 +^ k) by A6, A8, CARD_2:36 .= (succ a) +^ k by A7, ORDINAL3:30 ; hence f . b c< f . a by A2, A16; ::_thesis: verum end; 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 proof let f be array; ::_thesis: ( 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 ) implies f is descending ) assume A1: len- f = omega ; ::_thesis: ( ex a being ordinal number st ( a in dom f & succ a in dom f & not f . (succ a) c< f . a ) or f is descending ) assume A2: for a being ordinal number st a in dom f & succ a in dom f holds f . (succ a) c< f . a ; ::_thesis: f is descending let a be ordinal number ; :: according to EXCHSORT:def_8 ::_thesis: for b being ordinal number st a in dom f & b in dom f & a in b holds f . b c< f . a let b be ordinal number ; ::_thesis: ( a in dom f & b in dom f & a in b implies f . b c< f . a ) assume A3: ( a in dom f & b in dom f & a in b ) ; ::_thesis: f . b c< f . a consider c, d being ordinal number such that A4: dom f = c \ d by Def1; not f is empty by A3; then A5: ( base- f = d & limit- f = c ) by A4, Th23; ( d c= a & a in c ) by A3, A4, ORDINAL6:5; then d in c by ORDINAL1:12; then d c= c by ORDINAL1:def_2; then A6: c = d +^ omega by A5, A1, ORDINAL3:def_5; consider e1 being Ordinal such that A7: ( a = d +^ e1 & e1 in omega ) by A3, A4, A6, Th1; consider e2 being Ordinal such that A8: ( b = d +^ e2 & e2 in omega ) by A3, A4, A6, Th1; reconsider e1 = e1, e2 = e2 as Nat by A7, A8; reconsider se1 = succ e1 as Element of NAT by ORDINAL1:def_12; A9: succ a = d +^ (succ e1) by A7, ORDINAL2:28; e1 in e2 by A3, A7, A8, ORDINAL3:22; then succ e1 c= e2 by ORDINAL1:21; then succ e1 <= e2 by NAT_1:39; then consider k being Nat such that A10: e2 = se1 + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; deffunc H1( Ordinal) -> set = (succ a) +^ \$1; defpred S9[ Nat] means ( H1(\$1) in dom f implies f . H1(\$1) c< f . a ); H1( 0 ) = succ a by ORDINAL2:27; then A11: S9[ 0 ] by A2, A3; A12: for k being Nat st S9[k] holds S9[k + 1] proof let k be Nat; ::_thesis: ( S9[k] implies S9[k + 1] ) k + 1 = succ k by NAT_1:38; then A13: H1(k + 1) = succ H1(k) by ORDINAL2:28; then A14: ( H1(k) in H1(k + 1) & a in succ a ) by ORDINAL1:6; then A15: ( H1(k) c= H1(k + 1) & a c= succ a ) by ORDINAL1:def_2; succ a c= H1(k) by ORDINAL3:24; then A16: a c= H1(k) by A14, ORDINAL1:def_2; assume A17: ( S9[k] & H1(k + 1) in dom f ) ; ::_thesis: f . H1(k + 1) c< f . a then H1(k) in dom f by A3, A15, A16, Th9; then ( f . H1(k) c< f . a & f . H1(k + 1) c< f . H1(k) ) by A2, A13, A17; hence f . H1(k + 1) c< f . a by XBOOLE_1:56; ::_thesis: verum end; A18: for k being Nat holds S9[k] from NAT_1:sch_2(A11, A12); b = d +^ (se1 +^ k) by A8, A10, CARD_2:36 .= (succ a) +^ k by A9, ORDINAL3:30 ; hence f . b c< f . a by A3, A18; ::_thesis: verum end; theorem Th27: :: EXCHSORT:27 for f being T-Sequence st f is descending & f . 0 is finite holds f is finite proof let f be T-Sequence; ::_thesis: ( f is descending & f . 0 is finite implies f is finite ) assume A1: f is descending ; ::_thesis: ( not f . 0 is finite or f is finite ) assume A2: f . 0 is finite ; ::_thesis: f is finite deffunc H1( set ) -> set = card (f . \$1); consider g being T-Sequence such that A3: ( dom g = dom f & ( for a being ordinal number st a in dom f holds g . a = H1(a) ) ) from ORDINAL2:sch_2(); defpred S9[ set ] means f . \$1 is finite ; A4: S9[ {} ] by A2; A5: for a being ordinal number st S9[a] holds S9[ succ a] proof let a be ordinal number ; ::_thesis: ( S9[a] implies S9[ succ a] ) percases ( succ a nin dom f or succ a in dom f ) ; suppose succ a nin dom f ; ::_thesis: ( S9[a] implies S9[ succ a] ) hence ( S9[a] implies S9[ succ a] ) by FUNCT_1:def_2; ::_thesis: verum end; supposeA6: succ a in dom f ; ::_thesis: ( S9[a] implies S9[ succ a] ) A7: a in succ a by ORDINAL1:6; then a in dom f by A6, ORDINAL1:10; then f . (succ a) c< f . a by A1, A6, A7, Def8; then f . (succ a) c= f . a by XBOOLE_0:def_8; hence ( S9[a] implies S9[ succ a] ) ; ::_thesis: verum end; end; end; A8: for a being ordinal number st a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds S9[b] ) holds S9[a] proof let a be ordinal number ; ::_thesis: ( a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds S9[b] ) implies S9[a] ) assume a <> {} ; ::_thesis: ( not a is limit_ordinal or ex b being ordinal number st ( b in a & not S9[b] ) or S9[a] ) then A9: 0 in a by ORDINAL3:8; percases ( a in dom f or a nin dom f ) ; suppose a in dom f ; ::_thesis: ( not a is limit_ordinal or ex b being ordinal number st ( b in a & not S9[b] ) or S9[a] ) then ( 0 in dom f & a in dom f ) by ORDINAL3:8; then f . a c< f . 0 by A1, A9, Def8; then f . a c= f . 0 by XBOOLE_0:def_8; hence ( not a is limit_ordinal or ex b being ordinal number st ( b in a & not S9[b] ) or S9[a] ) by A2; ::_thesis: verum end; suppose a nin dom f ; ::_thesis: ( not a is limit_ordinal or ex b being ordinal number st ( b in a & not S9[b] ) or S9[a] ) hence ( not a is limit_ordinal or ex b being ordinal number st ( b in a & not S9[b] ) or S9[a] ) by FUNCT_1:def_2; ::_thesis: verum end; end; end; A10: for a being ordinal number holds S9[a] from ORDINAL2:sch_1(A4, A5, A8); g is decreasing proof let a be ordinal number ; :: according to ORDINAL5:def_1 ::_thesis: for b1 being set holds ( not a in b1 or not b1 in proj1 g or g . b1 in g . a ) let b be ordinal number ; ::_thesis: ( not a in b or not b in proj1 g or g . b in g . a ) assume A11: ( a in b & b in dom g ) ; ::_thesis: g . b in g . a then a in dom f by A3, ORDINAL1:10; then ( g . a = H1(a) & f . a is finite & f . b c< f . a & g . b = H1(b) & f . b is finite ) by A1, A3, A11, A10, Def8; hence g . b in g . a by CARD_2:48; ::_thesis: verum end; hence f is finite by A3, FINSET_1:10; ::_thesis: verum 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 let f be T-Sequence; ::_thesis: ( f is descending & f . 0 is finite & ( for a being ordinal number st f . a <> {} holds succ a in dom f ) implies last f = {} ) assume that A1: ( f is descending & f . 0 is finite ) and A2: for a being ordinal number st f . a <> {} holds succ a in dom f ; ::_thesis: last f = {} f is finite by A1, Th27; then reconsider d = dom f as finite Ordinal ; set u = union d; percases ( d = 0 or d <> 0 ) ; suppose d = 0 ; ::_thesis: last f = {} hence last f = {} by FUNCT_1:def_2; ::_thesis: verum end; suppose d <> 0 ; ::_thesis: last f = {} then consider n being Nat such that A3: d = n + 1 by NAT_1:6; A4: d = succ n by A3, NAT_1:38; then A5: union d = n by ORDINAL2:2; ( f . (union d) <> 0 implies d in d ) by A2, A4, A5; hence last f = {} ; ::_thesis: verum end; end; end; 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)) proof deffunc H1( set ) -> set = F2((F1() . \$1)); consider F being T-Sequence such that A3: ( dom F = dom F1() & ( for a being ordinal number st a in dom F1() holds F . a = H1(a) ) ) from ORDINAL2:sch_2(); percases ( dom F in omega or omega c= dom F ) by ORDINAL6:4; suppose dom F in omega ; ::_thesis: F1() is finite hence F1() is finite by A3, FINSET_1:10; ::_thesis: verum end; supposeA4: omega c= dom F ; ::_thesis: F1() is finite set f = F | omega; A5: dom (F | omega) = omega by A4, RELAT_1:62; A6: len- (F | omega) = dom (F | omega) by Th24; A7: 0 in omega by ORDINAL1:def_11; A8: (F | omega) . 0 = F . 0 by A7, A5, FUNCT_1:47 .= H1( 0 ) by A3, A7, A4 ; defpred S9[ Nat] means (F | omega) . \$1 is finite ; A9: S9[ 0 ] by A1, A8; A10: for n being Nat st S9[n] holds S9[n + 1] proof let n be Nat; ::_thesis: ( S9[n] implies S9[n + 1] ) set a = n; assume A11: S9[n] ; ::_thesis: S9[n + 1] A12: ( n in omega & succ n in omega ) by ORDINAL1:def_12; then A13: ( n in dom F & succ n in dom F & (F | omega) . n = F . n & (F | omega) . (succ n) = F . (succ n) ) by A4, A5, FUNCT_1:47; ( F . n = H1(n) & F . (succ n) = H1( succ n) ) by A3, A4, A12; then (F | omega) . (succ n) c< (F | omega) . n by A2, A3, A11, A13; then (F | omega) . (succ n) c= (F | omega) . n by XBOOLE_0:def_8; hence S9[n + 1] by A11, NAT_1:38; ::_thesis: verum end; A14: for n being Nat holds S9[n] from NAT_1:sch_2(A9, A10); for a being ordinal number st a in dom (F | omega) & succ a in dom (F | omega) holds (F | omega) . (succ a) c< (F | omega) . a proof let a be ordinal number ; ::_thesis: ( a in dom (F | omega) & succ a in dom (F | omega) implies (F | omega) . (succ a) c< (F | omega) . a ) assume A15: ( a in dom (F | omega) & succ a in dom (F | omega) ) ; ::_thesis: (F | omega) . (succ a) c< (F | omega) . a then reconsider n = a as Nat by A5; A16: ( S9[n] & (F | omega) . a = F . a & (F | omega) . (succ a) = F . (succ a) ) by A15, A14, FUNCT_1:47; ( F . a = H1(a) & F . (succ a) = H1( succ a) ) by A3, A15, A4, A5; hence (F | omega) . (succ a) c< (F | omega) . a by A2, A3, A16, A15, A4, A5; ::_thesis: verum end; then F | omega is descending by A6, Th26, A4, RELAT_1:62; then F | omega is finite by A1, A8, Th27; hence F1() is finite by A5; ::_thesis: verum end; end; 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 dom (Swap (f,a,b)) = dom f by FUNCT_7:99; hence dom (Swap (f,a,b)) c= X ; :: according to RELAT_1:def_18 ::_thesis: verum 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 rng (Swap (f,x,y)) = rng f by FUNCT_7:103; hence rng (Swap (f,x,y)) c= X by RELAT_1:def_19; :: according to RELAT_1:def_19 ::_thesis: verum 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 let x, y be set ; ::_thesis: for f being Function st x in dom f & y in dom f holds (Swap (f,x,y)) . x = f . y let f be Function; ::_thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) . x = f . y ) assume A1: ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) . x = f . y then A2: Swap (f,x,y) = (f +* (x,(f . y))) +* (y,(f . x)) by FUNCT_7:def_12; A3: dom f = dom (f +* (x,(f . y))) by FUNCT_7:30; now__::_thesis:_(_x_<>_y_implies_(Swap_(f,x,y))_._x_=_f_._y_) assume x <> y ; ::_thesis: (Swap (f,x,y)) . x = f . y then (Swap (f,x,y)) . x = (f +* (x,(f . y))) . x by A2, FUNCT_7:32; hence (Swap (f,x,y)) . x = f . y by A1, FUNCT_7:31; ::_thesis: verum end; hence (Swap (f,x,y)) . x = f . y by A3, A1, A2, FUNCT_7:31; ::_thesis: verum end; 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 proof let X, x, y be set ; ::_thesis: for f being array of X st x in dom f & y in dom f holds (Swap (f,x,y)) /. x = f /. y let f be array of X; ::_thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) /. x = f /. y ) assume A1: ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) /. x = f /. y dom (Swap (f,x,y)) = dom f by FUNCT_7:99; hence (Swap (f,x,y)) /. x = (Swap (f,x,y)) . x by A1, PARTFUN1:def_6 .= f . y by A1, Th29 .= f /. y by A1, PARTFUN1:def_6 ; ::_thesis: verum 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 let x, y be set ; ::_thesis: for f being Function st x in dom f & y in dom f holds (Swap (f,x,y)) . y = f . x let f be Function; ::_thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) . y = f . x ) assume A1: ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) . y = f . x then A2: Swap (f,x,y) = (f +* (x,(f . y))) +* (y,(f . x)) by FUNCT_7:def_12; dom f = dom (f +* (x,(f . y))) by FUNCT_7:30; hence (Swap (f,x,y)) . y = f . x by A1, A2, FUNCT_7:31; ::_thesis: verum end; 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 proof let X, x, y be set ; ::_thesis: for f being array of X st x in dom f & y in dom f holds (Swap (f,x,y)) /. y = f /. x let f be array of X; ::_thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) /. y = f /. x ) assume A1: ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) /. y = f /. x dom (Swap (f,x,y)) = dom f by FUNCT_7:99; hence (Swap (f,x,y)) /. y = (Swap (f,x,y)) . y by A1, PARTFUN1:def_6 .= f . x by A1, Th31 .= f /. x by A1, PARTFUN1:def_6 ; ::_thesis: verum end; 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 proof let z, x, y be set ; ::_thesis: for f being Function st z <> x & z <> y holds (Swap (f,x,y)) . z = f . z let f be Function; ::_thesis: ( z <> x & z <> y implies (Swap (f,x,y)) . z = f . z ) assume A1: ( z <> x & z <> y ) ; ::_thesis: (Swap (f,x,y)) . z = f . z percases ( ( x in dom f & y in dom f ) or not x in dom f or not y in dom f ) ; suppose ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) . z = f . z then Swap (f,x,y) = (f +* (x,(f . y))) +* (y,(f . x)) by FUNCT_7:def_12; hence (Swap (f,x,y)) . z = (f +* (x,(f . y))) . z by A1, FUNCT_7:32 .= f . z by A1, FUNCT_7:32 ; ::_thesis: verum end; suppose ( not x in dom f or not y in dom f ) ; ::_thesis: (Swap (f,x,y)) . z = f . z hence (Swap (f,x,y)) . z = f . z by FUNCT_7:def_12; ::_thesis: verum end; end; end; 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 proof let X, z, x, y be set ; ::_thesis: for f being array of X st z in dom f & z <> x & z <> y holds (Swap (f,x,y)) /. z = f /. z let f be array of X; ::_thesis: ( z in dom f & z <> x & z <> y implies (Swap (f,x,y)) /. z = f /. z ) assume A1: ( z in dom f & z <> x & z <> y ) ; ::_thesis: (Swap (f,x,y)) /. z = f /. z dom (Swap (f,x,y)) = dom f by FUNCT_7:99; hence (Swap (f,x,y)) /. z = (Swap (f,x,y)) . z by A1, PARTFUN1:def_6 .= f . z by A1, Th33 .= f /. z by A1, PARTFUN1:def_6 ; ::_thesis: verum 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 let x, y be set ; ::_thesis: for f being Function st x in dom f & y in dom f holds Swap (f,x,y) = Swap (f,y,x) let f be Function; ::_thesis: ( x in dom f & y in dom f implies Swap (f,x,y) = Swap (f,y,x) ) assume A1: ( x in dom f & y in dom f ) ; ::_thesis: Swap (f,x,y) = Swap (f,y,x) A2: ( dom (Swap (f,x,y)) = dom f & dom (Swap (f,y,x)) = dom f ) by FUNCT_7:99; now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_ (Swap_(f,x,y))_._z_=_(Swap_(f,y,x))_._z let z be set ; ::_thesis: ( z in dom f implies (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1 ) assume z in dom f ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1 percases ( ( z = x & z = y ) or ( z = x & z <> y ) or ( z <> x & z = y ) or ( z <> x & z <> y ) ) ; suppose ( z = x & z = y ) ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1 hence (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; ::_thesis: verum end; suppose ( z = x & z <> y ) ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1 then ( (Swap (f,x,y)) . z = f . y & (Swap (f,y,x)) . z = f . y ) by A1, Th29, Th31; hence (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; ::_thesis: verum end; suppose ( z <> x & z = y ) ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1 then ( (Swap (f,x,y)) . z = f . x & (Swap (f,y,x)) . z = f . x ) by A1, Th29, Th31; hence (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; ::_thesis: verum end; suppose ( z <> x & z <> y ) ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1 then ( (Swap (f,x,y)) . z = f . z & (Swap (f,y,x)) . z = f . z ) by Th33; hence (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; ::_thesis: verum end; end; end; hence Swap (f,x,y) = Swap (f,y,x) by A2, FUNCT_1:2; ::_thesis: verum end; 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 proof take id X ; ::_thesis: id X is onto thus id X is onto ; ::_thesis: verum 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 rng (Swap (f,x,y)) = rng f by FUNCT_7:103; hence rng (Swap (f,x,y)) = X by FUNCT_2:def_3; :: according to FUNCT_2:def_3 ::_thesis: verum 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 consider a1, a2 being ordinal number such that A1: dom A = a1 \ a2 by Def1; take a1 ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 (Swap (A,x,y)) = a1 \ b take a2 ; ::_thesis: proj1 (Swap (A,x,y)) = a1 \ a2 thus proj1 (Swap (A,x,y)) = a1 \ a2 by A1, FUNCT_7:99; ::_thesis: verum 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 let x, y be set ; ::_thesis: for A being array st x in dom A & y in dom A holds Swap ((Swap (A,x,y)),x,y) = A let A be array; ::_thesis: ( x in dom A & y in dom A implies Swap ((Swap (A,x,y)),x,y) = A ) assume A1: ( x in dom A & y in dom A ) ; ::_thesis: Swap ((Swap (A,x,y)),x,y) = A set B = Swap (A,x,y); set C = Swap ((Swap (A,x,y)),x,y); A2: ( dom (Swap ((Swap (A,x,y)),x,y)) = dom (Swap (A,x,y)) & dom (Swap (A,x,y)) = dom A ) by FUNCT_7:99; now__::_thesis:_for_z_being_set_st_z_in_dom_(Swap_(A,x,y))_holds_ (Swap_((Swap_(A,x,y)),x,y))_._z_=_A_._z let z be set ; ::_thesis: ( z in dom (Swap (A,x,y)) implies (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1 ) assume z in dom (Swap (A,x,y)) ; ::_thesis: (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1 percases ( ( z <> x & z <> y ) or z = x or z = y ) ; supposeA3: ( z <> x & z <> y ) ; ::_thesis: (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1 hence (Swap ((Swap (A,x,y)),x,y)) . z = (Swap (A,x,y)) . z by Th33 .= A . z by A3, Th33 ; ::_thesis: verum end; supposeA4: z = x ; ::_thesis: (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1 hence (Swap ((Swap (A,x,y)),x,y)) . z = (Swap (A,x,y)) . y by A1, A2, Th29 .= A . z by A1, A4, Th31 ; ::_thesis: verum end; supposeA5: z = y ; ::_thesis: (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1 hence (Swap ((Swap (A,x,y)),x,y)) . z = (Swap (A,x,y)) . x by A1, A2, Th31 .= A . z by A1, A5, Th29 ; ::_thesis: verum end; end; end; hence Swap ((Swap (A,x,y)),x,y) = A by A2, FUNCT_1:2; ::_thesis: verum end; 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 proof let B be array; ::_thesis: ( B = Swap (A,x,y) implies B is real-valued ) assume A1: B = Swap (A,x,y) ; ::_thesis: B is real-valued let z be set ; :: according to VALUED_0:def_9 ::_thesis: ( not z in proj1 B or B . z is real ) assume z in dom B ; ::_thesis: B . z is real then A2: ( z in dom A & ( x = z or x <> z ) & ( y = z or y <> z ) ) by A1, FUNCT_7:99; ( ( not x in dom A or not y in dom A ) implies B = A ) by A1, FUNCT_7:def_12; then ( B . z = A . y or B . z = A . x or B . z = A . z ) by A1, A2, Th29, Th31, Th33; hence B . z is real ; ::_thesis: verum end; 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 proof take A ; ::_thesis: ex f being Permutation of (dom A) st A = A * f take id (dom A) ; ::_thesis: A = A * (id (dom A)) thus A = A * (id (dom A)) by RELAT_1:51; ::_thesis: verum end; 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 ) proof let A be array; ::_thesis: for B being permutation of A holds ( dom B = dom A & rng B = rng A ) let B be permutation of A; ::_thesis: ( dom B = dom A & rng B = rng A ) consider f being Permutation of (dom A) such that A1: B = A * f by Def9; ( dom A <> {} implies dom A <> {} ) ; then ( rng f = dom A & dom f = dom A ) by FUNCT_2:def_1, FUNCT_2:def_3; hence ( dom B = dom A & rng B = rng A ) by A1, RELAT_1:27, RELAT_1:28; ::_thesis: verum end; theorem Th38: :: EXCHSORT:38 for A being array holds A is permutation of A proof let A be array; ::_thesis: A is permutation of A take id (dom A) ; :: according to EXCHSORT:def_9 ::_thesis: A = A * (id (dom A)) thus A = A * (id (dom A)) by RELAT_1:51; ::_thesis: verum end; theorem Th39: :: EXCHSORT:39 for A, B being array st A is permutation of B holds B is permutation of A proof let A, B be array; ::_thesis: ( A is permutation of B implies B is permutation of A ) assume A1: A is permutation of B ; ::_thesis: B is permutation of A then A2: dom A = dom B by Th37; consider f being Permutation of (dom B) such that A3: A = B * f by A1, Def9; reconsider g = f " as Permutation of (dom A) by A2; take g ; :: according to EXCHSORT:def_9 ::_thesis: B = A * g thus B = B * (id (dom B)) by RELAT_1:52 .= B * (f * g) by FUNCT_2:61 .= A * g by A3, RELAT_1:36 ; ::_thesis: verum 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 let A, B, C be array; ::_thesis: ( A is permutation of B & B is permutation of C implies A is permutation of C ) assume A1: ( A is permutation of B & B is permutation of C ) ; ::_thesis: A is permutation of C then A2: dom C = dom B by Th37; consider f being Permutation of (dom B) such that A3: A = B * f by A1, Def9; consider g being Permutation of (dom C) such that A4: B = C * g by A1, Def9; reconsider h = g * f as Permutation of (dom C) by A2; take h ; :: according to EXCHSORT:def_9 ::_thesis: A = C * h thus A = C * h by A3, A4, RELAT_1:36; ::_thesis: verum end; theorem Th41: :: EXCHSORT:41 for X, x, y being set holds Swap ((id X),x,y) is one-to-one proof let X, x, y be set ; ::_thesis: Swap ((id X),x,y) is one-to-one A1: dom (id X) = X ; percases ( ( x in X & y in X ) or not x in X or not y in X ) ; supposeA2: ( x in X & y in X ) ; ::_thesis: Swap ((id X),x,y) is one-to-one set g = id X; set f = Swap ((id X),x,y); let z be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not z in proj1 (Swap ((id X),x,y)) or not b1 in proj1 (Swap ((id X),x,y)) or not (Swap ((id X),x,y)) . z = (Swap ((id X),x,y)) . b1 or z = b1 ) let t be set ; ::_thesis: ( not z in proj1 (Swap ((id X),x,y)) or not t in proj1 (Swap ((id X),x,y)) or not (Swap ((id X),x,y)) . z = (Swap ((id X),x,y)) . t or z = t ) assume A3: ( z in dom (Swap ((id X),x,y)) & t in dom (Swap ((id X),x,y)) & (Swap ((id X),x,y)) . z = (Swap ((id X),x,y)) . t ) ; ::_thesis: z = t A4: ( (id X) . z = z & (id X) . t = t & (id X) . x = x & (id X) . y = y ) by A2, A3, FUNCT_1:17; then A5: ( ( z = x implies (Swap ((id X),x,y)) . z = y ) & ( z = y implies (Swap ((id X),x,y)) . z = x ) & ( z <> x & z <> y implies (Swap ((id X),x,y)) . z = z ) ) by A2, A1, Th29, Th31, Th33; ( ( t = x implies (Swap ((id X),x,y)) . t = y ) & ( t = y implies (Swap ((id X),x,y)) . t = x ) & ( t <> x & t <> y implies (Swap ((id X),x,y)) . t = t ) ) by A2, A1, A4, Th29, Th31, Th33; hence z = t by A3, A5; ::_thesis: verum end; suppose ( not x in X or not y in X ) ; ::_thesis: Swap ((id X),x,y) is one-to-one hence Swap ((id X),x,y) is one-to-one by A1, FUNCT_7:def_12; ::_thesis: verum end; end; 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 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 ) proof A1: dom (id X) = X ; reconsider a = x, b = y as Element of dom (id X) ; Swap ((id X),a,b) is onto ; hence Swap ((id X),x,y) is onto ; ::_thesis: Swap ((id X),x,y) is total thus dom (Swap ((id X),x,y)) = X by A1, FUNCT_7:99; :: according to PARTFUN1:def_2 ::_thesis: verum 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 set g = Swap (f,x,y); A1: dom f = X by FUNCT_2:def_1; A2: ( dom (Swap (f,x,y)) = dom f & rng (Swap (f,x,y)) = rng f ) by FUNCT_7:99, FUNCT_7:103; rng f c= Y by RELAT_1:def_19; hence Swap (f,x,y) is Function of X,Y by A1, A2, FUNCT_2:2; ::_thesis: verum end; 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 proof let x, X, y be set ; ::_thesis: 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 let f be Function; ::_thesis: 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 let A be array; ::_thesis: ( x in X & y in X & f = Swap ((id X),x,y) & X = dom A implies Swap (A,x,y) = A * f ) assume that A1: ( x in X & y in X ) and A2: ( f = Swap ((id X),x,y) & X = dom A ) ; ::_thesis: Swap (A,x,y) = A * f set g = id X; set s = Swap (A,x,y); A3: ( dom (id X) = X & rng (id X) = X ) ; then A4: ( dom f = X & rng f = X ) by A2, FUNCT_7:99, FUNCT_7:103; A5: dom (Swap (A,x,y)) = dom A by FUNCT_7:99; A6: dom (A * f) = dom f by A2, A4, RELAT_1:27; now__::_thesis:_for_z_being_set_st_z_in_X_holds_ (Swap_(A,x,y))_._z_=_(A_*_f)_._z let z be set ; ::_thesis: ( z in X implies (Swap (A,x,y)) . z = (A * f) . z ) assume A7: z in X ; ::_thesis: (Swap (A,x,y)) . z = (A * f) . z A8: ( (id X) . x = x & (id X) . y = y & (id X) . z = z ) by A1, A7, FUNCT_1:17; ( z = x or z = y or ( z <> x & z <> y ) ) ; then ( ( (Swap (A,x,y)) . z = A . y & f . z = (id X) . y ) or ( (Swap (A,x,y)) . z = A . x & f . z = (id X) . x ) or ( (Swap (A,x,y)) . z = A . z & f . z = (id X) . z ) ) by A1, A2, A3, Th29, Th31, Th33; hence (Swap (A,x,y)) . z = (A * f) . z by A7, A8, A4, FUNCT_1:13; ::_thesis: verum end; hence Swap (A,x,y) = A * f by A2, A4, A5, A6, FUNCT_1:2; ::_thesis: verum 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 let x, y be set ; ::_thesis: 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) ) let A be array; ::_thesis: ( x in dom A & y in dom A implies ( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) ) ) set X = dom A; assume A1: ( x in dom A & y in dom A ) ; ::_thesis: ( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) ) thus Swap (A,x,y) is permutation of A ::_thesis: A is permutation of Swap (A,x,y) proof reconsider X = dom A as non empty set by A1; reconsider x = x, y = y as Element of X by A1; reconsider f = Swap ((id X),x,y) as Permutation of (dom A) ; take f ; :: according to EXCHSORT:def_9 ::_thesis: Swap (A,x,y) = A * f thus Swap (A,x,y) = A * f by Th42; ::_thesis: verum end; hence A is permutation of Swap (A,x,y) by Th39; ::_thesis: verum 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 let x, y be set ; ::_thesis: 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) ) let A, B be array; ::_thesis: ( x in dom A & y in dom A & A is permutation of B implies ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) ) ) set X = dom A; assume A1: ( x in dom A & y in dom A & A is permutation of B ) ; ::_thesis: ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) ) then dom A = dom B by Th37; then ( Swap (A,x,y) is permutation of A & B is permutation of Swap (B,x,y) ) by A1, Th43; hence ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) ) by A1, Th40; ::_thesis: verum end; 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 proof let R be empty array of O; ::_thesis: R is ascending let a be ordinal number ; :: according to EXCHSORT:def_10 ::_thesis: for b being ordinal number st a in dom R & b in dom R & a in b holds R /. a <= R /. b thus for b being ordinal number st a in dom R & b in dom R & a in b holds R /. a <= R /. b ; ::_thesis: verum end; let A be empty array of O; cluster inversions A -> empty ; coherence inversions A is empty proof set w = the Element of inversions A; assume not inversions A is empty ; ::_thesis: contradiction then the Element of inversions A in inversions A ; then consider a, b being Element of dom A such that A1: ( the Element of inversions A = [a,b] & a in b & not A /. a <= A /. b ) ; thus contradiction by A1, SUBSET_1:def_1; ::_thesis: verum 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 let O be non empty connected Poset; ::_thesis: for x, y being Element of O holds ( x > y iff not x <= y ) let x, y be Element of O; ::_thesis: ( x > y iff not x <= y ) A1: ( x <= y & y <= x implies x = y ) by YELLOW_0:def_3; ( ( x <= y or x >= y ) & x <= x ) by WAYBEL_0:def_29; hence ( x > y iff not x <= y ) by A1, ORDERS_2:def_6; ::_thesis: verum 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 set N = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ; inversions R = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } proof thus inversions R c= { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } :: according to XBOOLE_0:def_10 ::_thesis: { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } c= inversions R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in inversions R or x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ) assume x in inversions R ; ::_thesis: x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } then consider a, b being Element of dom R such that A1: ( x = [a,b] & a in b & not R /. a <= R /. b ) ; R /. a > R /. b by A1, Th45; hence x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } by A1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } or x in inversions R ) assume x in { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ; ::_thesis: x in inversions R then consider a, b being Element of dom R such that A2: ( x = [a,b] & a in b & R /. a > R /. b ) ; not R /. a <= R /. b by A2, Th45; hence x in inversions R by A2; ::_thesis: verum end; hence 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 ) } ) ; ::_thesis: verum 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 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 ) ) proof let x, y be set ; ::_thesis: 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 ) ) let O be non empty connected Poset; ::_thesis: 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 ) ) let R be array of O; ::_thesis: ( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) ) hereby ::_thesis: ( x in dom R & y in dom R & x in y & R /. x > R /. y implies [x,y] in inversions R ) assume A1: [x,y] in inversions R ; ::_thesis: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) then reconsider R1 = R as non empty Function ; consider a, b being Element of dom R1 such that A2: ( [x,y] = [a,b] & a in b & not R /. a <= R /. b ) by A1; ( x = a & y = b ) by A2, XTUPLE_0:1; hence ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by A2, Th45; ::_thesis: verum end; thus ( x in dom R & y in dom R & x in y & R /. x > R /. y implies [x,y] in inversions R ) ; ::_thesis: verum 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 let O be non empty connected Poset; ::_thesis: for R being array of O holds inversions R c= [:(dom R),(dom R):] let R be array of O; ::_thesis: inversions R c= [:(dom R),(dom R):] let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in inversions R or x in [:(dom R),(dom R):] ) assume A1: x in inversions R ; ::_thesis: x in [:(dom R),(dom R):] then consider a, b being Element of dom R such that A2: ( x = [a,b] & a in b & R /. a > R /. b ) ; ( a in dom R & b in dom R ) by A2, A1, Th46; hence x in [:(dom R),(dom R):] by A2, ZFMISC_1:def_2; ::_thesis: verum 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 inversions R c= [:(dom R),(dom R):] by Th47; hence inversions R is finite ; ::_thesis: verum 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 let O be non empty connected Poset; ::_thesis: for R being array of O holds ( R is ascending iff inversions R = {} ) let R be array of O; ::_thesis: ( R is ascending iff inversions R = {} ) thus ( R is ascending implies inversions R = {} ) ::_thesis: ( inversions R = {} implies R is ascending ) proof assume A1: for a, b being ordinal number st a in dom R & b in dom R & a in b holds R /. a <= R /. b ; :: according to EXCHSORT:def_10 ::_thesis: inversions R = {} set x = the Element of inversions R; assume A2: inversions R <> {} ; ::_thesis: contradiction then the Element of inversions R in inversions R ; then consider a, b being Element of dom R such that A3: ( the Element of inversions R = [a,b] & a in b & R /. a > R /. b ) ; R <> {} by A2; then R /. a <= R /. b by A1, A3; hence contradiction by A3, Th45; ::_thesis: verum end; assume A4: inversions R = {} ; ::_thesis: R is ascending let a be ordinal number ; :: according to EXCHSORT:def_10 ::_thesis: for b being ordinal number st a in dom R & b in dom R & a in b holds R /. a <= R /. b let b be ordinal number ; ::_thesis: ( a in dom R & b in dom R & a in b implies R /. a <= R /. b ) assume ( a in dom R & b in dom R & a in b ) ; ::_thesis: R /. a <= R /. b then ( R /. a > R /. b implies [a,b] in inversions R ) ; hence R /. a <= R /. b by A4, Th45; ::_thesis: verum 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 let x, y be set ; ::_thesis: 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 let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R holds [y,x] nin inversions R let R be array of O; ::_thesis: ( [x,y] in inversions R implies [y,x] nin inversions R ) assume [x,y] in inversions R ; ::_thesis: [y,x] nin inversions R then y nin x by Th46; hence [y,x] nin inversions R by Th46; ::_thesis: verum 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 let x, y, z be set ; ::_thesis: 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 let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R & [y,z] in inversions R holds [x,z] in inversions R let R be array of O; ::_thesis: ( [x,y] in inversions R & [y,z] in inversions R implies [x,z] in inversions R ) assume A1: ( [x,y] in inversions R & [y,z] in inversions R ) ; ::_thesis: [x,z] in inversions R then reconsider x = x, y = y, z = z as Element of dom R by Th46; ( x in y & R /. x > R /. y & y in z & R /. y > R /. z ) by A1, Th46; then ( x in z & R /. x > R /. z ) by ORDERS_2:5, ORDINAL1:10; hence [x,z] in inversions R ; ::_thesis: verum 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 inversions R c= [:(dom R),(dom R):] by Th47; hence inversions R is Relation-like ; ::_thesis: verum end; 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 ) proof let r be Relation; ::_thesis: ( r = inversions R implies ( r is asymmetric & r is transitive ) ) assume A1: r = inversions R ; ::_thesis: ( r is asymmetric & r is transitive ) thus r is asymmetric ::_thesis: r is transitive proof let x be set ; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: for b1 being set holds ( not x in field r or not b1 in field r or not [x,b1] in r or not [b1,x] in r ) let y be set ; ::_thesis: ( not x in field r or not y in field r or not [x,y] in r or not [y,x] in r ) thus ( not x in field r or not y in field r or not [x,y] in r or not [y,x] in r ) by A1, Th49; ::_thesis: verum end; let x be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for b1, b2 being set holds ( not x in field r or not b1 in field r or not b2 in field r or not [x,b1] in r or not [b1,b2] in r or [x,b2] in r ) let y be set ; ::_thesis: for b1 being set holds ( not x in field r or not y in field r or not b1 in field r or not [x,y] in r or not [y,b1] in r or [x,b1] in r ) thus for b1 being set holds ( not x in field r or not y in field r or not b1 in field r or not [x,y] in r or not [y,b1] in r or [x,b1] in r ) by A1, Th50; ::_thesis: verum end; 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)) proof let x, y be set ; ::_thesis: 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)) let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R holds [x,y] nin inversions (Swap (R,x,y)) let R be array of O; ::_thesis: ( [x,y] in inversions R implies [x,y] nin inversions (Swap (R,x,y)) ) assume A1: [x,y] in inversions R ; ::_thesis: [x,y] nin inversions (Swap (R,x,y)) then A2: ( x in dom R & y in dom R & R /. x > R /. y ) by Th46; A3: not R /. x < R /. y by A1, Th46; ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. y = R /. x ) by A2, Th30, Th32; hence [x,y] nin inversions (Swap (R,x,y)) by A3, Th46; ::_thesis: verum 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 let x, y, z, t be set ; ::_thesis: 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)) ) let O be non empty connected Poset; ::_thesis: 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)) ) let R be array of O; ::_thesis: ( x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y implies ( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) ) ) set s = Swap (R,x,y); assume ( x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y ) ; ::_thesis: ( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) ) then A1: ( ( z in dom R implies (Swap (R,x,y)) /. z = R /. z ) & ( t in dom R implies (Swap (R,x,y)) /. t = R /. t ) & dom (Swap (R,x,y)) = dom R ) by Th34, FUNCT_7:99; hereby ::_thesis: ( [z,t] in inversions (Swap (R,x,y)) implies [z,t] in inversions R ) assume [z,t] in inversions R ; ::_thesis: [z,t] in inversions (Swap (R,x,y)) then ( z in dom R & t in dom R & z in t & R /. z > R /. t ) by Th46; hence [z,t] in inversions (Swap (R,x,y)) by A1; ::_thesis: verum end; assume [z,t] in inversions (Swap (R,x,y)) ; ::_thesis: [z,t] in inversions R then ( z in dom R & t in dom R & z in t & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. t ) by A1, Th46; hence [z,t] in inversions R by A1; ::_thesis: verum 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 let x, y, z be set ; ::_thesis: 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)) ) let O be non empty connected Poset; ::_thesis: 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)) ) let R be array of O; ::_thesis: ( [x,y] in inversions R implies ( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) ) ) set s = Swap (R,x,y); assume [x,y] in inversions R ; ::_thesis: ( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) ) then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46; then A2: ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. y = R /. x & dom (Swap (R,x,y)) = dom R ) by Th30, Th32, FUNCT_7:99; hereby ::_thesis: ( [z,x] in inversions (Swap (R,x,y)) implies ( [z,y] in inversions R & z in x ) ) assume A3: ( [z,y] in inversions R & z in x ) ; ::_thesis: [z,x] in inversions (Swap (R,x,y)) then A4: ( z in dom R & z in y & R /. z > R /. y ) by Th46; then ( x <> z & y <> z ) by A3; then (Swap (R,x,y)) /. z = R /. z by A4, Th34; hence [z,x] in inversions (Swap (R,x,y)) by A3, A1, A2, A4; ::_thesis: verum end; assume [z,x] in inversions (Swap (R,x,y)) ; ::_thesis: ( [z,y] in inversions R & z in x ) then A5: ( z in dom R & z in x & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. x ) by A2, Th46; then A6: z in y by A1, ORDINAL1:10; (Swap (R,x,y)) /. z = R /. z by A1, A5, Th34; hence ( [z,y] in inversions R & z in x ) by A1, A2, A5, A6; ::_thesis: verum 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 let x, y, z be set ; ::_thesis: 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)) ) ) let O be non empty connected Poset; ::_thesis: 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)) ) ) let R be array of O; ::_thesis: ( [x,y] in inversions R implies ( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) ) ) assume [x,y] in inversions R ; ::_thesis: ( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) ) then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46; A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99; hereby ::_thesis: ( z in x & [z,y] in inversions (Swap (R,x,y)) implies [z,x] in inversions R ) assume [z,x] in inversions R ; ::_thesis: ( z in x & [z,y] in inversions (Swap (R,x,y)) ) then A3: ( z in dom R & z in x & R /. z > R /. x ) by Th46; then A4: z in y by A1, ORDINAL1:10; ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A3, Th32, Th34; hence ( z in x & [z,y] in inversions (Swap (R,x,y)) ) by A1, A2, A3, A4; ::_thesis: verum end; assume A5: ( z in x & [z,y] in inversions (Swap (R,x,y)) ) ; ::_thesis: [z,x] in inversions R then A6: ( z in dom R & z in y & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. y ) by A2, Th46; then ( z <> x & z <> y ) by A5; then ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A6, Th32, Th34; hence [z,x] in inversions R by A1, A6, A5; ::_thesis: verum 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 let x, y, z be set ; ::_thesis: 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 let O be non empty connected Poset; ::_thesis: 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 let R be array of O; ::_thesis: ( [x,y] in inversions R & z in y & [x,z] in inversions (Swap (R,x,y)) implies [x,z] in inversions R ) assume [x,y] in inversions R ; ::_thesis: ( not z in y or not [x,z] in inversions (Swap (R,x,y)) or [x,z] in inversions R ) then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46; A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99; assume A3: z in y ; ::_thesis: ( not [x,z] in inversions (Swap (R,x,y)) or [x,z] in inversions R ) assume [x,z] in inversions (Swap (R,x,y)) ; ::_thesis: [x,z] in inversions R then A4: ( z in dom R & x in z & (Swap (R,x,y)) /. x > (Swap (R,x,y)) /. z ) by A2, Th46; then ( z <> x & z <> y ) by A3; then ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. z = R /. z ) by A1, A4, Th30, Th34; then R /. x > R /. z by A1, A4, ORDERS_2:5; hence [x,z] in inversions R by A1, A4; ::_thesis: verum 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 let x, y, z be set ; ::_thesis: 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 let O be non empty connected Poset; ::_thesis: 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 let R be array of O; ::_thesis: ( [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) implies [z,y] in inversions R ) assume [x,y] in inversions R ; ::_thesis: ( not x in z or not [z,y] in inversions (Swap (R,x,y)) or [z,y] in inversions R ) then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46; A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99; assume A3: x in z ; ::_thesis: ( not [z,y] in inversions (Swap (R,x,y)) or [z,y] in inversions R ) assume [z,y] in inversions (Swap (R,x,y)) ; ::_thesis: [z,y] in inversions R then A4: ( z in dom R & z in y & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. y ) by A2, Th46; then ( z <> x & z <> y ) by A3; then ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A4, Th32, Th34; then R /. z > R /. y by A1, A4, ORDERS_2:5; hence [z,y] in inversions R by A1, A4; ::_thesis: verum 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 let x, y, z be set ; ::_thesis: 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 let O be non empty connected Poset; ::_thesis: 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 let R be array of O; ::_thesis: ( [x,y] in inversions R & y in z & [x,z] in inversions (Swap (R,x,y)) implies [y,z] in inversions R ) assume [x,y] in inversions R ; ::_thesis: ( not y in z or not [x,z] in inversions (Swap (R,x,y)) or [y,z] in inversions R ) then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46; A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99; assume A3: y in z ; ::_thesis: ( not [x,z] in inversions (Swap (R,x,y)) or [y,z] in inversions R ) assume [x,z] in inversions (Swap (R,x,y)) ; ::_thesis: [y,z] in inversions R then A4: ( z in dom R & x in z & (Swap (R,x,y)) /. x > (Swap (R,x,y)) /. z ) by A2, Th46; then ( z <> x & z <> y ) by A3; then ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. z = R /. z ) by A1, A4, Th30, Th34; hence [y,z] in inversions R by A1, A4, A3; ::_thesis: verum 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 let x, y, z be set ; ::_thesis: 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)) ) let O be non empty connected Poset; ::_thesis: 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)) ) let R be array of O; ::_thesis: ( [x,y] in inversions R implies ( ( y in z & [x,z] in inversions R ) iff [y,z] in inversions (Swap (R,x,y)) ) ) assume [x,y] in inversions R ; ::_thesis: ( ( y in z & [x,z] in inversions R ) iff [y,z] in inversions (Swap (R,x,y)) ) then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46; A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99; hereby ::_thesis: ( [y,z] in inversions (Swap (R,x,y)) implies ( y in z & [x,z] in inversions R ) ) assume A3: ( y in z & [x,z] in inversions R ) ; ::_thesis: [y,z] in inversions (Swap (R,x,y)) then A4: ( z in dom R & x in z & R /. z < R /. x ) by Th46; then ( z <> x & z <> y ) by A3; then ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A4, Th32, Th34; hence [y,z] in inversions (Swap (R,x,y)) by A1, A2, A4, A3; ::_thesis: verum end; assume [y,z] in inversions (Swap (R,x,y)) ; ::_thesis: ( y in z & [x,z] in inversions R ) then A5: ( z in dom R & y in z & (Swap (R,x,y)) /. y > (Swap (R,x,y)) /. z ) by A2, Th46; then A6: x in z by A1, ORDINAL1:10; ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, Th32, Th34, A5; hence ( y in z & [x,z] in inversions R ) by A1, A5, A6; ::_thesis: verum 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 Th59: :: EXCHSORT:59 for c, b, a being ordinal number holds ( c in (succ b) \ a iff ( a c= c & c c= b ) ) proof let c, b, a be ordinal number ; ::_thesis: ( c in (succ b) \ a iff ( a c= c & c c= b ) ) ( a c= c iff c nin a ) by ORDINAL6:4; then ( c in (succ b) \ a iff ( c in succ b & a c= c ) ) by XBOOLE_0:def_5; hence ( c in (succ b) \ a iff ( a c= c & c c= b ) ) by ORDINAL1:22; ::_thesis: verum end; 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 proof let O be non empty connected Poset; ::_thesis: for T being non empty array of O for q, p being Element of dom T holds (succ q) \ p c= dom T let T be non empty array of O; ::_thesis: for q, p being Element of dom T holds (succ q) \ p c= dom T let q, p be Element of dom T; ::_thesis: (succ q) \ p c= dom T let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (succ q) \ p or x in dom T ) assume A1: x in (succ q) \ p ; ::_thesis: x in dom T A2: ( p c= x & x c= q ) by A1, Th59; consider a, b being ordinal number such that A3: dom T = a \ b by Def1; ( q in a & p nin b ) by A3, XBOOLE_0:def_5; then ( x in a & x nin b ) by A1, A2, ORDINAL1:12; hence x in dom T by A3, XBOOLE_0:def_5; ::_thesis: verum 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 let O be non empty connected Poset; ::_thesis: 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):] ) let T be non empty array of O; ::_thesis: 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):] ) let p, q be Element of dom T; ::_thesis: ( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] ) set X = dom T; set i = id (dom T); set s = Swap ((id (dom T)),p,q); set f = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]; set Y = (succ q) \ p; set Z1 = [:{p},((succ q) \ p):]; set Z2 = [:((succ q) \ p),{q}:]; set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]); dom (id (dom T)) = dom T ; then A1: dom (Swap ((id (dom T)),p,q)) = dom T by FUNCT_7:99; A2: ( {p} c= dom T & {q} c= dom T & (succ q) \ p c= dom T ) by Th60, ZFMISC_1:31; A3: [:(dom T),(dom T):] \/ ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]) = ([:(dom T),(dom T):] \/ [:{p},((succ q) \ p):]) \/ [:((succ q) \ p),{q}:] by XBOOLE_1:4 .= [:(dom T),(dom T):] \/ [:((succ q) \ p),{q}:] by A2, XBOOLE_1:12, ZFMISC_1:96 .= [:(dom T),(dom T):] by A2, XBOOLE_1:12, ZFMISC_1:96 ; thus dom ((T,p,q) incl) = (dom [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]) \/ (dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]))) by FUNCT_4:def_1 .= (dom [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]) \/ ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]) .= [:(dom T),(dom T):] by A1, A3, FUNCT_3:def_8 ; ::_thesis: rng ((T,p,q) incl) c= [:(dom T),(dom T):] A4: ( rng (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) = [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] & rng (id (dom T)) = dom T ) ; rng (Swap ((id (dom T)),p,q)) = dom T by A4, FUNCT_7:103; then rng [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] = [:(dom T),(dom T):] by FUNCT_3:67; hence rng ((T,p,q) incl) c= [:(dom T),(dom T):] by A3, A4, FUNCT_4:17; ::_thesis: verum end; 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] ) proof let O be non empty connected Poset; ::_thesis: 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] ) let T be non empty array of O; ::_thesis: 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] ) let p, r, q be Element of dom T; ::_thesis: ( p c= r & r c= q implies ( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] ) ) assume A1: ( p c= r & r c= q ) ; ::_thesis: ( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] ) set Y = (succ q) \ p; set Z1 = [:{p},((succ q) \ p):]; set Z2 = [:((succ q) \ p),{q}:]; set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]); ( p in {p} & q in {q} & r in (succ q) \ p ) by A1, Th59, TARSKI:def_1; then ( [p,r] in [:{p},((succ q) \ p):] & [r,q] in [:((succ q) \ p),{q}:] ) by ZFMISC_1:def_2; then A2: ( [p,r] in [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] & [r,q] in [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] ) by XBOOLE_0:def_3; A3: dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) = [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] ; hence ((T,p,q) incl) . (p,r) = (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) . (p,r) by A2, FUNCT_4:13 .= [p,r] by A2, FUNCT_1:17 ; ::_thesis: ((T,p,q) incl) . (r,q) = [r,q] thus ((T,p,q) incl) . (r,q) = (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) . (r,q) by A2, A3, FUNCT_4:13 .= [r,q] by A2, FUNCT_1:17 ; ::_thesis: verum 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 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 let f be Function; ::_thesis: 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)] let O be non empty connected Poset; ::_thesis: 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)] let T be non empty array of O; ::_thesis: 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)] let r, p, s, q be Element of dom T; ::_thesis: ( r <> p & s <> q & f = Swap ((id (dom T)),p,q) implies ((T,p,q) incl) . (r,s) = [(f . r),(f . s)] ) assume that A1: ( r <> p & s <> q ) and A2: f = Swap ((id (dom T)),p,q) ; ::_thesis: ((T,p,q) incl) . (r,s) = [(f . r),(f . s)] set Y = (succ q) \ p; set Z1 = [:{p},((succ q) \ p):]; set Z2 = [:((succ q) \ p),{q}:]; set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]); A3: dom f = dom (id (dom T)) by A2, FUNCT_7:99 .= dom T ; ( r nin {p} & s nin {q} ) by A1, TARSKI:def_1; then ( [r,s] nin [:{p},((succ q) \ p):] & [r,s] nin [:((succ q) \ p),{q}:] ) by ZFMISC_1:87; then [r,s] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) by XBOOLE_0:def_3; hence ((T,p,q) incl) . (r,s) = [:f,f:] . (r,s) by A2, FUNCT_4:11 .= [(f . r),(f . s)] by A3, FUNCT_3:def_8 ; ::_thesis: verum 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 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 let f be Function; ::_thesis: 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)] ) let O be non empty connected Poset; ::_thesis: 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)] ) let T be non empty array of O; ::_thesis: 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)] ) let r, p, q be Element of dom T; ::_thesis: ( r in p & f = Swap ((id (dom T)),p,q) implies ( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] ) ) assume that A1: r in p and A2: f = Swap ((id (dom T)),p,q) ; ::_thesis: ( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] ) set X = dom T; set i = id (dom T); set s = Swap ((id (dom T)),p,q); set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]; set Y = (succ q) \ p; set Z1 = [:{p},((succ q) \ p):]; set Z2 = [:((succ q) \ p),{q}:]; set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]); dom (id (dom T)) = dom T ; then A3: dom (Swap ((id (dom T)),p,q)) = dom T by FUNCT_7:99; not p c= r by A1, ORDINAL6:4; then ( r nin {p} & r nin (succ q) \ p ) by Th59, TARSKI:def_1; then ( [r,p] nin [:{p},((succ q) \ p):] & [r,p] nin [:((succ q) \ p),{q}:] & [r,q] nin [:{p},((succ q) \ p):] & [r,q] nin [:((succ q) \ p),{q}:] ) by ZFMISC_1:87; then A4: ( [r,q] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) & [r,p] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) ) by XBOOLE_0:def_3; hence ((T,p,q) incl) . (r,q) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (r,q) by FUNCT_4:11 .= [(f . r),(f . q)] by A2, A3, FUNCT_3:def_8 ; ::_thesis: ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] thus ((T,p,q) incl) . (r,p) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (r,p) by A4, FUNCT_4:11 .= [(f . r),(f . p)] by A2, A3, FUNCT_3:def_8 ; ::_thesis: verum 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 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 let f be Function; ::_thesis: 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)] ) let O be non empty connected Poset; ::_thesis: 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)] ) let T be non empty array of O; ::_thesis: 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)] ) let q, r, p be Element of dom T; ::_thesis: ( q in r & f = Swap ((id (dom T)),p,q) implies ( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] ) ) assume that A1: q in r and A2: f = Swap ((id (dom T)),p,q) ; ::_thesis: ( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] ) set X = dom T; set i = id (dom T); set s = Swap ((id (dom T)),p,q); set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]; set Y = (succ q) \ p; set Z1 = [:{p},((succ q) \ p):]; set Z2 = [:((succ q) \ p),{q}:]; set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]); dom (id (dom T)) = dom T ; then A3: dom (Swap ((id (dom T)),p,q)) = dom T by FUNCT_7:99; not r c= q by A1, ORDINAL6:4; then ( r nin {q} & r nin (succ q) \ p ) by Th59, TARSKI:def_1; then ( [p,r] nin [:{p},((succ q) \ p):] & [p,r] nin [:((succ q) \ p),{q}:] & [q,r] nin [:{p},((succ q) \ p):] & [q,r] nin [:((succ q) \ p),{q}:] ) by ZFMISC_1:87; then A4: ( [p,r] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) & [q,r] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) ) by XBOOLE_0:def_3; hence ((T,p,q) incl) . (p,r) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (p,r) by FUNCT_4:11 .= [(f . p),(f . r)] by A2, A3, FUNCT_3:def_8 ; ::_thesis: ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] thus ((T,p,q) incl) . (q,r) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (q,r) by A4, FUNCT_4:11 .= [(f . q),(f . r)] by A2, A3, FUNCT_3:def_8 ; ::_thesis: verum 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 let O be non empty connected Poset; ::_thesis: 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] let T be non empty array of O; ::_thesis: for p, q being Element of dom T st p in q holds ((T,p,q) incl) . (p,q) = [p,q] let p, q be Element of dom T; ::_thesis: ( p in q implies ((T,p,q) incl) . (p,q) = [p,q] ) assume p in q ; ::_thesis: ((T,p,q) incl) . (p,q) = [p,q] then p c= q by ORDINAL1:def_2; hence ((T,p,q) incl) . (p,q) = [p,q] by Th62; ::_thesis: verum 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 let O be non empty connected Poset; ::_thesis: 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] let T be non empty array of O; ::_thesis: 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] let p, q, r, s be Element of dom T; ::_thesis: ( p in q & r <> p & r <> q & s <> p & s <> q implies ((T,p,q) incl) . (r,s) = [r,s] ) assume A1: ( p in q & r <> p & r <> q & s <> p & s <> q ) ; ::_thesis: ((T,p,q) incl) . (r,s) = [r,s] set X = dom T; set i = id (dom T); set f = Swap ((id (dom T)),p,q); set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]; set Y = (succ q) \ p; thus ((T,p,q) incl) . (r,s) = [((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . s)] by A1, Th63 .= [((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . s)] by A1, Th33 .= [((id (dom T)) . r),((id (dom T)) . s)] by A1, Th33 .= [r,((id (dom T)) . s)] by FUNCT_1:17 .= [r,s] by FUNCT_1:17 ; ::_thesis: verum end; 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] ) proof let O be non empty connected Poset; ::_thesis: 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] ) let T be non empty array of O; ::_thesis: 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] ) let r, p, q be Element of dom T; ::_thesis: ( r in p & p in q implies ( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] ) ) assume A1: ( r in p & p in q ) ; ::_thesis: ( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] ) set X = dom T; set i = id (dom T); set f = Swap ((id (dom T)),p,q); set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]; set Y = (succ q) \ p; A2: dom (id (dom T)) = dom T ; A3: ( r <> p & r <> q ) by A1; thus ((T,p,q) incl) . (r,p) = [((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . p)] by A1, Th64 .= [((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . p)] by A3, Th33 .= [r,((Swap ((id (dom T)),p,q)) . p)] by FUNCT_1:17 .= [r,((id (dom T)) . q)] by A2, Th29 .= [r,q] by FUNCT_1:17 ; ::_thesis: ((T,p,q) incl) . (r,q) = [r,p] thus ((T,p,q) incl) . (r,q) = [((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . q)] by A1, Th64 .= [((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . q)] by A3, Th33 .= [r,((Swap ((id (dom T)),p,q)) . q)] by FUNCT_1:17 .= [r,((id (dom T)) . p)] by A2, Th31 .= [r,p] by FUNCT_1:17 ; ::_thesis: verum end; 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] ) proof let O be non empty connected Poset; ::_thesis: 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] ) let T be non empty array of O; ::_thesis: 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] ) let p, s, q be Element of dom T; ::_thesis: ( p in s & s in q implies ( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] ) ) assume ( p in s & s in q ) ; ::_thesis: ( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] ) then ( p c= s & s c= q ) by ORDINAL1:def_2; hence ( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] ) by Th62; ::_thesis: verum 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 let O be non empty connected Poset; ::_thesis: 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] ) let T be non empty array of O; ::_thesis: 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] ) let p, q, s be Element of dom T; ::_thesis: ( p in q & q in s implies ( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] ) ) assume A1: ( p in q & q in s ) ; ::_thesis: ( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] ) set X = dom T; set i = id (dom T); set f = Swap ((id (dom T)),p,q); set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]; set Y = (succ q) \ p; A2: dom (id (dom T)) = dom T ; A3: ( s <> p & s <> q ) by A1; thus ((T,p,q) incl) . (p,s) = [((Swap ((id (dom T)),p,q)) . p),((Swap ((id (dom T)),p,q)) . s)] by A1, Th65 .= [((Swap ((id (dom T)),p,q)) . p),((id (dom T)) . s)] by A3, Th33 .= [((Swap ((id (dom T)),p,q)) . p),s] by FUNCT_1:17 .= [((id (dom T)) . q),s] by A2, Th29 .= [q,s] by FUNCT_1:17 ; ::_thesis: ((T,p,q) incl) . (q,s) = [p,s] thus ((T,p,q) incl) . (q,s) = [((Swap ((id (dom T)),p,q)) . q),((Swap ((id (dom T)),p,q)) . s)] by A1, Th65 .= [((Swap ((id (dom T)),p,q)) . q),((id (dom T)) . s)] by A3, Th33 .= [((Swap ((id (dom T)),p,q)) . q),s] by FUNCT_1:17 .= [((id (dom T)) . p),s] by A2, Th31 .= [p,s] by FUNCT_1:17 ; ::_thesis: verum 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 let f be Function; ::_thesis: 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 ) let O be non empty connected Poset; ::_thesis: 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 ) let T be non empty array of O; ::_thesis: 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 ) let p, q be Element of dom T; ::_thesis: ( p in q & f = (T,p,q) incl implies 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 ) ) assume A1: ( p in q & f = (T,p,q) incl ) ; ::_thesis: 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 ) then A2: p <> q ; let x1, x2, y1, y2 be Element of dom T; ::_thesis: ( x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) implies ( x1 = x2 & y1 = y2 ) ) assume that A3: ( x1 in y1 & x2 in y2 ) and A4: f . (x1,y1) = f . (x2,y2) ; ::_thesis: ( x1 = x2 & y1 = y2 ) set X = dom T; set i = id (dom T); set s = Swap ((id (dom T)),p,q); set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]; set Y = (succ q) \ p; set Z1 = [:{p},((succ q) \ p):]; set Z2 = [:((succ q) \ p),{q}:]; set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]); percases ( ( x1 <> p & x1 <> q & y1 <> p & y1 <> q ) or ( x1 = p & y1 in q ) or ( x1 = p & y1 = q ) or ( p in x1 & y1 = q ) or ( x1 in p & y1 = p ) or ( x1 in p & y1 = q ) or ( x1 = p & q in y1 ) or ( x1 = q & q in y1 ) ) by A1, A3, Th2; supposeA5: ( x1 <> p & x1 <> q & y1 <> p & y1 <> q ) ; ::_thesis: ( x1 = x2 & y1 = y2 ) then A6: f . (x1,y1) = [x1,y1] by A1, Th67; percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2; suppose S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th67; hence ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; ::_thesis: verum end; suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,q] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; ::_thesis: verum end; suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,p] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; ::_thesis: verum end; suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; ::_thesis: verum end; suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th66; hence ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; ::_thesis: verum end; suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [q,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; ::_thesis: verum end; suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; ::_thesis: verum end; suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [p,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; ::_thesis: verum end; end; end; supposeA7: ( x1 = p & y1 in q ) ; ::_thesis: ( x1 = x2 & y1 = y2 ) then A8: f . (x1,y1) = [x1,y1] by A1, A3, Th69; percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2; suppose S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th67; hence ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; ::_thesis: verum end; suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,q] & x2 <> p ) by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A7, A4, A8, XTUPLE_0:1; ::_thesis: verum end; suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,p] & x2 <> p ) by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A7, A4, A8, XTUPLE_0:1; ::_thesis: verum end; suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; ::_thesis: verum end; suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th66; hence ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; ::_thesis: verum end; suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [q,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A2, A7, A4, A8, XTUPLE_0:1; ::_thesis: verum end; suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; ::_thesis: verum end; supposeA9: S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [p,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A7, A9, A4, A8, XTUPLE_0:1; ::_thesis: verum end; end; end; supposeA10: ( x1 = p & y1 = q ) ; ::_thesis: ( x1 = x2 & y1 = y2 ) then A11: f . (x1,y1) = [x1,y1] by A1, Th66; percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2; suppose S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th67; hence ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; ::_thesis: verum end; suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,q] & x2 <> p ) by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A10, A4, A11, XTUPLE_0:1; ::_thesis: verum end; suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,p] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A2, A10, A4, A11, XTUPLE_0:1; ::_thesis: verum end; suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; ::_thesis: verum end; suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th66; hence ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; ::_thesis: verum end; suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [q,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A2, A10, A4, A11, XTUPLE_0:1; ::_thesis: verum end; suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; ::_thesis: verum end; suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [p,y2] & y2 <> q ) by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A10, A4, A11, XTUPLE_0:1; ::_thesis: verum end; end; end; supposeA12: ( p in x1 & y1 = q ) ; ::_thesis: ( x1 = x2 & y1 = y2 ) then A13: f . (x1,y1) = [x1,y1] by A1, A3, Th69; percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2; suppose S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th67; hence ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; ::_thesis: verum end; supposeA14: S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,q] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A14, A12, A4, A13, XTUPLE_0:1; ::_thesis: verum end; supposeA15: S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,p] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A15, A12, A4, A13, XTUPLE_0:1; ::_thesis: verum end; suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; ::_thesis: verum end; suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th66; hence ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; ::_thesis: verum end; suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [q,y2] & y2 <> q ) by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A12, A4, A13, XTUPLE_0:1; ::_thesis: verum end; suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; ::_thesis: verum end; suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [p,y2] & y2 <> q ) by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A12, A4, A13, XTUPLE_0:1; ::_thesis: verum end; end; end; supposeA16: ( x1 in p & y1 = p ) ; ::_thesis: ( x1 = x2 & y1 = y2 ) then A17: f . (x1,y1) = [x1,q] by A1, Th68; percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2; supposeA18: S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th67; hence ( x1 = x2 & y1 = y2 ) by A18, A4, A17, XTUPLE_0:1; ::_thesis: verum end; supposeA19: S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,q] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A19, A16, A4, A17, XTUPLE_0:1; ::_thesis: verum end; suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,p] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A2, A4, A17, XTUPLE_0:1; ::_thesis: verum end; suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,y2] & x2 <> x1 ) by A16, A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; ::_thesis: verum end; suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,y2] & x2 <> x1 ) by A16, A1, Th66; hence ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; ::_thesis: verum end; suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [q,y2] & y2 <> q ) by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; ::_thesis: verum end; supposeA20: S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A16, A20, A4, A17, XTUPLE_0:1; ::_thesis: verum end; suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [p,y2] & x1 <> p ) by A16, A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; ::_thesis: verum end; end; end; supposeA21: ( x1 in p & y1 = q ) ; ::_thesis: ( x1 = x2 & y1 = y2 ) then A22: f . (x1,y1) = [x1,p] by A1, Th68; percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2; supposeA23: S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th67; hence ( x1 = x2 & y1 = y2 ) by A23, A4, A22, XTUPLE_0:1; ::_thesis: verum end; suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,q] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A2, A4, A22, XTUPLE_0:1; ::_thesis: verum end; supposeA24: S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,p] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A24, A21, A4, A22, XTUPLE_0:1; ::_thesis: verum end; supposeA25: S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,y2] & x1 <> p ) by A21, A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A25, A4, A22, XTUPLE_0:1; ::_thesis: verum end; supposeA26: S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th66; hence ( x1 = x2 & y1 = y2 ) by A26, A2, A4, A22, XTUPLE_0:1; ::_thesis: verum end; suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [q,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A1, A21, A4, A22, XTUPLE_0:1; ::_thesis: verum end; supposeA27: S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A2, A27, A4, A22, XTUPLE_0:1; ::_thesis: verum end; suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [p,y2] & x1 <> p ) by A21, A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A4, A22, XTUPLE_0:1; ::_thesis: verum end; end; end; supposeA28: ( x1 = p & q in y1 ) ; ::_thesis: ( x1 = x2 & y1 = y2 ) then A29: f . (x1,y1) = [q,y1] by A1, Th70; percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2; supposeA30: S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th67; hence ( x1 = x2 & y1 = y2 ) by A30, A4, A29, XTUPLE_0:1; ::_thesis: verum end; supposeA31: S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,q] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A1, A31, A4, A29, XTUPLE_0:1; ::_thesis: verum end; suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,p] by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A1, A28, A4, A29, XTUPLE_0:1; ::_thesis: verum end; suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,y2] & x2 <> q ) by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A29, XTUPLE_0:1; ::_thesis: verum end; supposeA32: S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th66; hence ( x1 = x2 & y1 = y2 ) by A2, A32, A4, A29, XTUPLE_0:1; ::_thesis: verum end; supposeA33: S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [q,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A33, A28, A4, A29, XTUPLE_0:1; ::_thesis: verum end; suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,y2] & x2 <> q ) by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A29, XTUPLE_0:1; ::_thesis: verum end; suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [p,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A2, A4, A29, XTUPLE_0:1; ::_thesis: verum end; end; end; supposeA34: ( x1 = q & q in y1 ) ; ::_thesis: ( x1 = x2 & y1 = y2 ) then A35: f . (x1,y1) = [p,y1] by A1, Th70; percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2; supposeA36: S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, Th67; hence ( x1 = x2 & y1 = y2 ) by A36, A4, A35, XTUPLE_0:1; ::_thesis: verum end; suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,q] & p <> x2 ) by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; ::_thesis: verum end; suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,p] & p <> x2 ) by A1, Th68; hence ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; ::_thesis: verum end; supposeA37: S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [x2,y2] by A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A34, A37, A4, A35, XTUPLE_0:1; ::_thesis: verum end; suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,y2] & y1 <> y2 ) by A34, A1, Th66; hence ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; ::_thesis: verum end; suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [q,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A2, A4, A35, XTUPLE_0:1; ::_thesis: verum end; suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then ( f . (x2,y2) = [x2,y2] & y2 <> y1 ) by A34, A1, A3, Th69; hence ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; ::_thesis: verum end; supposeA38: S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 ) then f . (x2,y2) = [p,y2] by A1, Th70; hence ( x1 = x2 & y1 = y2 ) by A38, A34, A4, A35, XTUPLE_0:1; ::_thesis: verum end; end; end; end; 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 let O be non empty connected Poset; ::_thesis: 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 let T be non empty array of O; ::_thesis: 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 let p, q be Element of dom T; ::_thesis: ( p in q implies ((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one ) assume A1: p in q ; ::_thesis: ((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one set f = (T,p,q) incl ; set s = Swap (T,p,q); set w = inversions (Swap (T,p,q)); set fw = ((T,p,q) incl) | (inversions (Swap (T,p,q))); A2: dom (Swap (T,p,q)) = dom T by FUNCT_7:99; let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not b1 in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not y in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y or x = y ) assume ( x in dom (((T,p,q) incl) | (inversions (Swap (T,p,q)))) & y in dom (((T,p,q) incl) | (inversions (Swap (T,p,q)))) ) ; ::_thesis: ( not (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y or x = y ) then A3: ( x in inversions (Swap (T,p,q)) & y in inversions (Swap (T,p,q)) ) by RELAT_1:57; then consider x1, y1 being Element of dom T such that A4: ( x = [x1,y1] & x1 in y1 & (Swap (T,p,q)) /. x1 > (Swap (T,p,q)) /. y1 ) by A2; consider x2, y2 being Element of dom T such that A5: ( y = [x2,y2] & x2 in y2 & (Swap (T,p,q)) /. x2 > (Swap (T,p,q)) /. y2 ) by A2, A3; assume (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y ; ::_thesis: x = y then ((T,p,q) incl) . (x1,y1) = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y by A4, A3, FUNCT_1:49 .= ((T,p,q) incl) . (x2,y2) by A5, A3, FUNCT_1:49 ; then ( x1 = x2 & y1 = y2 ) by A1, A4, A5, Lm1; hence x = y by A4, A5; ::_thesis: verum 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 set X = dom R; set i = id (dom R); set s = Swap ((id (dom R)),x,y); set h = [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):]; set Y = (succ y) \ x; set Z1 = [:{x},((succ y) \ x):]; set Z2 = [:((succ y) \ x),{y}:]; set g = id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]); A1: ((R,x,y) incl) .: z c= rng ((R,x,y) incl) by RELAT_1:111; A2: rng [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] = [:(rng (Swap ((id (dom R)),x,y))),(rng (Swap ((id (dom R)),x,y))):] by FUNCT_3:67; rng ((R,x,y) incl) c= (rng [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):]) \/ (rng (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]))) by FUNCT_4:17; hence ((R,x,y) incl) .: z is Relation-like by A1, A2; ::_thesis: verum end; 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 proof let x, y be set ; ::_thesis: 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 let O be non empty connected Poset; ::_thesis: 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 let R be array of O; ::_thesis: ( [x,y] in inversions R implies ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R ) assume A1: [x,y] in inversions R ; ::_thesis: ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R then A2: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46; reconsider T = R as non empty array of O by A1; reconsider p = x, q = y as Element of dom T by A1, Th46; set j = (R,x,y) incl ; set k = (T,p,q) incl ; set s = Swap (R,x,y); set t = Swap (T,p,q); set ws = inversions (Swap (R,x,y)); set w = inversions R; A3: dom (Swap (T,p,q)) = dom T by FUNCT_7:99; thus ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= inversions R :: according to XBOOLE_0:def_8 ::_thesis: not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions R proof let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [z,b1] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) or [z,b1] in inversions R ) let t be set ; ::_thesis: ( not [z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) or [z,t] in inversions R ) assume [z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ; ::_thesis: [z,t] in inversions R then consider a, b being set such that A4: ( [a,b] in inversions (Swap (R,x,y)) & [a,b] in dom ((R,x,y) incl) & [z,t] = ((R,x,y) incl) . (a,b) ) by Th5; A5: ( a in b & a in dom T & b in dom T ) by A4, A3, Th46; reconsider a = a, b = b as Element of dom T by A4, A3, Th46; percases ( ( a <> p & a <> q & b <> p & b <> q ) or ( a in p & b = p ) or ( a in p & b = q ) or ( a = p & b in q ) or ( a = p & b = q ) or ( a = p & q in b ) or ( a = q & q in b ) or ( p in a & q = b ) ) by A2, A5, Th2; supposeA6: ( a <> p & a <> q & b <> p & b <> q ) ; ::_thesis: [z,t] in inversions R then [z,t] = [a,b] by A4, A2, Th67; hence [z,t] in inversions R by A4, A6, Th52; ::_thesis: verum end; supposeA7: ( a in p & b = p ) ; ::_thesis: [z,t] in inversions R then [z,t] = [a,q] by A4, A2, Th68; hence [z,t] in inversions R by A1, A4, A7, Th53; ::_thesis: verum end; supposeA8: ( a in p & b = q ) ; ::_thesis: [z,t] in inversions R then [z,t] = [a,p] by A4, A2, Th68; hence [z,t] in inversions R by A1, A4, A8, Th54; ::_thesis: verum end; supposeA9: ( a = p & b in q ) ; ::_thesis: [z,t] in inversions R then [z,t] = [a,b] by A5, A4, Th69; hence [z,t] in inversions R by A1, A4, A9, Th55; ::_thesis: verum end; suppose ( a = p & b = q ) ; ::_thesis: [z,t] in inversions R hence [z,t] in inversions R by A1, A4, A2, Th66; ::_thesis: verum end; supposeA10: ( a = p & q in b ) ; ::_thesis: [z,t] in inversions R then [z,t] = [q,b] by A4, A2, Th70; hence [z,t] in inversions R by A1, A4, A10, Th57; ::_thesis: verum end; supposeA11: ( a = q & q in b ) ; ::_thesis: [z,t] in inversions R then [z,t] = [p,b] by A4, A2, Th70; hence [z,t] in inversions R by A1, A4, A11, Th58; ::_thesis: verum end; supposeA12: ( p in a & q = b ) ; ::_thesis: [z,t] in inversions R then [z,t] = [a,b] by A4, A5, Th69; hence [z,t] in inversions R by A1, A4, A12, Th56; ::_thesis: verum end; end; end; now__::_thesis:_(_[x,y]_in_((R,x,y)_incl)_.:_(inversions_(Swap_(R,x,y)))_implies_[x,y]_in_inversions_(Swap_(R,x,y))_) assume [x,y] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ; ::_thesis: [x,y] in inversions (Swap (R,x,y)) then consider a, b being set such that A13: ( [a,b] in inversions (Swap (R,x,y)) & [a,b] in dom ((R,x,y) incl) & [x,y] = ((R,x,y) incl) . (a,b) ) by Th5; A14: ((R,x,y) incl) . (p,q) = [p,q] by A2, Th66; A15: ( a in b & a in dom T & b in dom T ) by A13, A3, Th46; reconsider a = a, b = b as Element of dom T by A13, A3, Th46; ( a = p & b = q ) by A2, A13, A14, A15, Lm1; hence [x,y] in inversions (Swap (R,x,y)) by A13; ::_thesis: verum end; hence not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions R by A1, Th51; ::_thesis: verum 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 dom (Swap (R,x,y)) = dom R by FUNCT_7:99; hence Swap (R,x,y) is finite by FINSET_1:10; ::_thesis: verum 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 let x, y be set ; ::_thesis: 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) let O be non empty connected Poset; ::_thesis: 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) let R be array of O; ::_thesis: ( [x,y] in inversions R & inversions R is finite implies card (inversions (Swap (R,x,y))) in card (inversions R) ) set s = Swap (R,x,y); set h = (R,x,y) incl ; set ws = inversions (Swap (R,x,y)); assume A1: ( [x,y] in inversions R & inversions R is finite ) ; ::_thesis: card (inversions (Swap (R,x,y))) in card (inversions R) then reconsider w = inversions R as finite set ; ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R by A1, Th72; then ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= w by XBOOLE_0:def_8; then reconsider hws = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) as finite set ; card hws < card w by A1, Th72, TREES_1:6; then A2: card hws in card w by NAT_1:44; A3: ( x in dom R & y in dom R & x in y ) by A1, Th46; A4: not R is empty by A1; inversions (Swap (R,x,y)),((R,x,y) incl) .: (inversions (Swap (R,x,y))) are_equipotent proof take hw = ((R,x,y) incl) | (inversions (Swap (R,x,y))); :: according to WELLORD2:def_4 ::_thesis: ( hw is one-to-one & proj1 hw = inversions (Swap (R,x,y)) & proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ) thus hw is one-to-one by A3, A4, Th71; ::_thesis: ( proj1 hw = inversions (Swap (R,x,y)) & proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ) dom (Swap (R,x,y)) = dom R by FUNCT_7:99; then inversions (Swap (R,x,y)) c= [:(dom R),(dom R):] by Th47; then inversions (Swap (R,x,y)) c= dom ((R,x,y) incl) by A3, A4, Th61; hence dom hw = inversions (Swap (R,x,y)) by RELAT_1:62; ::_thesis: proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) thus proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) by RELAT_1:115; ::_thesis: verum end; hence card (inversions (Swap (R,x,y))) in card (inversions R) by A2, CARD_1:5; ::_thesis: verum 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 let x, y be set ; ::_thesis: 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) let O be non empty connected Poset; ::_thesis: for R being finite array of O st [x,y] in inversions R holds card (inversions (Swap (R,x,y))) < card (inversions R) let R be finite array of O; ::_thesis: ( [x,y] in inversions R implies card (inversions (Swap (R,x,y))) < card (inversions R) ) assume [x,y] in inversions R ; ::_thesis: card (inversions (Swap (R,x,y))) < card (inversions R) then card (inversions (Swap (R,x,y))) in card (inversions R) by Th73; hence card (inversions (Swap (R,x,y))) < card (inversions R) by NAT_1:44; ::_thesis: verum 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 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 reconsider C = <%R%> as non empty 0 -based array ; take C ; ::_thesis: ( C . (base- C) = R & ( for a being ordinal number st a in dom C holds C . a is array of O ) & ( for a being ordinal number st a in dom C & succ a in dom C holds ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) ) A1: ( dom C = 1 & 0 in 1 ) by AFINSQ_1:def_4, NAT_1:44; then base- C = 0 by Def4; hence C . (base- C) = R by AFINSQ_1:def_4; ::_thesis: ( ( for a being ordinal number st a in dom C holds C . a is array of O ) & ( for a being ordinal number st a in dom C & succ a in dom C holds ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) ) hereby ::_thesis: for a being ordinal number st a in dom C & succ a in dom C holds ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) let a be ordinal number ; ::_thesis: ( a in dom C implies C . a is array of O ) assume a in dom C ; ::_thesis: C . a is array of O then a = 0 by A1, ORDINAL3:15, TARSKI:def_1; hence C . a is array of O by AFINSQ_1:def_4; ::_thesis: verum end; let a be ordinal number ; ::_thesis: ( a in dom C & succ a in dom C implies ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) assume ( a in dom C & succ a in dom C ) ; ::_thesis: ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) hence ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) by A1, ORDINAL3:15, TARSKI:def_1; ::_thesis: verum end; 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 proof let a be ordinal number ; ::_thesis: for O being non empty connected Poset for R being array of O holds {[a,R]} is arr_computation of R let O be non empty connected Poset; ::_thesis: for R being array of O holds {[a,R]} is arr_computation of R let R be array of O; ::_thesis: {[a,R]} is arr_computation of R reconsider C = {[a,R]} as non empty a -based array ; C is arr_computation of R proof A1: ( dom C = {a} & a in {a} ) by FUNCT_5:12, TARSKI:def_1; then base- C = a by Def4; hence C . (base- C) = R by GRFUNC_1:6; :: according to EXCHSORT:def_14 ::_thesis: ( ( for a being ordinal number st a in dom C holds C . a is array of O ) & ( for a being ordinal number st a in dom C & succ a in dom C holds ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) ) hereby ::_thesis: for a being ordinal number st a in dom C & succ a in dom C holds ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) let b be ordinal number ; ::_thesis: ( b in dom C implies C . b is array of O ) assume b in dom C ; ::_thesis: C . b is array of O then a = b by A1, TARSKI:def_1; hence C . b is array of O by GRFUNC_1:6; ::_thesis: verum end; let b be ordinal number ; ::_thesis: ( b in dom C & succ b in dom C implies ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . b = R & C . (succ b) = Swap (R,x,y) ) ) assume ( b in dom C & succ b in dom C ) ; ::_thesis: ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . b = R & C . (succ b) = Swap (R,x,y) ) then ( a = b & a = succ b ) by A1, TARSKI:def_1; then a in a by ORDINAL1:6; hence ex R being array of O ex x, y being set st ( [x,y] in inversions R & C . b = R & C . (succ b) = Swap (R,x,y) ) ; ::_thesis: verum end; hence {[a,R]} is arr_computation of R ; ::_thesis: verum 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 for arr_computation of R; existence ex b1 being arr_computation of R st ( b1 is a -based & b1 is finite ) proof reconsider C = {[a,R]} as non empty finite a -based array ; C is arr_computation of R by Th75; hence ex b1 being arr_computation of R st ( b1 is a -based & b1 is finite ) ; ::_thesis: verum 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 ; clusterC . x -> Relation-like Function-like segmental ; coherence ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) proof percases ( x nin dom C or x in dom C ) ; suppose x nin dom C ; ::_thesis: ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) hence ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) by FUNCT_1:def_2; ::_thesis: verum end; suppose x in dom C ; ::_thesis: ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) hence ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) by Def14; ::_thesis: verum end; end; 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 ; clusterC . x -> the carrier of O -valued ; coherence C . x is the carrier of O -valued proof percases ( x nin dom C or x in dom C ) ; suppose x nin dom C ; ::_thesis: C . x is the carrier of O -valued then C . x = {} by FUNCT_1:def_2; then rng (C . x) = {} ; hence rng (C . x) c= the carrier of O by XBOOLE_1:2; :: according to RELAT_1:def_19 ::_thesis: verum end; suppose x in dom C ; ::_thesis: C . x is the carrier of O -valued hence C . x is the carrier of O -valued by Def14; ::_thesis: verum end; end; 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; 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 proof let O be non empty connected Poset; ::_thesis: 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 let R be array of O; ::_thesis: for C being 0 -based arr_computation of R st R is finite array of O holds C is finite let C be 0 -based arr_computation of R; ::_thesis: ( R is finite array of O implies C is finite ) assume R is finite array of O ; ::_thesis: C is finite then reconsider R = R as finite array of O ; A1: C . (base- C) = R by Def14; deffunc H1( array of O) -> set = card (inversions \$1); base- C = 0 by Th24; then A2: H1(C . 0) is finite by A1; A3: for a being ordinal number st succ a in dom C & H1(C . a) is finite holds H1(C . (succ a)) c< H1(C . a) proof let a be ordinal number ; ::_thesis: ( succ a in dom C & H1(C . a) is finite implies H1(C . (succ a)) c< H1(C . a) ) assume A4: ( succ a in dom C & H1(C . a) is finite ) ; ::_thesis: H1(C . (succ a)) c< H1(C . a) a in succ a by ORDINAL1:6; then a in dom C by A4, ORDINAL1:10; then consider R being array of O, x, y being set such that A5: ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) by A4, Def14; inversions R is finite by A4, A5; then H1(C . (succ a)) in H1(C . a) by A5, Th73; then ( H1(C . (succ a)) c= H1(C . a) & H1(C . (succ a)) <> H1(C . a) ) by ORDINAL1:def_2; hence H1(C . (succ a)) c< H1(C . a) by XBOOLE_0:def_8; ::_thesis: verum end; thus C is finite from EXCHSORT:sch_1(A2, A3); ::_thesis: verum 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 let O be non empty connected Poset; ::_thesis: 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 let R be array of O; ::_thesis: 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 let C be 0 -based arr_computation of R; ::_thesis: ( R is finite array of O & ( for a being ordinal number st inversions (C . a) <> {} holds succ a in dom C ) implies C is complete ) assume R is finite array of O ; ::_thesis: ( ex a being ordinal number st ( inversions (C . a) <> {} & not succ a in dom C ) or C is complete ) then C is finite by Th76; then reconsider d = dom C as non empty finite Ordinal ; assume A1: for a being ordinal number st inversions (C . a) <> {} holds succ a in dom C ; ::_thesis: C is complete set u = union d; consider n being Nat such that A2: d = n + 1 by NAT_1:6; A3: d = succ n by A2, NAT_1:38; then A4: union d = n by ORDINAL2:2; ( inversions (C . (union d)) <> 0 implies d in d ) by A1, A3, A4; hence last C is ascending by Th48; :: according to EXCHSORT:def_15 ::_thesis: verum 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 number st a in dom C holds C . a is permutation of R ) ) proof let O be non empty connected Poset; ::_thesis: 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 ) ) let R be array of O; ::_thesis: 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 ) ) let C be finite arr_computation of R; ::_thesis: ( last C is permutation of R & ( for a being ordinal number st a in dom C holds C . a is permutation of R ) ) consider a, b being ordinal number such that A1: dom C = a \ b by Def1; consider n being Nat such that A2: a = b +^ n by A1, Th7; defpred S9[ Nat] means ( b +^ \$1 in dom C implies C . (b +^ \$1) is permutation of R ); A3: b +^ 0 = b by ORDINAL2:27; then n <> 0 by A1, A2, XBOOLE_1:37; then consider m being Nat such that A4: n = m + 1 by NAT_1:6; A5: a = b +^ (succ m) by A2, A4, NAT_1:38 .= succ (b +^ m) by ORDINAL2:28 ; then A6: b +^ m = union a by ORDINAL2:2 .= union (a \ b) by A1, Th6 ; C . (base- C) = R by Def14; then C . b = R by A1, Th23; then A7: S9[ 0 ] by A3, Th38; A8: for k being Nat st S9[k] holds S9[k + 1] proof let k be Nat; ::_thesis: ( S9[k] implies S9[k + 1] ) assume A9: ( S9[k] & b +^ (k + 1) in dom C ) ; ::_thesis: C . (b +^ (k + 1)) is permutation of R k + 1 = succ k by NAT_1:38; then A10: b +^ (k + 1) = succ (b +^ k) by ORDINAL2:28; then ( b +^ k in b +^ (k + 1) & b +^ (k + 1) in a ) by A1, A9, ORDINAL1:6; then A11: ( b c= b +^ k & b +^ k in a ) by ORDINAL1:10, ORDINAL3:24; then b +^ k in dom C by A1, ORDINAL6:5; then consider Q being array of O, x, y being set such that A12: ( [x,y] in inversions Q & C . (b +^ k) = Q & C . (b +^ (k + 1)) = Swap (Q,x,y) ) by A9, A10, Def14; ( x in dom Q & y in dom Q ) by A12, Th46; then Swap (Q,x,y) is permutation of Q by Th43; hence C . (b +^ (k + 1)) is permutation of R by A9, A1, A11, A12, Th40, ORDINAL6:5; ::_thesis: verum end; A13: for k being Nat holds S9[k] from NAT_1:sch_2(A7, A8); ( b c= b +^ m & b +^ m in a ) by A5, ORDINAL1:6, ORDINAL3:24; then ( S9[m] & b +^ m in dom C ) by A1, A13, ORDINAL6:5; hence last C is permutation of R by A1, A6; ::_thesis: for a being ordinal number st a in dom C holds C . a is permutation of R let c be ordinal number ; ::_thesis: ( c in dom C implies C . c is permutation of R ) assume A14: c in dom C ; ::_thesis: C . c is permutation of R then A15: ( b c= c & c in a ) by A1, ORDINAL6:5; then c = b +^ (c -^ b) by ORDINAL3:def_5; then c -^ b in n by A2, A14, A1, ORDINAL3:22; then reconsider k = c -^ b as Nat ; S9[k] by A13; hence C . c is permutation of R by A14, A15, ORDINAL3:def_5; ::_thesis: verum end; 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 proof let X be set ; ::_thesis: for A being finite 0 -based array of X st A <> {} holds last A in X let A be finite 0 -based array of X; ::_thesis: ( A <> {} implies last A in X ) assume A <> {} ; ::_thesis: last A in X then consider n being Nat such that A1: dom A = n + 1 by NAT_1:6; n + 1 = succ n by NAT_1:38; then ( n in dom A & union (dom A) = n ) by A1, ORDINAL1:6, ORDINAL2:2; hence last A in X by FUNCT_1:102; ::_thesis: verum end; theorem Th80: :: EXCHSORT:80 for x being set holds last <%x%> = x proof let x be set ; ::_thesis: last <%x%> = x dom <%x%> = succ 0 by AFINSQ_1:def_4; then union (dom <%x%>) = 0 by ORDINAL2:2; hence last <%x%> = x by AFINSQ_1:def_4; ::_thesis: verum end; theorem Th81: :: EXCHSORT:81 for x being set for A being finite 0 -based array holds last (A ^ <%x%>) = x proof let x be set ; ::_thesis: for A being finite 0 -based array holds last (A ^ <%x%>) = x let A be finite 0 -based array; ::_thesis: last (A ^ <%x%>) = x dom <%x%> = 1 by AFINSQ_1:def_4; then dom (A ^ <%x%>) = (dom A) +^ 1 by ORDINAL4:def_1 .= succ (dom A) by ORDINAL2:31 ; then union (dom (A ^ <%x%>)) = len A by ORDINAL2:2; hence last (A ^ <%x%>) = x by AFINSQ_1:36; ::_thesis: verum end; 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) ) proof set D = F2() ^omega ; reconsider s0 = F3() as Element of F2() by A1; reconsider f0 = <%s0%> as Element of F2() ^omega by AFINSQ_1:42; defpred S9[ set , Element of F2() ^omega , Element of F2() ^omega ] means ( ( ( \$2 = {} or F1((last \$2)) = {} ) implies \$2 = \$3 ) & ( \$2 <> {} & F1((last \$2)) <> {} implies ex y being Element of F2() st ( P1[ last \$2,y] & F1(y) c< F1((last \$2)) & \$2 ^ <%y%> = \$3 ) ) ); A4: for a being Element of NAT for x being Element of F2() ^omega ex y being Element of F2() ^omega st S9[a,x,y] proof let a be Element of NAT ; ::_thesis: for x being Element of F2() ^omega ex y being Element of F2() ^omega st S9[a,x,y] let x be Element of F2() ^omega ; ::_thesis: ex y being Element of F2() ^omega st S9[a,x,y] percases ( x = {} or F1((last x)) = {} or ( x <> {} & F1((last x)) <> {} ) ) ; supposeA5: ( x = {} or F1((last x)) = {} ) ; ::_thesis: ex y being Element of F2() ^omega st S9[a,x,y] take y = x; ::_thesis: S9[a,x,y] thus S9[a,x,y] by A5; ::_thesis: verum end; supposeA6: ( x <> {} & F1((last x)) <> {} ) ; ::_thesis: ex y being Element of F2() ^omega st S9[a,x,y] then last x in F2() by Th79; then consider y being Element of F2() such that A7: ( P1[ last x,y] & F1(y) c< F1((last x)) ) by A3, A6; reconsider z = x ^ <%y%> as Element of F2() ^omega by AFINSQ_1:42; take z ; ::_thesis: S9[a,x,z] thus S9[a,x,z] by A6, A7; ::_thesis: verum end; end; end; consider F being Function of NAT,(F2() ^omega) such that A8: ( F . 0 = f0 & ( for a being Element of NAT holds S9[a,F . a,F . (a + 1)] ) ) from RECDEF_1:sch_2(A4); defpred S10[ Nat] means F . \$1 <> {} ; A9: S10[ 0 ] by A8; A10: for m being Nat st S10[m] holds S10[m + 1] proof let m be Nat; ::_thesis: ( S10[m] implies S10[m + 1] ) assume S10[m] ; ::_thesis: S10[m + 1] then reconsider f = F . m as non empty T-Sequence ; m in NAT by ORDINAL1:def_12; then S9[m,F . m,F . (m + 1)] by A8; then ( F . (m + 1) = f or ex x being set st F . (m + 1) = f ^ <%x%> ) ; hence S10[m + 1] ; ::_thesis: verum end; A11: for m being Nat holds S10[m] from NAT_1:sch_2(A9, A10); defpred S11[ Function] means ( \$1 . 0 = F3() & ( for a being ordinal number st succ a in dom \$1 holds ex x, y being Element of F2() st ( x = \$1 . a & y = \$1 . (succ a) & P1[x,y] ) ) ); defpred S12[ Nat] means S11[F . \$1]; A12: S12[ 0 ] proof thus (F . 0) . 0 = F3() by A8, AFINSQ_1:def_4; ::_thesis: for a being ordinal number st succ a in dom (F . 0) holds ex x, y being Element of F2() st ( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] ) let a be ordinal number ; ::_thesis: ( succ a in dom (F . 0) implies ex x, y being Element of F2() st ( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] ) ) assume succ a in dom (F . 0) ; ::_thesis: ex x, y being Element of F2() st ( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] ) then succ a in 1 by A8, AFINSQ_1:def_4; hence ex x, y being Element of F2() st ( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] ) by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; A13: for m being Nat st S12[m] holds S12[m + 1] proof let m be Nat; ::_thesis: ( S12[m] implies S12[m + 1] ) assume A14: S12[m] ; ::_thesis: S12[m + 1] A15: m in NAT by ORDINAL1:def_12; then A16: S9[m,F . m,F . (m + 1)] by A8; percases ( F . m = {} or F1((last (F . m))) = {} or ( F . m <> {} & F1((last (F . m))) <> {} ) ) ; suppose ( F . m = {} or F1((last (F . m))) = {} ) ; ::_thesis: S12[m + 1] hence S12[m + 1] by A14, A16; ::_thesis: verum end; supposeA17: ( F . m <> {} & F1((last (F . m))) <> {} ) ; ::_thesis: S12[m + 1] reconsider fm = F . m as non empty finite T-Sequence of by A17; reconsider fm1 = F . (m + 1) as finite T-Sequence of ; consider y being Element of F2() such that A18: ( P1[ last fm,y] & F1(y) c< F1((last fm)) & fm ^ <%y%> = F . (m + 1) ) by A8, A15, A17; 0 in dom fm by ORDINAL3:8; hence (F . (m + 1)) . 0 = F3() by A14, A18, ORDINAL4:def_1; ::_thesis: for a being ordinal number st succ a in dom (F . (m + 1)) holds ex x, y being Element of F2() st ( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] ) let a be ordinal number ; ::_thesis: ( succ a in dom (F . (m + 1)) implies ex x, y being Element of F2() st ( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] ) ) assume A19: succ a in dom (F . (m + 1)) ; ::_thesis: ex x, y being Element of F2() st ( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] ) A20: a in succ a by ORDINAL1:6; then A21: a in dom fm1 by A19, ORDINAL1:10; reconsider n = a as Nat by A19, A20; reconsider x = fm1 . a, z = fm1 . (succ a) as Element of F2() by A19, A21, FUNCT_1:102; A22: dom <%y%> = 1 by AFINSQ_1:def_4; then dom fm1 = (dom fm) +^ 1 by A18, ORDINAL4:def_1 .= succ (dom fm) by ORDINAL2:31 ; then A23: a in dom fm by A19, ORDINAL3:3; take x ; ::_thesis: ex y being Element of F2() st ( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] ) take z ; ::_thesis: ( x = (F . (m + 1)) . a & z = (F . (m + 1)) . (succ a) & P1[x,z] ) thus ( x = (F . (m + 1)) . a & z = (F . (m + 1)) . (succ a) ) ; ::_thesis: P1[x,z] percases ( succ a in dom fm or dom fm c= succ a ) by ORDINAL6:4; supposeA24: succ a in dom fm ; ::_thesis: P1[x,z] then a in dom fm by A20, ORDINAL1:10; then A25: ( x = fm . a & z = fm . (succ a) ) by A18, A24, ORDINAL4:def_1; ex x, y being Element of F2() st ( x = fm . a & y = fm . (succ a) & P1[x,y] ) by A14, A24; hence P1[x,z] by A25; ::_thesis: verum end; supposeA26: dom fm c= succ a ; ::_thesis: P1[x,z] succ a c= dom fm by A23, ORDINAL1:21; then A27: dom fm = succ a by A26, XBOOLE_0:def_10; then union (dom fm) = a by ORDINAL2:2; then A28: last fm = fm1 . a by A18, A23, ORDINAL4:def_1; ( 0 in 1 & (succ a) +^ 0 = succ a ) by NAT_1:44, ORDINAL2:27; then z = <%y%> . 0 by A22, A18, A27, ORDINAL4:def_1; hence P1[x,z] by A18, A28, AFINSQ_1:def_4; ::_thesis: verum end; end; end; end; end; A29: for m being Nat holds S12[m] from NAT_1:sch_2(A12, A13); defpred S13[ Nat] means ex n being Nat st card F1((last (F . n))) = \$1; A30: ex n being Nat st S13[n] proof last f0 = s0 by Th80; then reconsider n = card F1((last (F . 0))) as Nat by A2, A8; take n ; ::_thesis: S13[n] thus S13[n] ; ::_thesis: verum end; A31: for n being Nat st n <> 0 & S13[n] holds ex m being Nat st ( m < n & S13[m] ) proof let n be Nat; ::_thesis: ( n <> 0 & S13[n] implies ex m being Nat st ( m < n & S13[m] ) ) assume A32: n <> 0 ; ::_thesis: ( not S13[n] or ex m being Nat st ( m < n & S13[m] ) ) given k being Nat such that A33: card F1((last (F . k))) = n ; ::_thesis: ex m being Nat st ( m < n & S13[m] ) reconsider fk = F . k, fk1 = F . (k + 1) as Element of F2() ^omega ; k in NAT by ORDINAL1:def_12; then ( S9[k,fk,fk1] & fk <> {} ) by A11, A8; then consider y being Element of F2() such that A34: ( P1[ last fk,y] & F1(y) c< F1((last fk)) & fk ^ <%y%> = fk1 ) by A32, A33; A35: ( F1((last fk)) is finite & F1(y) c= F1((last fk)) ) by A33, A34, XBOOLE_0:def_8; A36: last fk1 = y by A34, Th81; then reconsider m = card F1((last fk1)) as Nat by A35; take m ; ::_thesis: ( m < n & S13[m] ) thus m < n by A33, A34, A35, A36, TREES_1:6; ::_thesis: S13[m] thus S13[m] ; ::_thesis: verum end; S13[ 0 ] from NAT_1:sch_7(A30, A31); then consider n being Nat such that A37: card F1((last (F . n))) = 0 ; reconsider f = F . n as non empty XFinSequence of by A11; take f ; ::_thesis: 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] ) ) ) reconsider k = last f as Element of F2() by Th79; take k ; ::_thesis: ( 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] ) ) ) thus ( k = last f & F1(k) = {} ) by A37; ::_thesis: ( 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] ) ) ) thus S11[f] by A29; ::_thesis: verum end; theorem Th82: :: EXCHSORT:82 for A being array for B being permutation of A holds B in Funcs ((dom A),(rng A)) proof let A be array; ::_thesis: for B being permutation of A holds B in Funcs ((dom A),(rng A)) let B be permutation of A; ::_thesis: B in Funcs ((dom A),(rng A)) ( dom B = dom A & rng B = rng A ) by Th37; hence B in Funcs ((dom A),(rng A)) by FUNCT_2:def_2; ::_thesis: verum end; 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 proof let B be permutation of A; ::_thesis: B is real-valued ex f being Permutation of (dom A) st B = A * f by Def9; hence B is real-valued ; ::_thesis: verum end; 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 proof let x be Element of Funcs (a,X); ::_thesis: x is T-Sequence-like dom x = a by FUNCT_2:92; hence x is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum end; 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 proof let B be permutation of A; ::_thesis: B is X -valued ex f being Permutation of (dom A) st B = A * f by Def9; hence B is X -valued ; ::_thesis: verum end; 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 proof let f be Element of Funcs (X,Y); ::_thesis: f is Z -valued percases ( f = {} or Funcs (X,Y) <> {} ) by SUBSET_1:def_1; suppose f = {} ; ::_thesis: f is Z -valued then rng f = {} ; hence rng f c= Z by XBOOLE_1:2; :: according to RELAT_1:def_19 ::_thesis: verum end; suppose Funcs (X,Y) <> {} ; ::_thesis: f is Z -valued then rng f c= Y by FUNCT_2:92; hence rng f c= Z by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum end; end; 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 let X, Y be set ; ::_thesis: for r being X -defined Y -valued Relation holds r is Relation of X,Y let r be X -defined Y -valued Relation; ::_thesis: r is Relation of X,Y ( [:(dom r),(rng r):] c= [:X,Y:] & r c= [:(dom r),(rng r):] ) by RELAT_1:7, ZFMISC_1:96; hence r is Relation of X,Y by XBOOLE_1:1; ::_thesis: verum 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 number st x = succ b ) proof let a be finite Ordinal; ::_thesis: for x being set holds ( not x in a or x = 0 or ex b being ordinal number st x = succ b ) let x be set ; ::_thesis: ( not x in a or x = 0 or ex b being ordinal number st x = succ b ) assume A1: ( x in a & x <> 0 ) ; ::_thesis: ex b being ordinal number st x = succ b then A2: {} in x by ORDINAL3:8; now__::_thesis:_not_x_is_limit_ordinal assume x is limit_ordinal ; ::_thesis: contradiction then ( omega c= x & x c= a ) by A1, A2, ORDINAL1:def_2, ORDINAL1:def_11; hence contradiction ; ::_thesis: verum end; hence ex b being ordinal number st x = succ b by A1, ORDINAL1:29; ::_thesis: verum 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 proof let O be non empty connected Poset; ::_thesis: for A being non empty finite 0 -based array of O ex C being 0 -based arr_computation of A st C is complete let A be non empty finite 0 -based array of O; ::_thesis: ex C being 0 -based arr_computation of A st C is complete reconsider rA = rng A as non empty Subset of O by RELAT_1:def_19; reconsider a = dom A as Ordinal ; set X = Funcs (a,rA); deffunc H1( array of O) -> set = card (inversions \$1); defpred S9[ Element of Funcs (a,rA), Element of Funcs (a,rA)] means ex p, q being Element of dom A st ( [p,q] in inversions \$1 & \$2 = Swap (\$1,p,q) ); A is permutation of A by Th38; then A1: A in Funcs (a,rA) by Th82; A2: H1(A) is finite ; A3: for x being Element of Funcs (a,rA) st H1(x) <> {} holds ex y being Element of Funcs (a,rA) st ( S9[x,y] & H1(y) c< H1(x) ) proof let x be Element of Funcs (a,rA); ::_thesis: ( H1(x) <> {} implies ex y being Element of Funcs (a,rA) st ( S9[x,y] & H1(y) c< H1(x) ) ) reconsider c = x as array of O ; set z = the Element of inversions c; set Fx = H1(x); assume H1(x) <> {} ; ::_thesis: ex y being Element of Funcs (a,rA) st ( S9[x,y] & H1(y) c< H1(x) ) then A4: inversions c <> {} ; then ( the Element of inversions c in inversions c & inversions c is Relation of (dom x),(dom x) ) by Th47; then consider p, q being set such that A5: ( the Element of inversions c = [p,q] & p in dom x & q in dom x ) by RELSET_1:2; set y = Swap (x,p,q); A6: ( dom (Swap (x,p,q)) = dom x & rng (Swap (x,p,q)) = rng x ) by FUNCT_7:99, FUNCT_7:103; ( dom x = dom A & rng x c= rng A ) by FUNCT_2:92; then reconsider y = Swap (x,p,q) as Element of Funcs (a,rA) by A6, FUNCT_2:def_2; reconsider b = y as array of O ; set Fy = H1(y); take y ; ::_thesis: ( S9[x,y] & H1(y) c< H1(x) ) thus S9[x,y] by A4, A5; ::_thesis: H1(y) c< H1(x) H1(b) in H1(c) by A4, A5, Th73; hence ( H1(y) c= H1(x) & H1(y) <> H1(x) ) by ORDINAL1:def_2; :: according to XBOOLE_0:def_8 ::_thesis: verum end; consider f being non empty finite 0 -based array, k being Element of Funcs (a,rA) such that A7: ( k = last f & H1(k) = {} & f . 0 = A ) and A8: for a being ordinal number st succ a in dom f holds ex x, y being Element of Funcs (a,rA) st ( x = f . a & y = f . (succ a) & S9[x,y] ) from EXCHSORT:sch_2(A1, A2, A3); f is arr_computation of A proof thus f . (base- f) = A by A7, Th24; :: according to EXCHSORT:def_14 ::_thesis: ( ( for a being ordinal number st a in dom f holds f . a is array of O ) & ( for a being ordinal number st a in dom f & succ a in dom f holds ex R being array of O ex x, y being set st ( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) ) ) ) thus for a being ordinal number st a in dom f holds f . a is array of O ::_thesis: for a being ordinal number st a in dom f & succ a in dom f holds ex R being array of O ex x, y being set st ( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) ) proof let a be ordinal number ; ::_thesis: ( a in dom f implies f . a is array of O ) assume A9: a in dom f ; ::_thesis: f . a is array of O percases ( a = 0 or ex b being ordinal number st a = succ b ) by A9, Th84; suppose a = 0 ; ::_thesis: f . a is array of O hence f . a is array of O by A7; ::_thesis: verum end; suppose ex b being ordinal number st a = succ b ; ::_thesis: f . a is array of O then consider b being ordinal number such that A10: a = succ b ; ex x, y being Element of Funcs (a,rA) st ( x = f . b & y = f . a & S9[x,y] ) by A8, A9, A10; hence f . a is array of O ; ::_thesis: verum end; end; end; let a be ordinal number ; ::_thesis: ( a in dom f & succ a in dom f implies ex R being array of O ex x, y being set st ( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) ) ) assume ( a in dom f & succ a in dom f ) ; ::_thesis: ex R being array of O ex x, y being set st ( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) ) then ex x, y being Element of Funcs (a,rA) st ( x = f . a & y = f . (succ a) & S9[x,y] ) by A8; hence ex R being array of O ex x, y being set st ( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) ) ; ::_thesis: verum end; then reconsider f = f as 0 -based arr_computation of A ; take f ; ::_thesis: f is complete inversions (last f) = {} by A7; hence last f is ascending by Th48; :: according to EXCHSORT:def_15 ::_thesis: verum 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 proof let O be non empty connected Poset; ::_thesis: for A being non empty finite 0 -based array of O ex B being permutation of A st B is ascending let A be non empty finite 0 -based array of O; ::_thesis: ex B being permutation of A st B is ascending consider C being 0 -based arr_computation of A such that A1: C is complete by Th85; C is finite by Th76; then reconsider B = last C as permutation of A by Th78; take B ; ::_thesis: B is ascending thus B is ascending by A1, Def15; ::_thesis: verum 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 for permutation of A; existence ex b1 being permutation of A st b1 is ascending proof A1: A is permutation of A by Th38; ( A is empty implies A is ascending ) ; hence ex b1 being permutation of A st b1 is ascending by A1, Th86; ::_thesis: verum end; end;