Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

### On the Decomposition of Finite Sequences

by
Andrzej Trybulec

MML identifier: FINSEQ_6
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, REALSET1, FINSEQ_5, RELAT_1, BOOLE, FUNCT_1, FINSEQ_4,
ARYTM_1, RLSUB_2, RFINSEQ, FINSEQ_6, ORDINAL2, ARYTM;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS,
XCMPLX_0, XREAL_0, NAT_1, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_4,
RFINSEQ, FINSEQ_5, REALSET1, TOPREAL1;
constructors REAL_1, NAT_1, MATRIX_2, FINSEQ_5, ENUMSET1, RFINSEQ, TOPREAL1,
REALSET1, FINSEQ_4, INT_1, MEMBERED, XBOOLE_0;
clusters RELSET_1, FINSEQ_5, FUNCT_1, GOBOARD4, FINSEQ_1, INT_1, REALSET1,
ZFMISC_1, XBOOLE_0, ORDINAL2, ARYTM_3;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin :: Preliminaries

reserve x,y,z for set;

definition let x,y,z;
cluster <*x,y,z*> -> non trivial;
end;

definition let f be non empty FinSequence;
cluster Rev f -> non empty;
end;

begin

reserve f,f1,f2,f3 for FinSequence,
p,p1,p2,p3 for set,
i,k for Nat;

canceled 2;

theorem :: FINSEQ_6:3
for X being set, i st X c= Seg i & 1 in X holds (Sgm X).1 = 1;

theorem :: FINSEQ_6:4
for f being FinSequence holds
k in dom f & (for i st 1 <= i & i < k holds f.i <> f.k)
implies (f.k)..f = k;

theorem :: FINSEQ_6:5
<*p1,p2*>| Seg 1 = <*p1*>;

theorem :: FINSEQ_6:6
<*p1,p2,p3*>| Seg 1 = <*p1*>;

theorem :: FINSEQ_6:7
<*p1,p2,p3*>| Seg 2 = <*p1,p2*>;

theorem :: FINSEQ_6:8
p in rng f1 implies p..(f1^f2) = p..f1;

theorem :: FINSEQ_6:9
p in rng f2 \ rng f1 implies p..(f1^f2) = len f1 + p..f2;

theorem :: FINSEQ_6:10
p in rng f1 implies (f1^f2)|--p = (f1|--p)^f2;

theorem :: FINSEQ_6:11
p in rng f2 \ rng f1 implies (f1^f2)|--p = f2|--p;

theorem :: FINSEQ_6:12
f1 c= f1^f2;

theorem :: FINSEQ_6:13
for A being set st A c= dom f1 holds (f1^f2)|A = f1 | A;

theorem :: FINSEQ_6:14
p in rng f1 implies (f1^f2)-|p = f1-|p;

definition let f1; let i be natural number;
cluster f1|Seg i -> FinSequence-like;
end;

theorem :: FINSEQ_6:15
f1 c= f2 implies f3^f1 c= f3^f2;

theorem :: FINSEQ_6:16
(f1^f2)|Seg(len f1 + i) = f1^(f2|Seg i);

theorem :: FINSEQ_6:17
p in rng f2 \ rng f1 implies (f1^f2)-|p = f1^(f2-|p);

canceled;

theorem :: FINSEQ_6:19
f1^f2 just_once_values p implies p in rng f1 \+\ rng f2;

theorem :: FINSEQ_6:20
f1^f2 just_once_values p & p in rng f1 implies f1 just_once_values p;

theorem :: FINSEQ_6:21
rng f is non trivial implies f is non trivial;

theorem :: FINSEQ_6:22
p..<*p*> = 1;

theorem :: FINSEQ_6:23
p1..<*p1,p2*> = 1;

theorem :: FINSEQ_6:24
p1 <> p2 implies p2..<*p1,p2*> = 2;

theorem :: FINSEQ_6:25
p1..<*p1,p2,p3*> = 1;

theorem :: FINSEQ_6:26
p1 <> p2 implies p2..<*p1,p2,p3*> = 2;

theorem :: FINSEQ_6:27
p1 <> p3 & p2 <> p3 implies p3..<*p1,p2,p3*> = 3;

theorem :: FINSEQ_6:28
for f being FinSequence holds
Rev(<*p*>^f) = Rev f ^ <*p*>;

theorem :: FINSEQ_6:29
for f being FinSequence holds
Rev Rev f = f;

theorem :: FINSEQ_6:30
x <> y implies <*x,y*> -| y = <*x*>;

theorem :: FINSEQ_6:31
x <> y implies <*x,y,z*> -| y = <*x*>;

theorem :: FINSEQ_6:32
x <> z & y <> z implies <*x,y,z*> -| z = <*x,y*>;

theorem :: FINSEQ_6:33
<*x,y*>|--x = <*y*>;

theorem :: FINSEQ_6:34
x <> y implies <*x,y,z*>|--y = <*z*>;

theorem :: FINSEQ_6:35
<*x,y,z*>|--x = <*y,z*>;

theorem :: FINSEQ_6:36
<*z*>|--z = {} & <*z*>-|z = {};

theorem :: FINSEQ_6:37
x <> y implies <*x,y*> |-- y = {};

theorem :: FINSEQ_6:38
x <> z & y <> z implies <*x,y,z*> |-- z = {};

theorem :: FINSEQ_6:39
x in rng f & y in rng(f-|x) implies f-|x-|y = f-|y;

theorem :: FINSEQ_6:40
not x in rng f1 implies x..(f1^<*x*>^f2) = len f1 + 1;

theorem :: FINSEQ_6:41
f just_once_values x implies x..f + x..Rev f = len f + 1;

theorem :: FINSEQ_6:42
f just_once_values x implies Rev(f-|x) = Rev f |--x;

theorem :: FINSEQ_6:43
f just_once_values x implies Rev f just_once_values x;

begin

reserve D for non empty set,
p,p1,p2,p3 for Element of D,
f,f1,f2 for FinSequence of D;

theorem :: FINSEQ_6:44
p in rng f implies f-:p = (f -| p)^<*p*>;

theorem :: FINSEQ_6:45
p in rng f implies f:-p = <*p*>^(f |-- p);

theorem :: FINSEQ_6:46
f <> {} implies f/.1 in rng f;

theorem :: FINSEQ_6:47
f <> {} implies f/.1..f = 1;

theorem :: FINSEQ_6:48
f <> {} & f/.1 = p implies f-:p = <*p*> & f:-p = f;

theorem :: FINSEQ_6:49
(<*p1*>^f)/^1 = f;

theorem :: FINSEQ_6:50
<*p1,p2*>/^1 = <*p2*>;

theorem :: FINSEQ_6:51
<*p1,p2,p3*>/^1 = <*p2,p3*>;

theorem :: FINSEQ_6:52
k in dom f & (for i st 1 <= i & i < k holds f/.i <> f/.k)
implies f/.k..f = k;

theorem :: FINSEQ_6:53
p1 <> p2 implies <*p1,p2*>-:p2 = <*p1,p2*>;

theorem :: FINSEQ_6:54
p1 <> p2 implies <*p1,p2,p3*>-:p2 = <*p1,p2*>;

theorem :: FINSEQ_6:55
p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*>-:p3 = <*p1,p2,p3*>;

theorem :: FINSEQ_6:56
<*p*>:-p = <*p*> & <*p*>-:p = <*p*>;

theorem :: FINSEQ_6:57
p1 <> p2 implies <*p1,p2*>:-p2 = <*p2*>;

theorem :: FINSEQ_6:58
p1 <> p2 implies <*p1,p2,p3*>:-p2 = <*p2,p3*>;

theorem :: FINSEQ_6:59
p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*>:-p3 = <*p3*>;

canceled;

theorem :: FINSEQ_6:61
p in rng f & p..f > k implies p..f = k + p..(f/^k);

theorem :: FINSEQ_6:62
p in rng f & p..f > k implies p in rng(f/^k);

theorem :: FINSEQ_6:63
k < i & i in dom f implies f/.i in rng(f/^k);

theorem :: FINSEQ_6:64
p in rng f & p..f > k implies (f/^k)-:p = (f-:p)/^k;

theorem :: FINSEQ_6:65
p in rng f & p..f <> 1 implies (f/^1)-:p = (f-:p)/^1;

theorem :: FINSEQ_6:66
p in rng(f:-p);

theorem :: FINSEQ_6:67
x in rng f & p in rng f & x..f >= p..f implies x in rng(f:-p);

theorem :: FINSEQ_6:68
p in rng f & k <= len f & k >= p..f implies f/.k in rng(f:-p);

theorem :: FINSEQ_6:69
p in rng f1 implies (f1^f2):-p = (f1:-p)^f2;

theorem :: FINSEQ_6:70
p in rng f2 \ rng f1 implies (f1^f2):-p = f2:-p;

theorem :: FINSEQ_6:71
p in rng f1 implies (f1^f2)-:p = f1-:p;

theorem :: FINSEQ_6:72
p in rng f2 \ rng f1 implies (f1^f2)-:p = f1^(f2-:p);

theorem :: FINSEQ_6:73
f:-p:-p = f:-p;

theorem :: FINSEQ_6:74
p1 in rng f & p2 in rng f \ rng(f-:p1) implies f|--p2 = f|--p1|--p2;

theorem :: FINSEQ_6:75
p in rng f implies rng f = rng(f-:p) \/ rng(f:-p);

theorem :: FINSEQ_6:76
p1 in rng f & p2 in rng f \ rng(f-:p1) implies f:-p1:-p2 = f:-p2;

theorem :: FINSEQ_6:77
p in rng f implies p..(f-:p) = p..f;

theorem :: FINSEQ_6:78
f|i|i = f|i;

theorem :: FINSEQ_6:79
p in rng f implies f-:p-:p = f-:p;

theorem :: FINSEQ_6:80
p1 in rng f & p2 in rng(f-:p1) implies f-:p1-:p2 = f-:p2;

theorem :: FINSEQ_6:81
p in rng f implies (f-:p)^((f:-p)/^1) = f;

theorem :: FINSEQ_6:82
f1 <> {} implies (f1^f2)/^1 = (f1/^1)^f2;

theorem :: FINSEQ_6:83
p2 in rng f & p2..f <> 1 implies p2 in rng(f/^1);

theorem :: FINSEQ_6:84
p..(f:-p) = 1;

canceled;

theorem :: FINSEQ_6:86
<*>D/^k = <*>D;

theorem :: FINSEQ_6:87
f/^(i+k) = f/^i/^k;

theorem :: FINSEQ_6:88
p in rng f & p..f > k implies (f/^k):-p = f:-p;

theorem :: FINSEQ_6:89
p in rng f & p..f <> 1 implies (f/^1):-p = f:-p;

theorem :: FINSEQ_6:90
i + k = len f implies Rev(f/^k) = Rev f|i;

theorem :: FINSEQ_6:91
i + k = len f implies Rev(f|k) = Rev f/^i;

theorem :: FINSEQ_6:92
f just_once_values p implies Rev(f|--p) = Rev f -|p;

theorem :: FINSEQ_6:93
f just_once_values p implies Rev(f:-p) = Rev f -:p;

theorem :: FINSEQ_6:94
f just_once_values p implies Rev(f-:p) = Rev f :-p;

begin :: rotation, circular

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

definition let D,f,p;
func Rotate(f,p) -> FinSequence of D equals
:: FINSEQ_6:def 2
(f:-p)^((f-:p)/^1) if p in rng f
otherwise f;
end;

definition let D; let f be non empty FinSequence of D, p be Element of D;
cluster Rotate(f,p) -> non empty;
end;

definition let D;
cluster circular non empty trivial FinSequence of D;
cluster circular non empty non trivial FinSequence of D;
end;

theorem :: FINSEQ_6:95
Rotate(f,f/.1) = f;

definition let D,p; let f be circular non empty FinSequence of D;
cluster Rotate(f,p) -> circular;
end;

theorem :: FINSEQ_6:96
f is circular & p in rng f implies rng Rotate(f,p) = rng f;

theorem :: FINSEQ_6:97
p in rng f implies p in rng Rotate(f,p);

theorem :: FINSEQ_6:98
p in rng f implies (Rotate(f,p))/.1 = p;

theorem :: FINSEQ_6:99
Rotate(Rotate(f,p),p) = Rotate(f,p);

theorem :: FINSEQ_6:100
Rotate(<*p*>,p) = <*p*>;

theorem :: FINSEQ_6:101
Rotate(<*p1,p2*>,p1) = <*p1,p2*>;

theorem :: FINSEQ_6:102
Rotate(<*p1,p2*>,p2) = <*p2,p2*>;

theorem :: FINSEQ_6:103
Rotate(<*p1,p2,p3*>,p1) = <*p1,p2,p3*>;

theorem :: FINSEQ_6:104
p1 <> p2 implies Rotate(<*p1,p2,p3*>,p2) = <*p2,p3,p2*>;

theorem :: FINSEQ_6:105
p2 <> p3 implies Rotate(<*p1,p2,p3*>,p3) = <*p3,p2,p3*>;

theorem :: FINSEQ_6:106
for f being circular non trivial FinSequence of D
holds rng(f/^1) = rng f;

theorem :: FINSEQ_6:107
rng(f/^1) c= rng Rotate(f,p);

theorem :: FINSEQ_6:108
p2 in rng f \ rng(f-:p1) implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2);

theorem :: FINSEQ_6:109
p2..f <> 1 & p2 in rng f \ rng(f:-p1)
implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2);

theorem :: FINSEQ_6:110
p2 in rng(f/^1) & f just_once_values p2
implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2);

theorem :: FINSEQ_6:111
f is circular & f just_once_values p2
implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2);

theorem :: FINSEQ_6:112
f is circular & f just_once_values p implies
Rev Rotate(f,p) = Rotate(Rev f,p);

```