:: On the Decomposition of Finite Sequences
:: by Andrzej Trybulec
::
:: Received May 24, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users

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

registration
let f be non empty FinSequence;
cluster Rev f -> non empty ;
coherence
not Rev f is empty
proof end;
end;

Lm1: for x, y being set holds rng <*x,y*> = {x,y}
proof end;

Lm2: for x, y, z being set holds rng <*x,y,z*> = {x,y,z}
proof end;

theorem Th1: :: FINSEQ_6:1
for X being set
for i being Nat st X c= Seg i & 1 in X holds
(Sgm X) . 1 = 1
proof end;

theorem Th2: :: FINSEQ_6:2
for k being Nat
for f being FinSequence st k in dom f & ( for i being Nat st 1 <= i & i < k holds
f . i <> f . k ) holds
(f . k) .. f = k
proof end;

theorem Th3: :: FINSEQ_6:3
for p1, p2 being set holds <*p1,p2*> | (Seg 1) = <*p1*>
proof end;

theorem Th4: :: FINSEQ_6:4
for p1, p2, p3 being set holds <*p1,p2,p3*> | (Seg 1) = <*p1*>
proof end;

theorem Th5: :: FINSEQ_6:5
for p1, p2, p3 being set holds <*p1,p2,p3*> | (Seg 2) = <*p1,p2*>
proof end;

theorem Th6: :: FINSEQ_6:6
for f1, f2 being FinSequence
for p being set st p in rng f1 holds
p .. (f1 ^ f2) = p .. f1
proof end;

theorem Th7: :: FINSEQ_6:7
for f1, f2 being FinSequence
for p being set st p in (rng f2) \ (rng f1) holds
p .. (f1 ^ f2) = (len f1) + (p .. f2)
proof end;

theorem Th8: :: FINSEQ_6:8
for f1, f2 being FinSequence
for p being set st p in rng f1 holds
(f1 ^ f2) |-- p = (f1 |-- p) ^ f2
proof end;

theorem Th9: :: FINSEQ_6:9
for f1, f2 being FinSequence
for p being set st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) |-- p = f2 |-- p
proof end;

theorem Th10: :: FINSEQ_6:10
for f1, f2 being FinSequence holds f1 c= f1 ^ f2
proof end;

theorem :: FINSEQ_6:11
for f1, f2 being FinSequence
for A being set st A c= dom f1 holds
(f1 ^ f2) | A = f1 | A by ;

theorem Th12: :: FINSEQ_6:12
for f1, f2 being FinSequence
for p being set st p in rng f1 holds
(f1 ^ f2) -| p = f1 -| p
proof end;

registration
let f1 be FinSequence;
let i be Nat;
cluster f1 | (Seg i) -> FinSequence-like ;
coherence
f1 | (Seg i) is FinSequence-like
by FINSEQ_1:15;
end;

theorem Th13: :: FINSEQ_6:13
for f1, f2, f3 being FinSequence st f1 c= f2 holds
f3 ^ f1 c= f3 ^ f2
proof end;

theorem Th14: :: FINSEQ_6:14
for f1, f2 being FinSequence
for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))
proof end;

theorem Th15: :: FINSEQ_6:15
for f1, f2 being FinSequence
for p being set st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) -| p = f1 ^ (f2 -| p)
proof end;

theorem Th16: :: FINSEQ_6:16
for f1, f2 being FinSequence
for p being set st f1 ^ f2 just_once_values p holds
p in (rng f1) \+\ (rng f2)
proof end;

theorem :: FINSEQ_6:17
for f1, f2 being FinSequence
for p being set st f1 ^ f2 just_once_values p & p in rng f1 holds
f1 just_once_values p
proof end;

theorem Th18: :: FINSEQ_6:18
for p being set holds p .. <*p*> = 1
proof end;

theorem Th19: :: FINSEQ_6:19
for p1, p2 being set holds p1 .. <*p1,p2*> = 1
proof end;

theorem Th20: :: FINSEQ_6:20
for p1, p2 being set st p1 <> p2 holds
p2 .. <*p1,p2*> = 2
proof end;

theorem Th21: :: FINSEQ_6:21
for p1, p2, p3 being set holds p1 .. <*p1,p2,p3*> = 1
proof end;

theorem Th22: :: FINSEQ_6:22
for p1, p2, p3 being set st p1 <> p2 holds
p2 .. <*p1,p2,p3*> = 2
proof end;

theorem Th23: :: FINSEQ_6:23
for p1, p2, p3 being set st p1 <> p3 & p2 <> p3 holds
p3 .. <*p1,p2,p3*> = 3
proof end;

theorem Th24: :: FINSEQ_6:24
for p being set
for f being FinSequence holds Rev (<*p*> ^ f) = (Rev f) ^ <*p*>
proof end;

theorem :: FINSEQ_6:25
for f being FinSequence holds Rev (Rev f) = f ;

theorem Th26: :: FINSEQ_6:26
for x, y being set st x <> y holds
<*x,y*> -| y = <*x*>
proof end;

theorem Th27: :: FINSEQ_6:27
for x, y, z being set st x <> y holds
<*x,y,z*> -| y = <*x*>
proof end;

theorem Th28: :: FINSEQ_6:28
for x, y, z being set st x <> z & y <> z holds
<*x,y,z*> -| z = <*x,y*>
proof end;

theorem :: FINSEQ_6:29
for x, y being set holds <*x,y*> |-- x = <*y*>
proof end;

theorem Th30: :: FINSEQ_6:30
for x, y, z being set st x <> y holds
<*x,y,z*> |-- y = <*z*>
proof end;

theorem :: FINSEQ_6:31
for x, y, z being set holds <*x,y,z*> |-- x = <*y,z*>
proof end;

theorem Th32: :: FINSEQ_6:32
for z being set holds
( <*z*> |-- z = {} & <*z*> -| z = {} )
proof end;

theorem Th33: :: FINSEQ_6:33
for x, y being set st x <> y holds
<*x,y*> |-- y = {}
proof end;

theorem Th34: :: FINSEQ_6:34
for x, y, z being set st x <> z & y <> z holds
<*x,y,z*> |-- z = {}
proof end;

theorem Th35: :: FINSEQ_6:35
for x, y being set
for f being FinSequence st x in rng f & y in rng (f -| x) holds
(f -| x) -| y = f -| y
proof end;

theorem Th36: :: FINSEQ_6:36
for x being set
for f1, f2 being FinSequence st not x in rng f1 holds
x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1
proof end;

theorem Th37: :: FINSEQ_6:37
for x being set
for f being FinSequence st f just_once_values x holds
(x .. f) + (x .. (Rev f)) = (len f) + 1
proof end;

theorem Th38: :: FINSEQ_6:38
for x being set
for f being FinSequence st f just_once_values x holds
Rev (f -| x) = (Rev f) |-- x
proof end;

theorem :: FINSEQ_6:39
for x being set
for f being FinSequence st f just_once_values x holds
Rev f just_once_values x
proof end;

theorem Th40: :: FINSEQ_6:40
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) ^ <*p*>
proof end;

theorem Th41: :: FINSEQ_6: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 = <*p*> ^ (f |-- p)
proof end;

theorem Th42: :: FINSEQ_6:42
for D being non empty set
for f being FinSequence of D st f <> {} holds
f /. 1 in rng f
proof end;

theorem Th43: :: FINSEQ_6:43
for D being non empty set
for f being FinSequence of D st f <> {} holds
(f /. 1) .. f = 1
proof end;

theorem Th44: :: FINSEQ_6:44
for D being non empty set
for p being Element of D
for f being FinSequence of D st f <> {} & f /. 1 = p holds
( f -: p = <*p*> & f :- p = f )
proof end;

theorem Th45: :: FINSEQ_6:45
for D being non empty set
for p1 being Element of D
for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f
proof end;

theorem Th46: :: FINSEQ_6:46
for D being non empty set
for p1, p2 being Element of D holds <*p1,p2*> /^ 1 = <*p2*> by Th45;

theorem Th47: :: FINSEQ_6:47
for D being non empty set
for p1, p2, p3 being Element of D holds <*p1,p2,p3*> /^ 1 = <*p2,p3*>
proof end;

theorem Th48: :: FINSEQ_6:48
for k being Nat
for D being non empty set
for f being FinSequence of D st k in dom f & ( for i being Nat st 1 <= i & i < k holds
f /. i <> f /. k ) holds
(f /. k) .. f = k
proof end;

theorem Th49: :: FINSEQ_6:49
for D being non empty set
for p1, p2 being Element of D st p1 <> p2 holds
<*p1,p2*> -: p2 = <*p1,p2*>
proof end;

theorem Th50: :: FINSEQ_6:50
for D being non empty set
for p1, p2, p3 being Element of D st p1 <> p2 holds
<*p1,p2,p3*> -: p2 = <*p1,p2*>
proof end;

theorem Th51: :: FINSEQ_6:51
for D being non empty set
for p1, p2, p3 being Element of D st p1 <> p3 & p2 <> p3 holds
<*p1,p2,p3*> -: p3 = <*p1,p2,p3*>
proof end;

theorem :: FINSEQ_6:52
for D being non empty set
for p being Element of D holds
( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> )
proof end;

theorem Th53: :: FINSEQ_6:53
for D being non empty set
for p1, p2 being Element of D st p1 <> p2 holds
<*p1,p2*> :- p2 = <*p2*>
proof end;

theorem Th54: :: FINSEQ_6:54
for D being non empty set
for p1, p2, p3 being Element of D st p1 <> p2 holds
<*p1,p2,p3*> :- p2 = <*p2,p3*>
proof end;

theorem Th55: :: FINSEQ_6:55
for D being non empty set
for p1, p2, p3 being Element of D st p1 <> p3 & p2 <> p3 holds
<*p1,p2,p3*> :- p3 = <*p3*>
proof end;

theorem Th56: :: FINSEQ_6:56
for k 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 & p .. f > k holds
p .. f = k + (p .. (f /^ k))
proof end;

theorem Th57: :: FINSEQ_6:57
for k 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 & p .. f > k holds
p in rng (f /^ k)
proof end;

theorem Th58: :: FINSEQ_6:58
for i, k being Nat
for D being non empty set
for f being FinSequence of D st k < i & i in dom f holds
f /. i in rng (f /^ k)
proof end;

theorem Th59: :: FINSEQ_6:59
for k 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 & p .. f > k holds
(f /^ k) -: p = (f -: p) /^ k
proof end;

theorem Th60: :: FINSEQ_6:60
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f <> 1 holds
(f /^ 1) -: p = (f -: p) /^ 1
proof end;

theorem Th61: :: FINSEQ_6:61
for D being non empty set
for p being Element of D
for f being FinSequence of D holds p in rng (f :- p)
proof end;

theorem Th62: :: FINSEQ_6:62
for x being set
for D being non empty set
for p being Element of D
for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds
x in rng (f :- p)
proof end;

theorem Th63: :: FINSEQ_6:63
for k 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 & k <= len f & k >= p .. f holds
f /. k in rng (f :- p)
proof end;

theorem Th64: :: FINSEQ_6:64
for D being non empty set
for p being Element of D
for f1, f2 being FinSequence of D st p in rng f1 holds
(f1 ^ f2) :- p = (f1 :- p) ^ f2
proof end;

theorem Th65: :: FINSEQ_6:65
for D being non empty set
for p being Element of D
for f1, f2 being FinSequence of D st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) :- p = f2 :- p
proof end;

theorem Th66: :: FINSEQ_6:66
for D being non empty set
for p being Element of D
for f1, f2 being FinSequence of D st p in rng f1 holds
(f1 ^ f2) -: p = f1 -: p
proof end;

theorem Th67: :: FINSEQ_6:67
for D being non empty set
for p being Element of D
for f1, f2 being FinSequence of D st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) -: p = f1 ^ (f2 -: p)
proof end;

theorem :: FINSEQ_6:68
for D being non empty set
for p being Element of D
for f being FinSequence of D holds (f :- p) :- p = f :- p
proof end;

theorem Th69: :: FINSEQ_6:69
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds
f |-- p2 = (f |-- p1) |-- p2
proof end;

theorem Th70: :: FINSEQ_6:70
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 = (rng (f -: p)) \/ (rng (f :- p))
proof end;

theorem Th71: :: FINSEQ_6:71
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds
(f :- p1) :- p2 = f :- p2
proof end;

theorem Th72: :: FINSEQ_6:72
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
p .. (f -: p) = p .. f
proof end;

theorem :: FINSEQ_6:73
for i being Nat
for D being non empty set
for f being FinSequence of D holds (f | i) | i = f | i ;

theorem Th74: :: FINSEQ_6:74
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 Th75: :: FINSEQ_6:75
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p1 in rng f & p2 in rng (f -: p1) holds
(f -: p1) -: p2 = f -: p2
proof end;

theorem Th76: :: FINSEQ_6:76
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) /^ 1) = f
proof end;

theorem Th77: :: FINSEQ_6:77
for D being non empty set
for f1, f2 being FinSequence of D st f1 <> {} holds
(f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2
proof end;

theorem Th78: :: FINSEQ_6:78
for D being non empty set
for p2 being Element of D
for f being FinSequence of D st p2 in rng f & p2 .. f <> 1 holds
p2 in rng (f /^ 1)
proof end;

theorem Th79: :: FINSEQ_6:79
for D being non empty set
for p being Element of D
for f being FinSequence of D holds p .. (f :- p) = 1
proof end;

Lm3: 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 & p .. f > i holds
i + (p .. (f /^ i)) = p .. f

proof end;

theorem Th80: :: FINSEQ_6:80
for k being Nat
for D being non empty set holds (<*> D) /^ k = <*> D
proof end;

theorem Th81: :: FINSEQ_6:81
for i, k being Nat
for D being non empty set
for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k
proof end;

theorem Th82: :: FINSEQ_6:82
for k 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 & p .. f > k holds
(f /^ k) :- p = f :- p
proof end;

theorem Th83: :: FINSEQ_6:83
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f <> 1 holds
(f /^ 1) :- p = f :- p
proof end;

theorem Th84: :: FINSEQ_6:84
for i, k being Nat
for D being non empty set
for f being FinSequence of D st i + k = len f holds
Rev (f /^ k) = (Rev f) | i
proof end;

theorem Th85: :: FINSEQ_6:85
for i, k being Nat
for D being non empty set
for f being FinSequence of D st i + k = len f holds
Rev (f | k) = (Rev f) /^ i
proof end;

theorem Th86: :: FINSEQ_6:86
for D being non empty set
for p being Element of D
for f being FinSequence of D st f just_once_values p holds
Rev (f |-- p) = (Rev f) -| p
proof end;

theorem Th87: :: FINSEQ_6:87
for D being non empty set
for p being Element of D
for f being FinSequence of D st f just_once_values p holds
Rev (f :- p) = (Rev f) -: p
proof end;

theorem Th88: :: FINSEQ_6:88
for D being non empty set
for p being Element of D
for f being FinSequence of D st f just_once_values p holds
Rev (f -: p) = (Rev f) :- p
proof end;

definition
let D be non empty set ;
let IT be FinSequence of D;
attr IT is circular means :Def1A: :: FINSEQ_6:def 1
IT /. 1 = IT /. (len IT);
end;

:: deftheorem Def1A defines circular FINSEQ_6:def 1 :
for D being non empty set
for IT being FinSequence of D holds
( IT is circular iff IT /. 1 = IT /. (len IT) );

definition
let D be non empty set ;
let f be FinSequence of D;
let p be Element of D;
func Rotate (f,p) -> FinSequence of D equals :Def2: :: FINSEQ_6:def 2
(f :- p) ^ ((f -: p) /^ 1) if p in rng f
otherwise f;
correctness
coherence
( ( p in rng f implies (f :- p) ^ ((f -: p) /^ 1) is FinSequence of D ) & ( not p in rng f implies f is FinSequence of D ) )
;
consistency
for b1 being FinSequence of D holds verum
;
;
end;

:: deftheorem Def2 defines Rotate FINSEQ_6:def 2 :
for D being non empty set
for f being FinSequence of D
for p being Element of D holds
( ( p in rng f implies Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) ) & ( not p in rng f implies Rotate (f,p) = f ) );

registration
let D be non empty set ;
let f be non empty FinSequence of D;
let p be Element of D;
cluster Rotate (f,p) -> non empty ;
coherence
not Rotate (f,p) is empty
proof end;
end;

registration
let D be non empty set ;
existence
ex b1 being FinSequence of D st
( b1 is circular & b1 is 1 -element )
proof end;
existence
ex b1 being FinSequence of D st
( b1 is circular & not b1 is trivial )
proof end;
end;

theorem Th89: :: FINSEQ_6:89
for D being non empty set
for f being FinSequence of D holds Rotate (f,(f /. 1)) = f
proof end;

registration
let D be non empty set ;
let p be Element of D;
let f be non empty circular FinSequence of D;
cluster Rotate (f,p) -> circular ;
coherence
Rotate (f,p) is circular
proof end;
end;

theorem Th90: :: FINSEQ_6:90
for D being non empty set
for p being Element of D
for f being FinSequence of D st f is circular & p in rng f holds
rng (Rotate (f,p)) = rng f
proof end;

theorem Th91: :: FINSEQ_6:91
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
p in rng (Rotate (f,p))
proof end;

theorem Th92: :: FINSEQ_6:92
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(Rotate (f,p)) /. 1 = p
proof end;

theorem Th93: :: FINSEQ_6:93
for D being non empty set
for p being Element of D
for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p)
proof end;

theorem :: FINSEQ_6:94
for D being non empty set
for p being Element of D holds Rotate (<*p*>,p) = <*p*>
proof end;

theorem Th95: :: FINSEQ_6:95
for D being non empty set
for p1, p2 being Element of D holds Rotate (<*p1,p2*>,p1) = <*p1,p2*>
proof end;

theorem :: FINSEQ_6:96
for D being non empty set
for p1, p2 being Element of D holds Rotate (<*p1,p2*>,p2) = <*p2,p2*>
proof end;

theorem Th97: :: FINSEQ_6:97
for D being non empty set
for p1, p2, p3 being Element of D holds Rotate (<*p1,p2,p3*>,p1) = <*p1,p2,p3*>
proof end;

theorem :: FINSEQ_6:98
for D being non empty set
for p1, p2, p3 being Element of D st p1 <> p2 holds
Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*>
proof end;

theorem :: FINSEQ_6:99
for D being non empty set
for p1, p2, p3 being Element of D st p2 <> p3 holds
Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>
proof end;

theorem :: FINSEQ_6:100
for D being non empty set
for f being non trivial circular FinSequence of D holds rng (f /^ 1) = rng f
proof end;

theorem Th101: :: FINSEQ_6:101
for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p))
proof end;

theorem Th102: :: FINSEQ_6:102
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
proof end;

theorem Th103: :: FINSEQ_6:103
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
proof end;

theorem Th104: :: FINSEQ_6:104
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p2 in rng (f /^ 1) & f just_once_values p2 holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
proof end;

theorem :: FINSEQ_6:105
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st f is circular & f just_once_values p2 holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
proof end;

theorem :: FINSEQ_6:106
for D being non empty set
for p being Element of D
for f being FinSequence of D st f is circular & f just_once_values p holds
Rev (Rotate (f,p)) = Rotate ((Rev f),p)
proof end;

:: from AMISTD_1, 2007.07.26, A.T.
theorem :: FINSEQ_6:107
for D being non empty set
for f being trivial FinSequence of D holds
( f is empty or ex x being Element of D st f = <*x*> )
proof end;

theorem :: FINSEQ_6:108
for i being Nat
for p, q being FinSequence st len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) holds
(p ^ q) . i = q . (i - (len p))
proof end;

theorem :: FINSEQ_6:109
for D being non empty set
for x being set
for f being FinSequence of D st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) )
proof end;

theorem Th110: :: FINSEQ_6:110
for f being FinSequence st len f = 1 holds
Rev f = f
proof end;

theorem :: FINSEQ_6:111
for D being non empty set
for f being FinSequence of D
for k being Nat holds len (f /^ k) = (len f) -' k by RFINSEQ:29;

definition
let f be FinSequence;
let k1, k2 be Nat;
func mid (f,k1,k2) -> FinSequence equals :Def3: :: FINSEQ_6:def 3
(f /^ (k1 -' 1)) | ((k2 -' k1) + 1) if k1 <= k2
otherwise Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1));
correctness
coherence
( ( k1 <= k2 implies (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is FinSequence ) & ( not k1 <= k2 implies Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is FinSequence ) )
;
consistency
for b1 being FinSequence holds verum
;
;
end;

:: deftheorem Def3 defines mid FINSEQ_6:def 3 :
for f being FinSequence
for k1, k2 being Nat holds
( ( k1 <= k2 implies mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) ) & ( not k1 <= k2 implies mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) ) );

definition
let D be non empty set ;
let f be FinSequence of D;
let k1, k2 be Nat;
:: original: mid
redefine func mid (f,k1,k2) -> FinSequence of D;
coherence
mid (f,k1,k2) is FinSequence of D
proof end;
end;

theorem :: FINSEQ_6:112
canceled;

::\$CT
theorem :: FINSEQ_6:113
for D being non empty set
for f being FinSequence of D
for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds
Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1))
proof end;

theorem Th113: :: FINSEQ_6:114
for n, m being Nat
for f being FinSequence st 1 <= m & m + n <= len f holds
(f /^ n) . m = f . (m + n)
proof end;

theorem Th114: :: FINSEQ_6:115
for i being Nat
for f being FinSequence st 1 <= i & i <= len f holds
(Rev f) . i = f . (((len f) - i) + 1)
proof end;

theorem :: FINSEQ_6:116
for f being FinSequence
for k being Nat st 1 <= k holds
mid (f,1,k) = f | k
proof end;

theorem :: FINSEQ_6:117
for f being FinSequence
for k being Nat st k <= len f holds
mid (f,k,(len f)) = f /^ (k -' 1)
proof end;

theorem Th117: :: FINSEQ_6:118
for f being FinSequence
for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds
( (mid (f,k1,k2)) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds
(mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds
(mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) )
proof end;

theorem :: FINSEQ_6:119
for f being FinSequence
for k1, k2 being Nat holds rng (mid (f,k1,k2)) c= rng f
proof end;

theorem :: FINSEQ_6:120
for f being FinSequence st 1 <= len f holds
mid (f,1,(len f)) = f
proof end;

theorem :: FINSEQ_6:121
for D being non empty set
for f being FinSequence of D st 1 <= len f holds
mid (f,(len f),1) = Rev f
proof end;

theorem Th121: :: FINSEQ_6:122
for f being FinSequence
for k1, k2, i being Nat st 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) holds
( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) )
proof end;

theorem :: FINSEQ_6:123
for f being FinSequence
for k, i being Nat st 1 <= i & i <= k & k <= len f holds
(mid (f,1,k)) . i = f . i
proof end;

theorem :: FINSEQ_6:124
for f being FinSequence
for k1, k2 being Nat holds len (mid (f,k1,k2)) <= len f
proof end;

theorem Th124: :: FINSEQ_6:125
for f being FinSequence
for k being Nat
for p being set holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)
proof end;

Th126: for D being non empty set
for f being FinSequence of D
for k1, k2 being Nat st k1 < k2 & k1 in dom f holds
mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2))

proof end;

theorem :: FINSEQ_6:126
for p being FinSequence
for k1, k2 being Nat st k1 < k2 & k1 in dom p holds
mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2))
proof end;

theorem Th1: :: FINSEQ_6:127
for m, k, n being Nat holds
( ( m + 1 <= k & k <= n ) iff ex i being Nat st
( m <= i & i < n & k = i + 1 ) )
proof end;

theorem :: FINSEQ_6:128
for p, q being FinSequence
for n being Nat st q = p | (Seg n) holds
( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds
p . i = q . i ) )
proof end;

theorem Th3: :: FINSEQ_6:129
for X, Y being set
for k being Nat st X c= Seg k & Y c= dom (Sgm X) holds
(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))
proof end;

Lm1: for m, n being Nat
for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + n ) } holds
card F = n + 1

proof end;

theorem Th4: :: FINSEQ_6:130
for m, n being Nat holds card { k where k is Nat : ( m <= k & k <= m + n ) } = n + 1
proof end;

theorem :: FINSEQ_6:131
for m, n, l being Nat st 1 <= l & l <= n holds
(Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l
proof end;

definition
let p be FinSequence;
let m, n be Nat;
func (m,n) -cut p -> FinSequence means :Def1: :: FINSEQ_6:def 4
( (len it) + m = n + 1 & ( for i being Nat st i < len it holds
it . (i + 1) = p . (m + i) ) ) if ( 1 <= m & m <= n & n <= len p )
otherwise it = {} ;
consistency
for b1 being FinSequence holds verum
;
existence
( ( 1 <= m & m <= n & n <= len p implies ex b1 being FinSequence st
( (len b1) + m = n + 1 & ( for i being Nat st i < len b1 holds
b1 . (i + 1) = p . (m + i) ) ) ) & ( ( not 1 <= m or not m <= n or not n <= len p ) implies ex b1 being FinSequence st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being FinSequence holds
( ( 1 <= m & m <= n & n <= len p & (len b1) + m = n + 1 & ( for i being Nat st i < len b1 holds
b1 . (i + 1) = p . (m + i) ) & (len b2) + m = n + 1 & ( for i being Nat st i < len b2 holds
b2 . (i + 1) = p . (m + i) ) implies b1 = b2 ) & ( ( not 1 <= m or not m <= n or not n <= len p ) & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
end;

:: deftheorem Def1 defines -cut FINSEQ_6:def 4 :
for p being FinSequence
for m, n being Nat
for b4 being FinSequence holds
( ( 1 <= m & m <= n & n <= len p implies ( b4 = (m,n) -cut p iff ( (len b4) + m = n + 1 & ( for i being Nat st i < len b4 holds
b4 . (i + 1) = p . (m + i) ) ) ) ) & ( ( not 1 <= m or not m <= n or not n <= len p ) implies ( b4 = (m,n) -cut p iff b4 = {} ) ) );

Lm2: for p being FinSequence
for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds
( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )

proof end;

theorem :: FINSEQ_6:132
for p being FinSequence
for m being Nat st 1 <= m & m <= len p holds
(m,m) -cut p = <*(p . m)*>
proof end;

theorem Th7: :: FINSEQ_6:133
for p being FinSequence holds (1,(len p)) -cut p = p
proof end;

theorem Th8: :: FINSEQ_6:134
for p being FinSequence
for m, n, r being Nat st m <= n & n <= r & r <= len p holds
(((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p
proof end;

theorem :: FINSEQ_6:135
for p being FinSequence
for m being Nat st m <= len p holds
((1,m) -cut p) ^ (((m + 1),(len p)) -cut p) = p
proof end;

theorem :: FINSEQ_6:136
for p being FinSequence
for m, n being Nat st m <= n & n <= len p holds
(((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = p
proof end;

theorem Th11: :: FINSEQ_6:137
for p being FinSequence
for m, n being Nat holds rng ((m,n) -cut p) c= rng p
proof end;

definition
let D be set ;
let p be FinSequence of D;
let m, n be Nat;
:: original: -cut
redefine func (m,n) -cut p -> FinSequence of D;
coherence
(m,n) -cut p is FinSequence of D
proof end;
end;

theorem :: FINSEQ_6:138
for p being FinSequence
for m, n being Nat st 1 <= m & m <= n & n <= len p holds
( ((m,n) -cut p) . 1 = p . m & ((m,n) -cut p) . (len ((m,n) -cut p)) = p . n )
proof end;

definition
let p, q be FinSequence;
func p ^' q -> FinSequence equals :: FINSEQ_6:def 5
p ^ ((2,(len q)) -cut q);
correctness
coherence
p ^ ((2,(len q)) -cut q) is FinSequence
;
;
end;

:: deftheorem defines ^' FINSEQ_6:def 5 :
for p, q being FinSequence holds p ^' q = p ^ ((2,(len q)) -cut q);

theorem Th13: :: FINSEQ_6:139
for p, q being FinSequence st q <> {} holds
(len (p ^' q)) + 1 = (len p) + (len q)
proof end;

theorem Th14: :: FINSEQ_6:140
for p, q being FinSequence
for k being Nat st 1 <= k & k <= len p holds
(p ^' q) . k = p . k
proof end;

theorem Th15: :: FINSEQ_6:141
for p, q being FinSequence
for k being Nat st 1 <= k & k < len q holds
(p ^' q) . ((len p) + k) = q . (k + 1)
proof end;

theorem Th16: :: FINSEQ_6:142
for p, q being FinSequence st 1 < len q holds
(p ^' q) . (len (p ^' q)) = q . (len q)
proof end;

theorem Th17: :: FINSEQ_6:143
for p, q being FinSequence holds rng (p ^' q) c= (rng p) \/ (rng q)
proof end;

definition
let D be set ;
let p, q be FinSequence of D;
:: original: ^'
redefine func p ^' q -> FinSequence of D;
coherence
p ^' q is FinSequence of D
proof end;
end;

theorem :: FINSEQ_6:144
for p, q being FinSequence st p <> {} & q <> {} & p . (len p) = q . 1 holds
rng (p ^' q) = (rng p) \/ (rng q)
proof end;

definition
let f be FinSequence;
attr f is TwoValued means :: FINSEQ_6:def 6
card (rng f) = 2;
end;

:: deftheorem defines TwoValued FINSEQ_6:def 6 :
for f being FinSequence holds
( f is TwoValued iff card (rng f) = 2 );

Lm3: now :: thesis: ( len <*1,2*> > 1 & 1 <> 2 & rng <*1,2*> = {1,2} )
set p = <*1,2*>;
2 > 1 ;
hence len <*1,2*> > 1 by FINSEQ_1:44; :: thesis: ( 1 <> 2 & rng <*1,2*> = {1,2} )
thus 1 <> 2 ; :: thesis: rng <*1,2*> = {1,2}
thus rng <*1,2*> = () \/ () by FINSEQ_1:31
.= {1} \/ () by FINSEQ_1:38
.= {1} \/ {2} by FINSEQ_1:38
.= {1,2} by ENUMSET1:1 ; :: thesis: verum
end;

theorem Th19: :: FINSEQ_6:145
for p being FinSequence holds
( p is TwoValued iff ( len p > 1 & ex x, y being object st
( x <> y & rng p = {x,y} ) ) )
proof end;

then Lm4: <*1,2*> is TwoValued
by Lm3;

Lm5: now :: thesis: for i being Nat st 1 <= i & i + 1 <= len <*1,2*> holds
<*1,2*> . i <> <*1,2*> . (i + 1)
let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len <*1,2*> implies <*1,2*> . i <> <*1,2*> . (i + 1) )
set p = <*1,2*>;
assume that
A1: 1 <= i and
A2: i + 1 <= len <*1,2*> ; :: thesis: <*1,2*> . i <> <*1,2*> . (i + 1)
i + 1 <= 1 + 1 by ;
then i <= 1 by XREAL_1:6;
then A3: i = 1 by ;
then <*1,2*> . i = 1 by FINSEQ_1:44;
hence <*1,2*> . i <> <*1,2*> . (i + 1) by ; :: thesis: verum
end;

definition
let f be FinSequence;
attr f is Alternating means :Def4: :: FINSEQ_6:def 7
for i being Nat st 1 <= i & i + 1 <= len f holds
f . i <> f . (i + 1);
end;

:: deftheorem Def4 defines Alternating FINSEQ_6:def 7 :
for f being FinSequence holds
( f is Alternating iff for i being Nat st 1 <= i & i + 1 <= len f holds
f . i <> f . (i + 1) );

Lm6: <*1,2*> is Alternating
by Lm5;

registration
existence
ex b1 being FinSequence st
( b1 is TwoValued & b1 is Alternating )
by ;
end;

theorem Th20: :: FINSEQ_6:146
for a1, a2 being TwoValued Alternating FinSequence st len a1 = len a2 & rng a1 = rng a2 & a1 . 1 = a2 . 1 holds
a1 = a2
proof end;

theorem Th21: :: FINSEQ_6:147
for a1, a2 being TwoValued Alternating FinSequence st a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 holds
for i being Nat st 1 <= i & i <= len a1 holds
a1 . i <> a2 . i
proof end;

theorem :: FINSEQ_6:148
for a1, a2 being TwoValued Alternating FinSequence st a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 holds
for a being TwoValued Alternating FinSequence st len a = len a1 & rng a = rng a1 & not a = a1 holds
a = a2
proof end;

theorem :: FINSEQ_6:149
for X, Y being set
for n being Nat st X <> Y & n > 1 holds
ex a1 being TwoValued Alternating FinSequence st
( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )
proof end;

registration
let X be set ;
let fs be FinSequence of X;
cluster -> FinSubsequence-like for Element of bool fs;
coherence
for b1 being Subset of fs holds b1 is FinSubsequence-like
proof end;
end;

theorem :: FINSEQ_6:150
for f being FinSubsequence
for g, h, fg, fh, fgh being FinSequence st rng g c= dom f & rng h c= dom f & fg = f * g & fh = f * h & fgh = f * (g ^ h) holds
fgh = fg ^ fh
proof end;

theorem :: FINSEQ_6:151
for X being set
for fs being FinSequence of X
for fss being Subset of fs holds
( dom fss c= dom fs & rng fss c= rng fs ) by RELAT_1:11;

theorem :: FINSEQ_6:152
for X being set
for fs being FinSequence of X holds fs is Subset of fs
proof end;

theorem :: FINSEQ_6:153
for X, Y being set
for fs being FinSequence of X
for fss being Subset of fs holds fss | Y is Subset of fs
proof end;

theorem :: FINSEQ_6:154
for X being set
for fs, fs1, fs2 being FinSequence of X
for fss, fss2 being Subset of fs
for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds
Seq fss2 = fs2
proof end;

:: from AMISTD_1, 2006.01.12, A.T.
theorem :: FINSEQ_6:155
for D being non empty set
for f1 being non empty FinSequence of D
for f2 being FinSequence of D holds (f1 ^' f2) /. 1 = f1 /. 1
proof end;

theorem :: FINSEQ_6:156
for D being non empty set
for f1 being FinSequence of D
for f2 being non trivial FinSequence of D holds (f1 ^' f2) /. (len (f1 ^' f2)) = f2 /. (len f2)
proof end;

theorem Th55: :: FINSEQ_6:157
for f being FinSequence holds f ^' {} = f
proof end;

theorem :: FINSEQ_6:158
for x being set
for f being FinSequence holds f ^' <*x*> = f
proof end;

theorem :: FINSEQ_6:159
for D being non empty set
for n being Nat
for f1, f2 being FinSequence of D st 1 <= n & n <= len f1 holds
(f1 ^' f2) /. n = f1 /. n
proof end;

theorem :: FINSEQ_6:160
for D being non empty set
for n being Nat
for f1, f2 being FinSequence of D st 1 <= n & n < len f2 holds
(f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1)
proof end;

:: from SFMASTR3, 2007.07.26, A.T.
definition
let F be FinSequence of INT ;
let m, n be Nat;
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len F ;
func min_at (F,m,n) -> Nat means :Def11: :: FINSEQ_6:def 8
ex X being non empty finite Subset of INT st
( X = rng ((m,n) -cut F) & it + 1 = ((min X) .. ((m,n) -cut F)) + m );
existence
ex b1 being Nat ex X being non empty finite Subset of INT st
( X = rng ((m,n) -cut F) & b1 + 1 = ((min X) .. ((m,n) -cut F)) + m )
proof end;
uniqueness
for b1, b2 being Nat st ex X being non empty finite Subset of INT st
( X = rng ((m,n) -cut F) & b1 + 1 = ((min X) .. ((m,n) -cut F)) + m ) & ex X being non empty finite Subset of INT st
( X = rng ((m,n) -cut F) & b2 + 1 = ((min X) .. ((m,n) -cut F)) + m ) holds
b1 = b2
;
end;

:: deftheorem Def11 defines min_at FINSEQ_6:def 8 :
for F being FinSequence of INT
for m, n being Nat st 1 <= m & m <= n & n <= len F holds
for b4 being Nat holds
( b4 = min_at (F,m,n) iff ex X being non empty finite Subset of INT st
( X = rng ((m,n) -cut F) & b4 + 1 = ((min X) .. ((m,n) -cut F)) + m ) );

theorem Th59: :: FINSEQ_6:161
for F being FinSequence of INT
for m, n, ma being Nat st 1 <= m & m <= n & n <= len F holds
( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds
F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds
F . ma < F . i ) ) )
proof end;

theorem :: FINSEQ_6:162
for F being FinSequence of INT
for m being Nat st 1 <= m & m <= len F holds
min_at (F,m,m) = m
proof end;

definition
let F be FinSequence of INT ;
let m, n be Nat;
pred F is_non_decreasing_on m,n means :: FINSEQ_6:def 9
for i, j being Nat st m <= i & i <= j & j <= n holds
F . i <= F . j;
end;

:: deftheorem defines is_non_decreasing_on FINSEQ_6:def 9 :
for F being FinSequence of INT
for m, n being Nat holds
( F is_non_decreasing_on m,n iff for i, j being Nat st m <= i & i <= j & j <= n holds
F . i <= F . j );

definition
let F be FinSequence of INT ;
let n be Nat;
pred F is_split_at n means :: FINSEQ_6:def 10
for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds
F . i <= F . j;
end;

:: deftheorem defines is_split_at FINSEQ_6:def 10 :
for F being FinSequence of INT
for n being Nat holds
( F is_split_at n iff for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds
F . i <= F . j );

theorem :: FINSEQ_6:163
for F, F1 being FinSequence of INT
for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds
F1 is_non_decreasing_on 1,k + 1
proof end;

theorem :: FINSEQ_6:164
for F, F1 being FinSequence of INT
for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds
F1 is_split_at k + 1
proof end;

:: from SCPISORT, 2011.02.13
theorem :: FINSEQ_6:165
for f being FinSequence of INT
for m, n being Nat st m >= n holds
f is_non_decreasing_on m,n
proof end;

definition
let D be non empty set ;
let f be FinSequence of D;
:: original: constant
redefine attr f is constant means :Def1: :: FINSEQ_6:def 11
for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m;
compatibility
( f is constant iff for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m )
proof end;
end;

:: deftheorem Def1 defines constant FINSEQ_6:def 11 :
for D being non empty set
for f being FinSequence of D holds
( f is constant iff for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m );

theorem Th1: :: FINSEQ_6:166
for D being non empty set
for f being FinSequence of D st f just_once_values f /. (len f) holds
(f /. (len f)) .. f = len f
proof end;

theorem :: FINSEQ_6:167
for D being non empty set
for f being FinSequence of D holds f /^ (len f) = {} by RFINSEQ:27;

theorem Th3: :: FINSEQ_6:168
for D being non empty set
for f being non empty FinSequence of D holds f /. (len f) in rng f
proof end;

definition
let D be non empty set ;
let f be FinSequence of D;
let y be set ;
:: original: just_once_values
redefine pred f just_once_values y means :: FINSEQ_6:def 12
ex x being set st
( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) );
compatibility
( f just_once_values y iff ex x being set st
( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) ) )
proof end;
end;

:: deftheorem defines just_once_values FINSEQ_6:def 12 :
for D being non empty set
for f being FinSequence of D
for y being set holds
( f just_once_values y iff ex x being set st
( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) ) );

theorem Th4: :: FINSEQ_6:169
for D being non empty set
for f being FinSequence of D st f just_once_values f /. (len f) holds
f -: (f /. (len f)) = f
proof end;

theorem Th5: :: FINSEQ_6:170
for D being non empty set
for f being FinSequence of D st f just_once_values f /. (len f) holds
f :- (f /. (len f)) = <*(f /. (len f))*>
proof end;

theorem Th6: :: FINSEQ_6:171
for D being non empty set
for p being Element of D
for f being FinSequence of D holds 1 <= len (f :- p)
proof end;

theorem :: FINSEQ_6:172
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
proof end;

theorem :: FINSEQ_6:173
for D being non empty set
for f being non empty circular FinSequence of D holds Rev f is circular
proof end;

theorem Th9: :: FINSEQ_6:174
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 & 1 <= i & i <= len (f :- p) holds
(Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f))
proof end;

theorem Th10: :: FINSEQ_6:175
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 & p .. f <= i & i <= len f holds
f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))
proof end;

theorem :: FINSEQ_6:176
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)
proof end;

NAT27: for i, j being Nat st j < i holds
(i -' (j + 1)) + 1 = i -' j

proof end;

theorem Th12: :: FINSEQ_6:177
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 & len (f :- p) < i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
proof end;

theorem :: FINSEQ_6:178
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 & 1 < i & i <= p .. f holds
f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
proof end;

theorem Th14: :: FINSEQ_6:179
for D being non empty set
for p being Element of D
for f being FinSequence of D holds len (Rotate (f,p)) = len f
proof end;

theorem Th15: :: FINSEQ_6:180
for D being non empty set
for p being Element of D
for f being FinSequence of D holds dom (Rotate (f,p)) = dom f
proof end;

theorem :: FINSEQ_6:181
for D being non empty set
for f being circular FinSequence of D
for p being Element of D st ( for i being Nat st 1 < i & i < len f holds
f /. i <> f /. 1 ) holds
Rotate ((Rotate (f,p)),(f /. 1)) = f
proof end;

theorem Th17: :: FINSEQ_6:182
for i being Nat
for D being non empty set
for p being Element of D
for f being circular FinSequence of D st p in rng f & len (f :- p) <= i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
proof end;

theorem Th18: :: FINSEQ_6:183
for i being Nat
for D being non empty set
for p being Element of D
for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds
f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
proof end;

registration
let D be non trivial set ;
existence
ex b1 being FinSequence of D st
( b1 is V25() & b1 is circular )
proof end;
end;

registration
let D be non trivial set ;
let p be Element of D;
let f be V25() circular FinSequence of D;
cluster Rotate (f,p) -> V25() ;
coherence
not Rotate (f,p) is constant
proof end;
end;