<abstract xmlns="http://www.w3.org/1999/xhtml"><p>The coexistence of “classical” <italic>finite sequences</italic> [1] and their zero-based equivalents <italic>finite 0-sequences</italic> [6] in Mizar has been regarded as a disadvantage. However the suggested replacement of the former type with the latter [5] has not yet been implemented, despite of several advantages of this form, such as the identity of length and domain operators [4]. On the other hand the number of theorems formalized using <italic>finite sequence</italic> notation is much larger then of those based on <italic>finite 0-sequences</italic>, so such translation would require quite an effort.</p><p>The paper addresses this problem with another solution, using the Mizar system [3], [2]. Instead of removing one notation it is possible to introduce operators which would concatenate sequences of various types, and in this way allow utilization of the whole range of formalized theorems. While the operation could replace existing FS2XFS, XFS2FS commands (by using empty sequences as initial elements) its universal notation (independent on sequences that are concatenated to the initial object) allows to “forget” about the type of sequences that are concatenated on further positions, and thus simplify the proofs.</p></abstract>

The coexistence of “classical” finite sequences [1] and their zero-based equivalents finite 0-sequences [6] in Mizar has been regarded as a disadvantage. However the suggested replacement of the former type with the latter [5] has not yet been implemented, despite of several advantages of this form, such as the identity of length and domain operators [4]. On the other hand the number of theorems formalized using finite sequence notation is much larger then of those based on finite 0-sequences, so such translation would require quite an effort.The paper addresses this problem with another solution, using the Mizar system [3], [2]. Instead of removing one notation it is possible to introduce operators which would concatenate sequences of various types, and in this way allow utilization of the whole range of formalized theorems. While the operation could replace existing FS2XFS, XFS2FS commands (by using empty sequences as initial elements) its universal notation (independent on sequences that are concatenated to the initial object) allows to “forget” about the type of sequences that are concatenated on further positions, and thus simplify the proofs.

Concatenation of Finite Sequences

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 Public License.

{"article-title":"Concatenation of Finite Sequences"}

The coexistence of “classical” finite sequences [1] and their zero-based equivalents finite 0-sequences [6] in Mizar has been regarded as a disadvantage....

Concatenation of Finite Sequences

Publié en ligne: 16 mai 2019

Pages: 1 - 13

Accepté: 27 févr. 2019

DOI: https://doi.org/10.2478/forma-2019-0001

Mots clés
finite sequence, finite 0-sequence, concatenation

© 2019 Rafał Ziobro, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 Public License.

Concatenation of Finite Sequences

Publié en ligne: 16 mai 2019

Pages: 1 - 13

Accepté: 27 févr. 2019

DOI: https://doi.org/10.2478/forma-2019-0001

Mots clésfinite sequence, finite 0-sequence, concatenation

© 2019 Rafał Ziobro, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 Public License.

Mots clés
finite sequence, finite 0-sequence, concatenation