begin
theorem
theorem
theorem
theorem
Lm1:
for j, i being Nat holds (j -' i) -' 1 = (j -' 1) -' i
begin
:: deftheorem Def1 defines Replace FINSEQ_7:def 1 :
for D being non empty set
for f being FinSequence of D
for i being Nat
for p being Element of D holds
( ( 1 <= i & i <= len f implies Replace f,i,p = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) & ( ( not 1 <= i or not i <= len f ) implies Replace f,i,p = f ) );
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
Lm2:
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace f,i,p) . i = p
theorem
theorem
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
begin
definition
let D be non
empty set ;
let f be
FinSequence of
D;
let i,
j be
Nat;
Swapredefine func Swap f,
i,
j -> FinSequence of
D equals :
Def2:
Replace (Replace f,i,(f /. j)),
j,
(f /. i) if ( 1
<= i &
i <= len f & 1
<= j &
j <= len f )
otherwise f;
coherence
Swap f,i,j is FinSequence of D
compatibility
for b1 being FinSequence of D holds
( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( b1 = Swap f,i,j iff b1 = Replace (Replace f,i,(f /. j)),j,(f /. i) ) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( b1 = Swap f,i,j iff b1 = f ) ) )
correctness
consistency
for b1 being FinSequence of D holds verum;
;
end;
:: deftheorem Def2 defines Swap FINSEQ_7:def 2 :
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds
( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap f,i,j = Replace (Replace f,i,(f /. j)),j,(f /. i) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies Swap f,i,j = f ) );
theorem Th20:
Lm3:
for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i )
theorem Th21:
theorem
theorem Th23:
theorem
theorem
theorem
theorem
theorem
theorem Th29:
theorem
theorem
Lm4:
for D being non empty set
for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k holds
(Swap f,i,j) . k = f . k
theorem Th32:
theorem Th33:
begin
theorem Th34:
theorem Th35:
for
D being non
empty set for
f being
FinSequence of
D for
p being
Element of
D for
i,
k,
j being
Nat st
i <> k &
j <> k & 1
<= i &
i <= len f & 1
<= j &
j <= len f holds
Swap (Replace f,k,p),
i,
j = Replace (Swap f,i,j),
k,
p
theorem
for
D being non
empty set for
f being
FinSequence of
D for
i,
k,
j being
Nat st
i <> k &
j <> k & 1
<= i &
i <= len f & 1
<= j &
j <= len f & 1
<= k &
k <= len f holds
Swap (Swap f,i,j),
j,
k = Swap (Swap f,i,k),
i,
j
theorem
for
D being non
empty set for
f being
FinSequence of
D for
i,
k,
j,
l being
Nat st
i <> k &
j <> k &
l <> i &
l <> j & 1
<= i &
i <= len f & 1
<= j &
j <= len f & 1
<= k &
k <= len f & 1
<= l &
l <= len f holds
Swap (Swap f,i,j),
k,
l = Swap (Swap f,k,l),
i,
j