environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FINSEQ_1, SUBSET_1, NAT_1, XXREAL_0, ARYTM_3, RELAT_1, ARYTM_1, ORDINAL4, FUNCT_1, RFINSEQ, PARTFUN1, CARD_1, AFINSQ_1, FUNCT_4, TARSKI, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, RFINSEQ, FUNCT_7, XXREAL_0;
definitions FINSEQ_1;
theorems NAT_1, FINSEQ_1, FINSEQ_3, FINSEQ_5, FINSEQ_6, RFINSEQ, INT_1, GENEALG1, FUNCT_7, XREAL_1, XXREAL_0, ORDINAL1, NAT_2, PARTFUN1, NAT_D, XREAL_0;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, FUNCT_7, ORDINAL1, NAT_1;
constructors HIDDEN, PARTFUN1, FUNCT_4, XXREAL_0, REAL_1, NAT_1, INT_1, FINSEQ_4, RFINSEQ, NAT_D, FUNCT_7, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_1;
expansions FINSEQ_1;
Lm1:
for i, j being Nat holds (j -' i) -' 1 = (j -' 1) -' i
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
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, j, k being Nat st i <> k & j <> k holds
(Swap (f,i,j)) . k = f . k
theorem Th33:
for
D being non
empty set for
f being
FinSequence of
D for
p being
Element of
D for
i,
j,
k 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,
j,
k 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,
j,
k,
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)