:: On Replace Function and Swap Function for Finite Sequences
:: by Hiroshi Yamazaki , Yoshinori Fujisawa and Yatsuka Nakamura
::
:: Received August 28, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: FINSEQ_7:1
theorem :: FINSEQ_7:2
theorem :: FINSEQ_7:3
theorem :: FINSEQ_7:4
Lm1:
for j, i being Nat holds (j -' i) -' 1 = (j -' 1) -' i
:: deftheorem Def1 defines Replace FINSEQ_7:def 1 :
theorem :: FINSEQ_7:5
canceled;
theorem :: FINSEQ_7:6
canceled;
theorem Th7: :: FINSEQ_7:7
theorem :: FINSEQ_7:8
theorem :: FINSEQ_7:9
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 :: FINSEQ_7:10
theorem :: FINSEQ_7:11
theorem Th12: :: FINSEQ_7:12
theorem Th13: :: FINSEQ_7:13
theorem :: FINSEQ_7:14
theorem Th15: :: FINSEQ_7:15
theorem Th16: :: FINSEQ_7:16
theorem Th17: :: FINSEQ_7:17
theorem Th18: :: FINSEQ_7:18
theorem Th19: :: FINSEQ_7:19
definition
let D be non
empty set ;
let f be
FinSequence of
D;
let i,
j be
Nat;
:: original: Swapredefine func Swap f,
i,
j -> FinSequence of
D equals :
Def2:
:: FINSEQ_7:def 2
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 :
theorem Th20: :: FINSEQ_7:20
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: :: FINSEQ_7:21
theorem :: FINSEQ_7:22
theorem Th23: :: FINSEQ_7:23
theorem :: FINSEQ_7:24
theorem :: FINSEQ_7:25
theorem :: FINSEQ_7:26
theorem :: FINSEQ_7:27
theorem :: FINSEQ_7:28
theorem Th29: :: FINSEQ_7:29
theorem :: FINSEQ_7:30
theorem :: FINSEQ_7:31
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: :: FINSEQ_7:32
theorem Th33: :: FINSEQ_7:33
theorem Th34: :: FINSEQ_7:34
theorem Th35: :: FINSEQ_7:35
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 :: FINSEQ_7:36
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 :: FINSEQ_7:37
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