Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

### Zero-Based Finite Sequences

by
Tetsuya Tsunetou,
Grzegorz Bancerek, and
Yatsuka Nakamura

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

```environ

vocabulary FUNCT_1, BOOLE, ORDINAL1, FINSEQ_1, FINSET_1, RELAT_1, ORDINAL2,
CARD_1, TARSKI, PARTFUN1, ALGSEQ_1, ARYTM_1, FUNCT_4, FINSEQ_7, CAT_1,
AFINSQ_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, RELAT_1,
FUNCT_1, ORDINAL1, ORDINAL2, ORDINAL4, REAL_1, NAT_1, PARTFUN1, FINSET_1,
CARD_1, FINSEQ_1, FUNCT_4, CQC_LANG, FUNCT_7;
constructors REAL_1, NAT_1, WELLORD2, CQC_LANG, FUNCT_7, ORDINAL4, XREAL_0,
MEMBERED;
clusters FUNCT_1, RELAT_1, RELSET_1, CARD_1, SUBSET_1, ORDINAL1, ARYTM_3,
FUNCT_7, NAT_1, XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve k,m,n for Nat,
x,y,z,y1,y2,X,Y for set,
f,g for Function;

:::::::::::::::::::::::::::::::::::::::::::::::
::                                           ::
::   Extended Segments of Natural Numbers    ::
::                                           ::
:::::::::::::::::::::::::::::::::::::::::::::::

theorem :: AFINSQ_1:1
n in n+1;

theorem :: AFINSQ_1:2
k <= n implies k = k /\ n;

theorem :: AFINSQ_1:3
k = k /\ n implies k <= n;

theorem :: AFINSQ_1:4   :: ORDINAL1:def 1, CARD_1:52
n \/ { n } = n+1;

theorem :: AFINSQ_1:5
Seg n c= n+1;

theorem :: AFINSQ_1:6
n+1 = {0} \/ Seg n;

::::::::::::::::::::::::::::::::
::                            ::
::  Finite ExFinSequences     ::
::                            ::
::::::::::::::::::::::::::::::::

theorem :: AFINSQ_1:7
for r being Function holds
r is finite T-Sequence-like iff ex n st dom r = n;

definition
cluster finite T-Sequence-like Function;
end;

definition
mode XFinSequence is finite T-Sequence;
end;

reserve p,q,r,s,t for XFinSequence;

definition
cluster natural -> finite set;
let p;
cluster dom p -> natural;
end;

definition let p;
redefine func Card p -> Nat means
:: AFINSQ_1:def 1
it = dom p;
synonym len p;
end;

definition let p;
redefine func dom p -> Subset of NAT;
end;

theorem :: AFINSQ_1:8
(ex k st dom f c= k) implies ex p st f c= p;

scheme XSeqEx{A()->Nat,P[set,set]}:
ex p st dom p = A() & for k st k in A() holds P[k,p.k]
provided
for k,y1,y2 st k in A() & P[k,y1] & P[k,y2] holds y1=y2
and
for k st k in A() ex x st P[k,x];

scheme XSeqLambda{A()->Nat,F(set) -> set}:
ex p being XFinSequence st len p = A() & for k st k in A() holds p.k=F(k);

theorem :: AFINSQ_1:9
z in p implies ex k st (k in dom p & z=[k,p.k]);

theorem :: AFINSQ_1:10
dom p = dom q & (for k st k in dom p holds p.k = q.k) implies p=q;

theorem :: AFINSQ_1:11
( len p = len q & for k st k < len p holds p.k=q.k ) implies p=q;

theorem :: AFINSQ_1:12
p|n is XFinSequence;

theorem :: AFINSQ_1:13
rng p c= dom f implies f*p is XFinSequence;

theorem :: AFINSQ_1:14
k < len p & q = p|k implies len q = k & dom q = k;

:::::::::::::::::::::::::::::::::
::                             ::
::    XFinSequences of D       ::
::                             ::
:::::::::::::::::::::::::::::::::

definition let D be set;
cluster finite T-Sequence of D;
end;

definition let D be set;
mode XFinSequence of D is finite T-Sequence of D;
end;

theorem :: AFINSQ_1:15
for D being set, f being XFinSequence of D holds f is PartFunc of NAT,D;

definition
cluster {} -> T-Sequence-like;
end;

definition let D be set;
cluster finite T-Sequence-like PartFunc of NAT,D;
end;

reserve D for set;

theorem :: AFINSQ_1:16
for p being XFinSequence of D holds p|k is XFinSequence of D;

theorem :: AFINSQ_1:17
for D being non empty set
ex p being XFinSequence of D st len p = k;

::::::::::::::::::::::::::::::::::::
::                                ::
::    The Empty XFinSequence      ::
::                                ::
::::::::::::::::::::::::::::::::::::

definition
cluster empty XFinSequence;
end;

theorem :: AFINSQ_1:18
len p = 0 iff p = {};

theorem :: AFINSQ_1:19
for D be set holds {} is XFinSequence of D;

definition
let D be set;
cluster empty XFinSequence of D;
end;

definition let x;
func <%x%> -> set equals
:: AFINSQ_1:def 2
{ [0,x] };
end;

definition let D be set;
func <%>D -> empty XFinSequence of D equals
:: AFINSQ_1:def 3
{};
end;

definition let p,q;
cluster p^q -> finite;
redefine func p^q means
:: AFINSQ_1:def 4
dom it = len p + len q &
(for k st k in dom p holds it.k=p.k) &
(for k st k in dom q holds it.(len p + k) = q.k);
end;

theorem :: AFINSQ_1:20
len(p^q) = len p + len q;

theorem :: AFINSQ_1:21
(len p <= k & k < len p + len q) implies (p^q).k=q.(k-len p);

theorem :: AFINSQ_1:22
len p <= k & k < len(p^q) implies (p^q).k = q.(k - len p);

theorem :: AFINSQ_1:23
k in dom (p^q) implies
(k in dom p or (ex n st n in dom q & k=len p + n));

theorem :: AFINSQ_1:24
for p,q being T-Sequence holds dom p c= dom(p^q);

theorem :: AFINSQ_1:25
x in dom q implies ex k st k=x & len p + k in dom(p^q);

theorem :: AFINSQ_1:26
k in dom q implies len p + k in dom(p^q);

theorem :: AFINSQ_1:27
rng p c= rng(p^q);

theorem :: AFINSQ_1:28
rng q c= rng(p^q);

theorem :: AFINSQ_1:29
rng(p^q) = rng p \/ rng q;

theorem :: AFINSQ_1:30
p^q^r = p^(q^r);

theorem :: AFINSQ_1:31
p^r = q^r or r^p = r^q implies p = q;

theorem :: AFINSQ_1:32
p^{} = p & {}^p = p;

theorem :: AFINSQ_1:33
p^q = {} implies p={} & q={};

definition let D be set;let p,q be XFinSequence of D;
redefine func p^q -> T-Sequence of D;
end;

definition let x;
redefine func <%x%> -> Function means
:: AFINSQ_1:def 5
dom it = 1 & it.0 = x;
end;

definition let x;
cluster <%x%> -> Function-like Relation-like;
end;

definition let x;
cluster <%x%> -> finite T-Sequence-like;
end;

theorem :: AFINSQ_1:34
p^q is XFinSequence of D implies
p is XFinSequence of D & q is XFinSequence of D;

definition let x,y;
func <%x,y%> -> set equals
:: AFINSQ_1:def 6
<%x%>^<%y%>;

let z;
func <%x,y,z%> -> set equals
:: AFINSQ_1:def 7
<%x%>^<%y%>^<%z%>;
end;

definition let x,y;
cluster <%x,y%> -> Function-like Relation-like;

let z;
cluster <%x,y,z%> -> Function-like Relation-like;
end;

definition let x,y;
cluster <%x,y%> -> finite T-Sequence-like;

let z;
cluster <%x,y,z%> -> finite T-Sequence-like;
end;

theorem :: AFINSQ_1:35
<%x%> = { [0,x] };

theorem :: AFINSQ_1:36
p=<%x%> iff dom p = 1 & rng p = {x};

theorem :: AFINSQ_1:37
p=<%x%> iff len p = 1 & rng p = {x};

theorem :: AFINSQ_1:38
p = <%x%> iff len p = 1 & p.0 = x;

theorem :: AFINSQ_1:39
(<%x%>^p).0 = x;

theorem :: AFINSQ_1:40
(p^<%x%>).(len p)=x;

theorem :: AFINSQ_1:41
<%x,y,z%>=<%x%>^<%y,z%> &
<%x,y,z%>=<%x,y%>^<%z%>;

theorem :: AFINSQ_1:42
p = <%x,y%> iff len p = 2 & p.0=x & p.1=y;

theorem :: AFINSQ_1:43
p = <%x,y,z%> iff len p = 3 & p.0 = x & p.1 = y & p.2 = z;

theorem :: AFINSQ_1:44
p <> {} implies ex q,x st p=q^<%x%>;

definition let D be non empty set; let x be Element of D;
redefine func <%x%> -> XFinSequence of D;
end;

:: scheme of induction for extended finite sequences ::

scheme IndXSeq{P[XFinSequence]}:
for p holds P[p]
provided
P[{}] and
for p,x st P[p] holds P[p^<%x%>];

theorem :: AFINSQ_1:45
for p,q,r,s being XFinSequence st p^q = r^s & len p <= len r
ex t being XFinSequence st p^t = r;

definition let D be set;
func D^omega -> set means
:: AFINSQ_1:def 8
x in it iff x is XFinSequence of D;
end;

definition let D be set;
cluster D^omega -> non empty;
end;

theorem :: AFINSQ_1:46
x in D^omega iff x is XFinSequence of D;

theorem :: AFINSQ_1:47
{} in D^omega;

scheme SepXSeq{D()->non empty set, P[XFinSequence]}:
ex X st (for x holds x in X iff ex p st p in D()^omega & P[p] & x=p);

definition
let p be XFinSequence;
let i,x be set;
cluster p+*(i,x) -> finite T-Sequence-like;
redefine func p+*(i,x); synonym Replace(p,i,x);
end;

theorem :: AFINSQ_1:48
for p being XFinSequence, i being Nat, x being set holds
len Replace(p,i,x) = len p &
(i < len p implies Replace(p,i,x).i = x) &
for j being Nat st j <> i holds Replace(p,i,x).j = p.j;

definition
let D be non empty set;
let p be XFinSequence of D;
let i be Nat, a be Element of D;
redefine func Replace(p,i,a) -> XFinSequence of D;
end;

```