let O be non empty connected Poset; 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; 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; ( 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 S9[ 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:
S9[ 0 ]
by A3, Th38;
A8:
for k being Nat st S9[k] holds
S9[k + 1]
proof
let k be
Nat;
( S9[k] implies S9[k + 1] )
assume A9:
(
S9[
k] &
b +^ (k + 1) in dom C )
;
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;
verum
end;
A13:
for k being Nat holds S9[k]
from NAT_1:sch 2(A7, A8);
( b c= b +^ m & b +^ m in a )
by A5, ORDINAL1:6, ORDINAL3:24;
then
( S9[m] & b +^ m in dom C )
by A1, A13, ORDINAL6:5;
hence
last C is permutation of R
by A1, A6; for a being Ordinal st a in dom C holds
C . a is permutation of R
let c be Ordinal; ( c in dom C implies C . c is permutation of R )
assume A14:
c in dom C
; 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 ;
S9[k]
by A13;
hence
C . c is permutation of R
by A14, A15, ORDINAL3:def 5; verum