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 ThRef;
then A0: A in Funcs (a,rA) by ThF;
A1: H₁(A) is finite ;
A2: 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 B0: inversions c <> {} ;
then ( the Element of inversions c in inversions c & inversions c is Relation of (dom x),(dom x) ) by TW1;
then consider p, q being set such that
B1: ( 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);
B2: ( 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 B2, 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 B0, B1; :: thesis: H₁(y) c< H₁(x)
H₁(b) in H₁(c) by B0, B1, MAIN3;
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
A3: ( k = last f & H₁(k) = {} & f . 0 = A ) and
A4: 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) & S₉[x,y] ) from EXCHSORT:sch 2(A0, A1, A2);
f is arr_computation of A

proof

thus f . (base- f) = A by A3, TT0; :: 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 Z1: a in dom f ; :: thesis: f . a is array of O

per cases ( a = 0 or ex b being ordinal number st a = succ b ) by Z1, Lem1;

suppose a = 0 ; :: thesis: f . a is array of O

hence f . a is array of O by A3; :: 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
Z2: a = succ b ;
ex x, y being Element of Funcs (a,rA) st
( x = f . b & y = f . a & S₉[x,y] ) by A4, Z1, Z2;
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) & S₉[x,y] ) by A4;
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 A3;
hence last f is ascending by SORT; :: according to EXCHSORT:def 15 :: thesis: verum