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 holds
C is finite
let R be array of O; :: thesis: for C being 0 -based arr_computation of R st R is finite array of O holds
C is finite
let C be 0 -based arr_computation of R; :: thesis: ( R is finite array of O implies C is finite )
assume R is finite array of O ; :: thesis: C is finite
then reconsider R = R as finite array of O ;
A1: C . (base- C) = R by Def14;
deffunc H1( array of O) -> set = card (inversions $1);
base- C = 0 by Th24;
then A2: H1(C . 0) is finite by A1;
A3: for a being Ordinal st succ a in dom C & H1(C . a) is finite holds
H1(C . (succ a)) c< H1(C . a)
proof
let a be Ordinal; :: thesis: ( succ a in dom C & H1(C . a) is finite implies H1(C . (succ a)) c< H1(C . a) )
assume A4: ( succ a in dom C & H1(C . a) is finite ) ; :: thesis: H1(C . (succ a)) c< H1(C . a)
a in succ a by ORDINAL1:6;
then a in dom C by A4, ORDINAL1:10;
then consider R being array of O, x, y being set such that
A5: ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) by A4, Def14;
inversions R is finite by A4, A5;
then H1(C . (succ a)) in H1(C . a) by A5, Th73;
then ( H1(C . (succ a)) c= H1(C . a) & H1(C . (succ a)) <> H1(C . a) ) by ORDINAL1:def 2;
hence H1(C . (succ a)) c< H1(C . a) ; :: thesis: verum
end;
thus C is finite from EXCHSORT:sch 1(A2, A3); :: thesis: verum