<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

Publié en ligne: 23 févr. 2019

Pages: 199 - 208

Accepté: 29 sept. 2018

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

Mots clés
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

Publié en ligne: 23 févr. 2019

Pages: 199 - 208

Accepté: 29 sept. 2018

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

Mots clésfinite sequences, functions, relations

© 2018 Rafał Ziobro, published by Sciendo

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

Mots clés
finite sequences, functions, relations