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 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 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 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 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 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;
d = Segm (n + 1) by A2;
then A3: d = succ (Segm n) by 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