begin
Lm1:
for j, i being Nat holds (j -' i) -' 1 = (j -' 1) -' i
begin
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
begin
definition
let D be non
empty set ;
let f be
FinSequence of
D;
let i,
j be
Nat;
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;
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 )
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
begin
theorem Th33:
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)