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

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 object 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 object st f is one-to-one & y1 in rng f & f " {y1} = f " {y2} holds
y1 = y2

proof end;

registration

let x be object ;

cluster <*x*> -> trivial ;

coherence
<*x*> is trivial ;
let y be object ;

cluster <*x,y*> -> non trivial ;

coherence
not <*x,y*> is trivial

proof end;

end;

registration

cluster Relation-like NAT -defined non empty Function-like one-to-one V41() FinSequence-like FinSubsequence-like for 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 object
for f being FinSequence holds len (<*x*> ^ f) = 1 + (len f)

proof end;

theorem :: FINSEQ_5:9

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 Th10: :: FINSEQ_5:10

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 Th11: :: FINSEQ_5:11

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 Relation-like NAT -defined D -valued non empty Function-like one-to-one V41() FinSequence-like FinSubsequence-like for FinSequence of D;

existence
ex b₁ being FinSequence of D st
( b₁ is one-to-one & not b₁ is empty )

proof end;

end;

:: FINSEQ_1:17

theorem :: FINSEQ_5:12

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;

:: FINSEQ_1:18

theorem :: FINSEQ_5:13

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 Th14: :: FINSEQ_5:14

for f being FinSequence st len f = 1 holds
f = <*(f . 1)*> by FINSEQ_1:40;

theorem Th15: :: FINSEQ_5:15

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
by FINSEQ_1:def 7;

theorem Th16: :: FINSEQ_5:16

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

proof end;

theorem Th17: :: FINSEQ_5:17

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

proof end;

theorem Th18: :: FINSEQ_5:18

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

proof end;

theorem Th19: :: FINSEQ_5:19

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

proof end;

theorem Th20: :: FINSEQ_5:20

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

proof end;

theorem :: FINSEQ_5:21

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 Th22: :: FINSEQ_5:22

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

proof end;

theorem :: FINSEQ_5:23

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

proof end;

theorem :: FINSEQ_5:24

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 .. f)

proof end;

theorem :: FINSEQ_5:25

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

proof end;

theorem Th26: :: FINSEQ_5:26

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

proof end;

theorem Th27: :: FINSEQ_5:27

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

proof end;

theorem Th28: :: FINSEQ_5:28

for f being FinSequence holds f /^ 0 = f

proof end;

registration

let f be FinSequence;

reduce f /^ 0 to f;

reducibility
f /^ 0 = f by Th28;

end;

theorem Th29: :: FINSEQ_5:29

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:30

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

proof end;

theorem Th31: :: FINSEQ_5:31

for i, j 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 Th32: :: FINSEQ_5:32

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

proof end;

theorem Th33: :: FINSEQ_5:33

for n being Nat
for f being FinSequence 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 Th34: :: FINSEQ_5:34

for n being Nat
for f being FinSequence st f is one-to-one holds
rng (f | n) misses rng (f /^ n)

proof end;

theorem :: FINSEQ_5:35

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 Th36: :: FINSEQ_5:36

for i being Nat
for f, g being FinSequence holds (f ^ g) /^ ((len f) + i) = g /^ i

proof end;

theorem Th37: :: FINSEQ_5:37

for f, g being FinSequence holds (f ^ g) /^ (len f) = g

proof end;

registration

let f, g be FinSequence;

reduce (f ^ g) /^ (len f) to g;

reducibility
(f ^ g) /^ (len f) = g by Th37;

end;

theorem Th38: :: 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

proof end;

theorem Th39: :: FINSEQ_5:39

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:40

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:41

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 Th42: :: FINSEQ_5:42

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 Th43: :: 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 in Seg (p .. f) holds
(f -: p) /. i = f /. i

proof end;

theorem :: FINSEQ_5:44

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: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
(f -: p) /. (p .. f) = p

proof end;

theorem :: FINSEQ_5:46

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: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
not f -: p is empty

proof end;

theorem :: FINSEQ_5:48

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

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 Th49: :: FINSEQ_5:49

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 Th50: :: 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
len (f :- p) = ((len f) - (p .. f)) + 1

proof end;

theorem Th51: :: FINSEQ_5:51

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 Th52: :: FINSEQ_5:52

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:53

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

theorem :: FINSEQ_5:54

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:55

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:56

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;

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

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 Th57: :: FINSEQ_5:57

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

proof end;

theorem Th58: :: FINSEQ_5:58

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 Th59: :: FINSEQ_5:59

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:60

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

proof end;

theorem :: FINSEQ_5:61

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

proof end;

theorem Th62: :: FINSEQ_5:62

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 Th63: :: FINSEQ_5:63

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

proof end;

theorem :: FINSEQ_5:64

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:65

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:66

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

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:67

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 by FINSEQ_1:34;

theorem Th68: :: FINSEQ_5:68

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:69

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 Th70: :: FINSEQ_5:70

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:71

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 Th72: :: 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
for i being Nat st i in dom (f | n) holds
(Ins (f,n,p)) . i = f . i

proof end;

theorem :: 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 st n <= len f holds
(Ins (f,n,p)) . (n + 1) = p

proof 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
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:75

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:76

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;

:: from JORDAN4, 2005.11.16, A.T.

theorem :: FINSEQ_5:77

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:78

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

theorem :: FINSEQ_5:79

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

:: from AMISTD_1, 2006.03,15, A.T.

registration

cluster Relation-like NAT -defined non trivial Function-like V41() FinSequence-like FinSubsequence-like for set ;

existence
not for b₁ being FinSequence holds b₁ is trivial

proof end;

end;

:: from JORDAN3, 2007.03.09, A.T

theorem :: FINSEQ_5:80

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:81

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

proof end;

theorem :: FINSEQ_5:82

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;

:: from JORDAN3, 2007.03.18, A.T.

theorem Th83: :: FINSEQ_5:83

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

proof end;

:: from POLYNOM4, 2007.03.18, A.T.

theorem :: FINSEQ_5:84

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

proof end;

:: from POLYALG1, 2016.10.19, A.K.

theorem Th3: :: FINSEQ_5:85

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

proof end;

theorem :: FINSEQ_5:86

for D being non empty set
for f being non empty FinSequence of D holds f = <*(f . 1)*> ^ (Del (f,1))

proof end;