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 MAIN4;
then reconsider d = dom C as non empty finite Ordinal ;
assume Z1: 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
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;
( inversions (C . (union d)) <> 0 implies d in d ) by Z1, A4, A5;
hence last C is ascending by SORT; :: according to EXCHSORT:def 15 :: thesis: verum