<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

Publicado en línea: 16 may 2019

Páginas: 1 - 13

Aceptado: 27 feb 2019

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

Palabras clave
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

Publicado en línea: 16 may 2019

Páginas: 1 - 13

Aceptado: 27 feb 2019

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

Palabras clavefinite 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.

Palabras clave
finite sequence, finite 0-sequence, concatenation