@misc{FINSEQ_9.MIZ,
  AUTHOR = {Ziobro, Rafa{\l}},
  TITLE = {Arithmetic Operations on Short Finite Sequences},
  ADDRESS1 = {Department of Carbohydrate Technology, University of Agriculture in Krakow},
  DAY = {29},
  MONTH = {September},
  YEAR = {2018},
  ACKNOWLEDGEMENT = {Ad Maiorem Dei Gloriam},
  KEYWORDS = {finite sequences, functions, relations},
  MSC2010 = {11B99 03B35},
  SUMMARY = {In contrast to other proving systems Mizar Mathematical Library
  is maintained as a single base of theorems, which allows the users
  to benefit from earlier formalized items \cite{Bancerek2017}. This
  eventually leads to a development of certain
  branches of articles using common notation and ideas. Such formalism for
  finite sequences has been developed since 1989 \cite{FINSEQ_1.ABS} and
  further developed despite of the controversy over indexing which
  excludes zero \cite{Rudnicki2003}.
  The article aims to add some new machinery for
  dealing with finite sequences, especially those of short length.}}

@Article{Bancerek2017,
  author        = {Bancerek, Grzegorz and Byliński, Czesław and Grabowski, Adam and Korniłowicz, Artur and Matuszewski, Roman and Naumowicz, Adam and P±k, Karol},
  journal       = {Journal of Automated Reasoning},
  pages         = {1},
  title         = {The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar},
  year          = {2017},
  month         = nov,
  date          = {2017-11-25},
  doi           = {10.1007/s10817-017-9440-6},
  issn          = {1573-0670},
  publisher     = {Springer},
  timestamp     = {2018.01.31},
  url           = {http://dx.doi.org/10.1007/s10817-017-9440-6},
}


@Article{Rudnicki2003,
  author        = {Rudnicki, Piotr and Trybulec, Andrzej},
  journal       = {Mathematical Knowledge Management},
  title         = {On the Integrity of a Repository of Formalized Mathematics},
  year          = {2003},
  month         = jan,
  date          = {2003-01-01},
  doi           = {10.1007/3-540-36469-2_13},
  publisher     = {Springer},
  timestamp     = {2018.01.31},
  url           = {http://dx.doi.org/10.1007/3-540-36469-2_13},
}
}
