:: by Hiroshi Yamazaki , Yoshinori Fujisawa and Yatsuka Nakamura

::

:: Received August 28, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

theorem :: FINSEQ_7:1

for D being non empty set

for f being FinSequence of D

for i, j being Nat st 1 <= i & j <= len f & i < j holds

f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j)

for f being FinSequence of D

for i, j being Nat st 1 <= i & j <= len f & i < j holds

f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j)

proof end;

theorem :: FINSEQ_7:2

for i being Nat

for f, g, h being FinSequence st len g = len h & len g < i & i <= len (g ^ f) holds

(g ^ f) . i = (h ^ f) . i

for f, g, h being FinSequence st len g = len h & len g < i & i <= len (g ^ f) holds

(g ^ f) . i = (h ^ f) . i

proof end;

theorem :: FINSEQ_7:3

for i being Nat

for f, g being FinSequence st 1 <= i & i <= len f holds

f . i = (g ^ f) . ((len g) + i)

for f, g being FinSequence st 1 <= i & i <= len f holds

f . i = (g ^ f) . ((len g) + i)

proof end;

theorem :: FINSEQ_7:4

for D being non empty set

for f being FinSequence of D

for i, n being Nat st i in dom (f /^ n) holds

(f /^ n) . i = f . (n + i)

for f being FinSequence of D

for i, n being Nat st i in dom (f /^ n) holds

(f /^ n) . i = f . (n + i)

proof end;

Lm1: for j, i being Nat holds (j -' i) -' 1 = (j -' 1) -' i

proof end;

begin

notation

let D be non empty set ;

let f be FinSequence of D;

let i be Nat;

let p be Element of D;

synonym Replace (f,i,p) for D +* (f,i);

end;
let f be FinSequence of D;

let i be Nat;

let p be Element of D;

synonym Replace (f,i,p) for D +* (f,i);

definition

let D be non empty set ;

let f be FinSequence of D;

let i be Nat;

let p be Element of D;

for b_{1} being FinSequence of D holds

( ( 1 <= i & i <= len f implies ( b_{1} = Replace (i,p,) iff b_{1} = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b_{1} = Replace (i,p,) iff b_{1} = f ) ) )

coherence

Replace (i,p,) is FinSequence of D;

consistency

for b_{1} being FinSequence of D holds verum;

end;
let f be FinSequence of D;

let i be Nat;

let p be Element of D;

:: original: Replace

redefine func Replace (f,i,p) -> FinSequence of D equals :Def1: :: FINSEQ_7:def 1

((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) if ( 1 <= i & i <= len f )

otherwise f;

compatibility redefine func Replace (f,i,p) -> FinSequence of D equals :Def1: :: FINSEQ_7:def 1

((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) if ( 1 <= i & i <= len f )

otherwise f;

for b

( ( 1 <= i & i <= len f implies ( b

proof end;

correctness coherence

Replace (i,p,) is FinSequence of D;

consistency

for b

proof end;

:: 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 ) );

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 :: FINSEQ_7:5

for D being non empty set

for f being FinSequence of D

for p being Element of D

for i being Nat holds len (Replace (f,i,p)) = len f by FUNCT_7:97;

for f being FinSequence of D

for p being Element of D

for i being Nat holds len (Replace (f,i,p)) = len f by FUNCT_7:97;

theorem :: FINSEQ_7:6

theorem :: FINSEQ_7:7

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

p in rng (Replace (f,i,p))

for f being FinSequence of D

for p being Element of D

for i being Nat st 1 <= i & i <= len f holds

p in rng (Replace (f,i,p))

proof end;

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

proof end;

theorem :: FINSEQ_7:8

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

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

proof end;

theorem :: FINSEQ_7:9

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

for k being Nat st 0 < k & k <= (len f) - i holds

(Replace (f,i,p)) . (i + k) = (f /^ i) . k

for f being FinSequence of D

for p being Element of D

for i being Nat st 1 <= i & i <= len f holds

for k being Nat st 0 < k & k <= (len f) - i holds

(Replace (f,i,p)) . (i + k) = (f /^ i) . k

proof end;

theorem Th10: :: FINSEQ_7:10

for D being non empty set

for f being FinSequence of D

for p being Element of D

for k, i being Nat st 1 <= k & k <= len f & k <> i holds

(Replace (f,i,p)) /. k = f /. k

for f being FinSequence of D

for p being Element of D

for k, i being Nat st 1 <= k & k <= len f & k <> i holds

(Replace (f,i,p)) /. k = f /. k

proof end;

theorem Th11: :: FINSEQ_7:11

for D being non empty set

for f being FinSequence of D

for q, p being Element of D

for i, j being Nat st 1 <= i & i < j & j <= len f holds

Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j)

for f being FinSequence of D

for q, p being Element of D

for i, j being Nat st 1 <= i & i < j & j <= len f holds

Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j)

proof end;

theorem Th15: :: FINSEQ_7:15

for D being non empty set

for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*>

for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*>

proof end;

theorem Th16: :: FINSEQ_7:16

for D being non empty set

for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*>

for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*>

proof end;

theorem Th17: :: FINSEQ_7:17

for D being non empty set

for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*>

for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*>

proof end;

begin

registration

let f be FinSequence;

let i, j be Nat;

correctness

coherence

Swap (f,i,j) is FinSequence-like ;

end;
let i, j be Nat;

correctness

coherence

Swap (f,i,j) is FinSequence-like ;

proof end;

definition

let D be non empty set ;

let f be FinSequence of D;

let i, j be Nat;

Swap (f,i,j) is FinSequence of D

for b_{1} being FinSequence of D holds

( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( b_{1} = Swap (f,i,j) iff b_{1} = 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 ( b_{1} = Swap (f,i,j) iff b_{1} = f ) ) )

consistency

for b_{1} being FinSequence of D holds verum;

;

end;
let f be FinSequence of D;

let i, j be Nat;

:: original: Swap

redefine 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 redefine 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;

Swap (f,i,j) is FinSequence of D

proof end;

compatibility for b

( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( b

proof end;

correctness consistency

for b

;

:: 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 ) );

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 Th18: :: FINSEQ_7:18

for D being non empty set

for f being FinSequence of D

for i, j being Nat holds len (Swap (f,i,j)) = len f

for f being FinSequence of D

for i, j being Nat holds len (Swap (f,i,j)) = len f

proof 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 )

proof end;

theorem :: FINSEQ_7:20

for D being non empty set

for f being FinSequence of D

for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f

for f being FinSequence of D

for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f

proof end;

theorem Th21: :: FINSEQ_7:21

for D being non empty set

for f being FinSequence of D

for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i)

for f being FinSequence of D

for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i)

proof end;

theorem :: FINSEQ_7:22

for D being non empty set

for f being FinSequence of D

for i, j being Nat holds rng (Swap (f,i,j)) = rng f by FUNCT_7:103;

for f being FinSequence of D

for i, j being Nat holds rng (Swap (f,i,j)) = rng f by FUNCT_7:103;

theorem :: FINSEQ_7:24

for D being non empty set

for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*>

for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*>

proof end;

theorem :: FINSEQ_7:25

for D being non empty set

for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*>

for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*>

proof end;

theorem :: FINSEQ_7:26

for D being non empty set

for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*>

for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*>

proof end;

theorem Th27: :: FINSEQ_7:27

for D being non empty set

for f being FinSequence of D

for i, j being Nat st 1 <= i & i < j & j <= len f holds

Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)

for f being FinSequence of D

for i, j being Nat st 1 <= i & i < j & j <= len f holds

Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)

proof end;

theorem :: FINSEQ_7:28

for D being non empty set

for f being FinSequence of D

for i being Nat st 1 < i & i <= len f holds

Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)

for f being FinSequence of D

for i being Nat st 1 < i & i <= len f holds

Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)

proof end;

theorem :: FINSEQ_7:29

for D being non empty set

for f being FinSequence of D

for i being Nat st 1 <= i & i < len f holds

Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>

for f being FinSequence of D

for i being Nat st 1 <= i & i < len f holds

Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>

proof end;

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

proof end;

theorem Th30: :: FINSEQ_7:30

for D being non empty set

for f being FinSequence of D

for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds

(Swap (f,i,j)) /. k = f /. k

for f being FinSequence of D

for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds

(Swap (f,i,j)) /. k = f /. k

proof end;

theorem Th31: :: FINSEQ_7:31

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 )

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 )

proof end;

begin

theorem Th32: :: FINSEQ_7:32

for D being non empty set

for f being FinSequence of D

for p being Element of D

for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds

Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)

for f being FinSequence of D

for p being Element of D

for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds

Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)

proof end;

theorem Th33: :: FINSEQ_7:33

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)

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)

proof end;

theorem :: FINSEQ_7:34

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)

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)

proof end;

theorem :: FINSEQ_7:35

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)

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)

proof end;