:: Some Properties of Restrictions of Finite Sequences
:: by Czes\law Byli\'nski
::
:: Received January 25, 1995
:: Copyright (c) 1995-2011 Association of Mizar Users

begin

theorem Th1: :: FINSEQ_5:1

for i, n being Nat st i <= n holds
(n - i) + 1 is Element of NAT

proof end;

theorem Th2: :: FINSEQ_5:2

for i, n being Nat st i in Seg n holds
(n - i) + 1 in Seg n

proof end;

theorem Th3: :: FINSEQ_5:3

for f being Function
for x, y being set st f " {y} = {x} holds
( x in dom f & y in rng f & f . x = y )

proof end;

theorem :: FINSEQ_5:4

for f being Function holds
( f is one-to-one iff for x being set st x in dom f holds
f " {(f . x)} = {x} )

proof end;

theorem :: FINSEQ_5:5

for f being Function
for y1, y2 being set st f is one-to-one & y1 in rng f & f " {y1} = f " {y2} holds
y1 = y2

proof end;

registration

let x be set ;
cluster <*x*> -> trivial ;
coherence
<*x*> is trivial

proof end;

let y be set ;
cluster <*x,y*> -> non trivial ;
coherence
not <*x,y*> is trivial

proof end;

end;

registration

cluster non empty Relation-like Function-like one-to-one V31() FinSequence-like FinSubsequence-like set ;
existence
ex b₁ being FinSequence st
( b₁ is one-to-one & not b₁ is empty )

proof end;

end;

theorem Th6: :: FINSEQ_5:6

for f being non empty FinSequence holds
( 1 in dom f & len f in dom f )

proof end;

theorem :: FINSEQ_5:7

for f being non empty FinSequence ex i being Nat st i + 1 = len f by NAT_1:6;

theorem Th8: :: FINSEQ_5:8

for x being set
for f being FinSequence holds len (<*x*> ^ f) = 1 + (len f)

proof end;

theorem :: FINSEQ_5:9

canceled;

theorem :: FINSEQ_5:10

for f being FinSequence
for p, q being set st p in rng f & q in rng f & p .. f = q .. f holds
p = q

proof end;

theorem Th11: :: FINSEQ_5:11

for n being Nat
for f, g being FinSequence st n + 1 in dom f & g = f | (Seg n) holds
f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*>

proof end;

theorem Th12: :: FINSEQ_5:12

for i being Nat
for f being one-to-one FinSequence st i in dom f holds
(f . i) .. f = i

proof end;

registration

let D be non empty set ;
cluster non empty Relation-like D -valued Function-like one-to-one V31() FinSequence-like FinSubsequence-like FinSequence of D;
existence
ex b₁ being FinSequence of D st
( b₁ is one-to-one & not b₁ is empty )

proof end;

end;

theorem :: FINSEQ_5:13

for D being non empty set
for f, g being FinSequence of D st dom f = dom g & ( for i being Nat st i in dom f holds
f /. i = g /. i ) holds
f = g

proof end;

theorem Th14: :: FINSEQ_5:14

for D being non empty set
for f, g being FinSequence of D st len f = len g & ( for k being Nat st 1 <= k & k <= len f holds
f /. k = g /. k ) holds
f = g

proof end;

theorem Th15: :: FINSEQ_5:15

for D being non empty set
for f being FinSequence of D st len f = 1 holds
f = <*(f /. 1)*>

proof end;

theorem Th16: :: FINSEQ_5:16

for D being non empty set
for p being Element of D
for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p

proof end;

Lm1: for i being Nat
for D being non empty set
for f, g being FinSequence of D st i in dom f holds
(f ^ g) /. i = f /. i

proof end;

theorem :: FINSEQ_5:17

canceled;

theorem Th18: :: FINSEQ_5:18

for f being FinSequence
for i being Nat holds len (f | i) <= len f

proof end;

theorem Th19: :: FINSEQ_5:19

for f being FinSequence
for i being Nat holds len (f | i) <= i

proof end;

theorem Th20: :: FINSEQ_5:20

for f being FinSequence
for i being Nat holds dom (f | i) c= dom f

proof end;

theorem Th21: :: FINSEQ_5:21

for f being FinSequence
for i being Nat holds rng (f | i) c= rng f

proof end;

theorem :: FINSEQ_5:22

canceled;

theorem Th23: :: FINSEQ_5:23

for D being set
for f being FinSequence of D st not f is empty holds
f | 1 = <*(f /. 1)*>

proof end;

theorem :: FINSEQ_5:24

for i being Nat
for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f = (f | i) ^ <*(f /. (len f))*>

proof end;

Lm2: for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f | i is one-to-one

proof end;

registration

let i be Nat;
let D be non empty set ;
let f be one-to-one FinSequence of D;
cluster f | i -> one-to-one ;
coherence
f | i is one-to-one by Lm2;

end;

theorem Th25: :: FINSEQ_5:25

for i being Nat
for D being set
for f, g being FinSequence of D st i <= len f holds
(f ^ g) | i = f | i

proof end;

theorem :: FINSEQ_5:26

for D being set
for f, g being FinSequence of D holds (f ^ g) | (len f) = f

proof end;

theorem :: FINSEQ_5:27

for D being non empty set
for p being Element of D
for D being set
for f being FinSequence of D st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)

proof end;

theorem :: FINSEQ_5:28

for i being Nat
for D being non empty set
for f being FinSequence of D holds len (f /^ i) <= len f

proof end;

theorem Th29: :: FINSEQ_5:29

for i, n being Nat
for D being set
for f being FinSequence of D st i in dom (f /^ n) holds
n + i in dom f

proof end;

theorem Th30: :: FINSEQ_5:30

for i, n being Nat
for D being set
for f being FinSequence of D st i in dom (f /^ n) holds
(f /^ n) /. i = f /. (n + i)

proof end;

theorem Th31: :: FINSEQ_5:31

for D being set
for f being FinSequence of D holds f /^ 0 = f

proof end;

theorem :: FINSEQ_5:32

for D being non empty set
for f being FinSequence of D st not f is empty holds
f = <*(f /. 1)*> ^ (f /^ 1)

proof end;

theorem :: FINSEQ_5:33

for i being Nat
for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f /^ i = <*(f /. (len f))*>

proof end;

theorem Th34: :: FINSEQ_5:34

for j, i being Nat
for D being non empty set
for f being FinSequence of D st j + 1 = i & i in dom f holds
<*(f /. i)*> ^ (f /^ i) = f /^ j

proof end;

theorem Th35: :: FINSEQ_5:35

for i being Nat
for D being set
for f being FinSequence of D st len f <= i holds
f /^ i is empty

proof end;

theorem Th36: :: FINSEQ_5:36

for n being Nat
for D being non empty set
for f being FinSequence of D holds rng (f /^ n) c= rng f

proof end;

Lm3: for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f /^ i is one-to-one

proof end;

registration

let i be Nat;
let D be non empty set ;
let f be one-to-one FinSequence of D;
cluster f /^ i -> one-to-one ;
coherence
f /^ i is one-to-one by Lm3;

end;

theorem Th37: :: FINSEQ_5:37

for n being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
rng (f | n) misses rng (f /^ n)

proof end;

theorem :: FINSEQ_5:38

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
f |-- p = f /^ (p .. f)

proof end;

theorem Th39: :: FINSEQ_5:39

for i being Nat
for D being non empty set
for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i

proof end;

theorem :: FINSEQ_5:40

for D being non empty set
for f, g being FinSequence of D holds (f ^ g) /^ (len f) = g

proof end;

theorem Th41: :: FINSEQ_5:41

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
f /. (p .. f) = p

proof end;

theorem Th42: :: FINSEQ_5:42

for i being Nat
for D being non empty set
for f being FinSequence of D st i in dom f holds
(f /. i) .. f <= i

proof end;

theorem :: FINSEQ_5:43

for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng (f | i) holds
p .. (f | i) = p .. f

proof end;

theorem :: FINSEQ_5:44

for i being Nat
for D being non empty set
for f being FinSequence of D st i in dom f & f is one-to-one holds
(f /. i) .. f = i

proof end;

definition

let D be non empty set ;
let f be FinSequence of D;
let p be set ;
func f -: p -> FinSequence of D equals :: FINSEQ_5:def 1
f | (p .. f);
correctness
coherence
f | (p .. f) is FinSequence of D;
;

end;

:: deftheorem defines -: FINSEQ_5:def 1 :
for D being non empty set
for f being FinSequence of D
for p being set holds f -: p = f | (p .. f);

theorem Th45: :: FINSEQ_5:45

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
len (f -: p) = p .. f

proof end;

theorem Th46: :: FINSEQ_5:46

for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds
(f -: p) /. i = f /. i

proof end;

theorem :: FINSEQ_5:47

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(f -: p) /. 1 = f /. 1

proof end;

theorem :: FINSEQ_5:48

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(f -: p) /. (p .. f) = p

proof end;

theorem :: FINSEQ_5:49

for D being non empty set
for p being Element of D
for f being FinSequence of D
for x being set st x in rng f & p in rng f & x .. f <= p .. f holds
x in rng (f -: p)

proof end;

theorem :: FINSEQ_5:50

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
not f -: p is empty

proof end;

theorem :: FINSEQ_5:51

for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (f -: p) c= rng f by Th21;

registration

let D be non empty set ;
let p be Element of D;
let f be one-to-one FinSequence of D;
cluster f -: p -> one-to-one ;
coherence
f -: p is one-to-one ;

end;

definition

let D be non empty set ;
let f be FinSequence of D;
let p be Element of D;
func f :- p -> FinSequence of D equals :: FINSEQ_5:def 2
<*p*> ^ (f /^ (p .. f));
coherence
<*p*> ^ (f /^ (p .. f)) is FinSequence of D ;

end;

:: deftheorem defines :- FINSEQ_5:def 2 :
for D being non empty set
for f being FinSequence of D
for p being Element of D holds f :- p = <*p*> ^ (f /^ (p .. f));

theorem Th52: :: FINSEQ_5:52

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i )

proof end;

theorem Th53: :: FINSEQ_5:53

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
len (f :- p) = ((len f) - (p .. f)) + 1

proof end;

theorem Th54: :: FINSEQ_5:54

for j being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
j + (p .. f) in dom f

proof end;

registration

let D be non empty set ;
let p be Element of D;
let f be FinSequence of D;
cluster f :- p -> non empty ;
coherence
not f :- p is empty ;

end;

theorem Th55: :: FINSEQ_5:55

for j being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
(f :- p) /. (j + 1) = f /. (j + (p .. f))

proof end;

theorem :: FINSEQ_5:56

for D being non empty set
for p being Element of D
for f being FinSequence of D holds (f :- p) /. 1 = p by Th16;

theorem :: FINSEQ_5:57

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(f :- p) /. (len (f :- p)) = f /. (len f)

proof end;

theorem :: FINSEQ_5:58

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
rng (f :- p) c= rng f

proof end;

theorem :: FINSEQ_5:59

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & f is one-to-one holds
f :- p is one-to-one

proof end;

definition

let f be FinSequence;
func Rev f -> FinSequence means :Def3: :: FINSEQ_5:def 3
( len it = len f & ( for i being Nat st i in dom it holds
it . i = f . (((len f) - i) + 1) ) );
existence
ex b₁ being FinSequence st
( len b₁ = len f & ( for i being Nat st i in dom b₁ holds
b₁ . i = f . (((len f) - i) + 1) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st len b₁ = len f & ( for i being Nat st i in dom b₁ holds
b₁ . i = f . (((len f) - i) + 1) ) & len b₂ = len f & ( for i being Nat st i in dom b₂ holds
b₂ . i = f . (((len f) - i) + 1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Rev FINSEQ_5:def 3 :
for f, b₂ being FinSequence holds
( b₂ = Rev f iff ( len b₂ = len f & ( for i being Nat st i in dom b₂ holds
b₂ . i = f . (((len f) - i) + 1) ) ) );

theorem Th60: :: FINSEQ_5:60

for f being FinSequence holds
( dom f = dom (Rev f) & rng f = rng (Rev f) )

proof end;

theorem Th61: :: FINSEQ_5:61

for i being Nat
for f being FinSequence st i in dom f holds
(Rev f) . i = f . (((len f) - i) + 1)

proof end;

theorem Th62: :: FINSEQ_5:62

for f being FinSequence
for i, j being Nat st i in dom f & i + j = (len f) + 1 holds
j in dom (Rev f)

proof end;

registration

let f be empty FinSequence;
cluster Rev f -> empty ;
coherence
Rev f is empty

proof end;

end;

theorem :: FINSEQ_5:63

for x being set holds Rev <*x*> = <*x*>

proof end;

theorem :: FINSEQ_5:64

for x1, x2 being set holds Rev <*x1,x2*> = <*x2,x1*>

proof end;

theorem Th65: :: FINSEQ_5:65

for f being FinSequence holds
( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 )

proof end;

registration

let f be one-to-one FinSequence;
cluster Rev f -> one-to-one ;
coherence
Rev f is one-to-one

proof end;

end;

theorem Th66: :: FINSEQ_5:66

for f being FinSequence
for x being set holds Rev (f ^ <*x*>) = <*x*> ^ (Rev f)

proof end;

theorem :: FINSEQ_5:67

for f, g being FinSequence holds Rev (f ^ g) = (Rev g) ^ (Rev f)

proof end;

definition

let D be set ;
let f be FinSequence of D;
:: original: Rev
redefine func Rev f -> FinSequence of D;
coherence
Rev f is FinSequence of D

proof end;

end;

theorem :: FINSEQ_5:68

for D being non empty set
for f being FinSequence of D st not f is empty holds
( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 )

proof end;

theorem :: FINSEQ_5:69

for j being Nat
for D being non empty set
for f being FinSequence of D
for i being Nat st i in dom f & i + j = (len f) + 1 holds
f /. i = (Rev f) /. j

proof end;

definition

let D be non empty set ;
let f be FinSequence of D;
let p be Element of D;
let n be Nat;
func Ins (f,n,p) -> FinSequence of D equals :: FINSEQ_5:def 4
((f | n) ^ <*p*>) ^ (f /^ n);
correctness
coherence
((f | n) ^ <*p*>) ^ (f /^ n) is FinSequence of D;
;

end;

:: deftheorem defines Ins FINSEQ_5:def 4 :
for D being non empty set
for f being FinSequence of D
for p being Element of D
for n being Nat holds Ins (f,n,p) = ((f | n) ^ <*p*>) ^ (f /^ n);

theorem :: FINSEQ_5:70

for D being non empty set
for p being Element of D
for f being FinSequence of D holds Ins (f,0,p) = <*p*> ^ f

proof end;

theorem Th71: :: FINSEQ_5:71

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st len f <= n holds
Ins (f,n,p) = f ^ <*p*>

proof end;

theorem :: FINSEQ_5:72

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1

proof end;

theorem Th73: :: FINSEQ_5:73

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f)

proof end;

registration

let D be non empty set ;
let f be FinSequence of D;
let n be Nat;
let p be Element of D;
cluster Ins (f,n,p) -> non empty ;
coherence
not Ins (f,n,p) is empty ;

end;

theorem :: FINSEQ_5:74

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds p in rng (Ins (f,n,p))

proof end;

theorem Th75: :: FINSEQ_5:75

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D
for i being Nat st i in dom (f | n) holds
(Ins (f,n,p)) /. i = f /. i

proof end;

theorem :: FINSEQ_5:76

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st n <= len f holds
(Ins (f,n,p)) /. (n + 1) = p

proof end;

theorem :: FINSEQ_5:77

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D
for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) /. (i + 1) = f /. i

proof end;

theorem :: FINSEQ_5:78

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins (f,n,p)) /. 1 = f /. 1

proof end;

theorem :: FINSEQ_5:79

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st f is one-to-one & not p in rng f holds
Ins (f,n,p) is one-to-one

proof end;

begin

theorem :: FINSEQ_5:80

for D being non empty set
for f being FinSequence of D
for i1, i2 being Nat st i1 <= i2 holds
( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 )

proof end;

theorem :: FINSEQ_5:81

for D being non empty set
for i being Nat holds (<*> D) | i = <*> D ;

theorem :: FINSEQ_5:82

for D being non empty set holds Rev (<*> D) = <*> D ;

registration

cluster non trivial Relation-like Function-like V31() FinSequence-like FinSubsequence-like set ;
existence
not for b₁ being FinSequence holds b₁ is trivial

proof end;

end;

theorem :: FINSEQ_5:83

for D being non empty set
for f being FinSequence of D
for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1

proof end;

theorem :: FINSEQ_5:84

for D being set
for f being FinSequence of D st len f >= 2 holds
f | 2 = <*(f /. 1),(f /. 2)*>

proof end;

theorem Th85: :: FINSEQ_5:85

for k being Nat
for D being set
for f being FinSequence of D st k + 1 <= len f holds
f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*>

proof end;

theorem Th86: :: FINSEQ_5:86

for D being set
for p being FinSequence of D
for i being Nat st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>

proof end;

theorem :: FINSEQ_5:87

for D being non empty set
for p being FinSequence of D
for n being Nat st 1 <= n & n <= len p holds
p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n)

proof end;