let O be non empty connected Poset; :: thesis: for R being array of O
for C being finite arr_computation of R holds
( last C is permutation of R & ( for a being Ordinal st a in dom C holds
C . a is permutation of R ) )
let R be array of O; :: thesis: for C being finite arr_computation of R holds
( last C is permutation of R & ( for a being Ordinal st a in dom C holds
C . a is permutation of R ) )
let C be finite arr_computation of R; :: thesis: ( last C is permutation of R & ( for a being Ordinal st a in dom C holds
C . a is permutation of R ) )
consider a, b being Ordinal such that
A1: dom C = a \ b by Def1;
consider n being Nat such that
A2: a = b +^ n by A1, Th7;
defpred S₉[ Nat] means ( b +^ $1 in dom C implies C . (b +^ $1) is permutation of R );
A3: b +^ 0 = b by ORDINAL2:27;
then n <> 0 by A1, A2, XBOOLE_1:37;
then consider m being Nat such that
A4: n = m + 1 by NAT_1:6;
n = Segm (m + 1) by A4;
then A5: a = b +^ (succ (Segm m)) by A2, NAT_1:38
.= succ (b +^ m) by ORDINAL2:28 ;
then A6: b +^ m = union a by ORDINAL2:2
.= union (a \ b) by A1, Th6 ;
C . (base- C) = R by Def14;
then C . b = R by A1, Th23;
then A7: S₉[ 0 ] by A3, Th38;
A8: for k being Nat st S₉[k] holds
S₉[k + 1]

proof

let k be Nat; :: thesis: ( S₉[k] implies S₉[k + 1] )
assume A9: ( S₉[k] & b +^ (k + 1) in dom C ) ; :: thesis: C . (b +^ (k + 1)) is permutation of R
Segm (k + 1) = succ (Segm k) by NAT_1:38;
then A10: b +^ (k + 1) = succ (b +^ k) by ORDINAL2:28;
then ( b +^ k in b +^ (k + 1) & b +^ (k + 1) in a ) by A1, A9, ORDINAL1:6;
then A11: ( b c= b +^ k & b +^ k in a ) by ORDINAL1:10, ORDINAL3:24;
then b +^ k in dom C by A1, ORDINAL6:5;
then consider Q being array of O, x, y being set such that
A12: ( [x,y] in inversions Q & C . (b +^ k) = Q & C . (b +^ (k + 1)) = Swap (Q,x,y) ) by A9, A10, Def14;
( x in dom Q & y in dom Q ) by A12, Th46;
then Swap (Q,x,y) is permutation of Q by Th43;
hence C . (b +^ (k + 1)) is permutation of R by A9, A1, A11, A12, Th40, ORDINAL6:5; :: thesis: verum

end;

A13: for k being Nat holds S₉[k] from NAT_1:sch 2(A7, A8);
( b c= b +^ m & b +^ m in a ) by A5, ORDINAL1:6, ORDINAL3:24;
then ( S₉[m] & b +^ m in dom C ) by A1, A13, ORDINAL6:5;
hence last C is permutation of R by A1, A6; :: thesis: for a being Ordinal st a in dom C holds
C . a is permutation of R
let c be Ordinal; :: thesis: ( c in dom C implies C . c is permutation of R )
assume A14: c in dom C ; :: thesis: C . c is permutation of R
then A15: ( b c= c & c in a ) by A1, ORDINAL6:5;
then c = b +^ (c -^ b) by ORDINAL3:def 5;
then c -^ b in n by A2, A14, A1, ORDINAL3:22;
then c -^ b in Segm n ;
then reconsider k = c -^ b as Nat ;
S₉[k] by A13;
hence C . c is permutation of R by A14, A15, ORDINAL3:def 5; :: thesis: verum