The abstract of the Mizar article:

Zero-Based Finite Sequences

by

Tetsuya Tsunetou,

Grzegorz Bancerek, and

Yatsuka Nakamura

Received September 28, 2001

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;