:: Some Properties of Restrictions of Finite Sequences
:: by Czes\law Byli\'nski
::
:: Received January 25, 1995
:: Copyright (c) 1995-2012 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 ;
let y be set ;
cluster <*x,y*> -> non trivial ;
coherence
not <*x,y*> is trivial
proof end;
end;

registration
cluster non empty Relation-like NAT -defined Function-like one-to-one V34() FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st
( b1 is one-to-one & not b1 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
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 non empty Relation-like NAT -defined D -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like for FinSequence of D;
existence
ex b1 being FinSequence of D st
( b1 is one-to-one & not b1 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 Th13: :: 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 D being non empty set
for f being FinSequence of D st len f = 1 holds
f = <*(f /. 1)*>
proof end;

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
proof end;

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 D being set
for f being FinSequence of D 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 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:23
for D being set
for f, g being FinSequence of D 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 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:25
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 Th26: :: FINSEQ_5:26
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 Th27: :: FINSEQ_5:27
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 Th28: :: FINSEQ_5:28
for D being set
for f being FinSequence of D holds f /^ 0 = f
proof end;

theorem :: 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 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 Th31: :: FINSEQ_5:31
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 Th32: :: FINSEQ_5:32
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 Th33: :: FINSEQ_5:33
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 Th34: :: FINSEQ_5:34
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: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 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:37
for D being non empty set
for f, g being FinSequence of D holds (f ^ g) /^ (len f) = g
proof 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 b1 being FinSequence st
( len b1 = len f & ( for i being Nat st i in dom b1 holds
b1 . i = f . (((len f) - i) + 1) ) )
proof end;
uniqueness
for b1, b2 being FinSequence st len b1 = len f & ( for i being Nat st i in dom b1 holds
b1 . i = f . (((len f) - i) + 1) ) & len b2 = len f & ( for i being Nat st i in dom b2 holds
b2 . i = f . (((len f) - i) + 1) ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being FinSequence st len b1 = len b2 & ( for i being Nat st i in dom b1 holds
b1 . i = b2 . (((len b2) - i) + 1) ) holds
( len b2 = len b1 & ( for i being Nat st i in dom b2 holds
b2 . i = b1 . (((len b1) - i) + 1) ) )
proof end;
end;

:: deftheorem Def3 defines Rev FINSEQ_5:def 3 :
for f, b2 being FinSequence holds
( b2 = Rev f iff ( len b2 = len f & ( for i being Nat st i in dom b2 holds
b2 . 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 set holds Rev <*x*> = <*x*>
proof end;

theorem :: FINSEQ_5:61
for x1, x2 being set 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 set 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);
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: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
proof end;

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;

begin

:: 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 non trivial Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like for set ;
existence
not for b1 being FinSequence holds b1 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 Th82: :: 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 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;

:: from POLYNOM4, 2007.03.18, A.T.
theorem :: FINSEQ_5:84
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;