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 H₁( array of O) -> set = card (inversions $1);
defpred S₉[ 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: H₁(A) is finite ;
A3: for x being Element of Funcs (a,rA) st H₁(x) <> {} holds
ex y being Element of Funcs (a,rA) st
( S₉[x,y] & H₁(y) c< H₁(x) )

proof

let x be Element of Funcs (a,rA); :: thesis: ( H₁(x) <> {} implies ex y being Element of Funcs (a,rA) st
( S₉[x,y] & H₁(y) c< H₁(x) ) )
reconsider c = x as array of O ;
set z = the Element of inversions c;
set Fx = H₁(x);
assume H₁(x) <> {} ; :: thesis: ex y being Element of Funcs (a,rA) st
( S₉[x,y] & H₁(y) c< H₁(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 = H₁(y);
take y ; :: thesis: ( S₉[x,y] & H₁(y) c< H₁(x) )
thus S₉[x,y] by A4, A5; :: thesis: H₁(y) c< H₁(x)
H₁(b) in H₁(c) by A4, A5, Th73;
hence ( H₁(y) c= H₁(x) & H₁(y) <> H₁(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 & H₁(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) & S₉[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 & S₉[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) & S₉[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