<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

Data publikacji: 23 lut 2019

Zakres stron: 199 - 208

Przyjęty: 29 wrz 2018

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

Słowa kluczowe
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

Data publikacji: 23 lut 2019

Zakres stron: 199 - 208

Przyjęty: 29 wrz 2018

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

Słowa kluczowefinite sequences, functions, relations

© 2018 Rafał Ziobro, published by Sciendo

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

Słowa kluczowe
finite sequences, functions, relations