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 object 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 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 st a in dom f holds
f . a is array of O ) & ( for a being Ordinal 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 st a in dom f holds
f . a is array of O :: thesis: for a being Ordinal 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; :: 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
per cases ( a = 0 or ex b being Ordinal 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 st a = succ b ; :: thesis: f . a is array of O
then consider b being Ordinal 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; :: 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