<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

Published Online: Feb 23, 2019

Page range: 199 - 208

Accepted: Sep 29, 2018

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

Keywords
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

Published Online: Feb 23, 2019

Page range: 199 - 208

Accepted: Sep 29, 2018

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

Keywordsfinite sequences, functions, relations

© 2018 Rafał Ziobro, published by Sciendo

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

Keywords
finite sequences, functions, relations