<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In contrast to other proving systems Mizar Mathematical Library, considered as one of the largest formal mathematical libraries [4], is maintained as a single base of theorems, which allows the users to benefit from earlier formalized items [3], [2]. 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 [1] and further developed despite of the controversy over indexing which excludes zero [6], also for some advanced and new mathematics [5].</p><p>The article aims to add some new machinery for dealing with finite sequences, especially those of short length.</p></abstract>

In contrast to other proving systems Mizar Mathematical Library, considered as one of the largest formal mathematical libraries [4], is maintained as a single base of theorems, which allows the users to benefit from earlier formalized items [3], [2]. 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 [1] and further developed despite of the controversy over indexing which excludes zero [6], also for some advanced and new mathematics [5].The article aims to add some new machinery for dealing with finite sequences, especially those of short length.

Arithmetic Operations on Short Finite Sequences

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Arithmetic Operations on Short Finite Sequences"}

In contrast to other proving systems Mizar Mathematical Library, considered as one of the largest formal mathematical libraries [4], is maintained as a single...

Arithmetic Operations on Short Finite Sequences

Publicado en línea: 23 feb 2019

Páginas: 199 - 208

Aceptado: 29 sept 2018

DOI: https://doi.org/10.2478/forma-2018-0018

Palabras clave
finite sequences, functions, relations

© 2018 Rafał Ziobro, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Arithmetic Operations on Short Finite Sequences

Publicado en línea: 23 feb 2019

Páginas: 199 - 208

Aceptado: 29 sept 2018

DOI: https://doi.org/10.2478/forma-2018-0018

Palabras clavefinite sequences, functions, relations

© 2018 Rafał Ziobro, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Palabras clave
finite sequences, functions, relations