Concatenation of Finite Sequences

Rafał Ziobro


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 thisform, 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 Mizarsystem [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
Author Rafał Ziobro (FoFT / DoCT)
Rafał Ziobro,,
- Department of Carbohydrate Technology
Journal seriesFormalized Mathematics, ISSN 1426-2630, e-ISSN 1898-9934, (N/A 20 pkt, Not active)
Issue year2019
Publication size in sheets0.6
Keywords in Englishfinite sequence, finite 0-sequence; concatenation
ASJC Classification2604 Applied Mathematics; 2605 Computational Mathematics
Internal identifierWTŻ/2019/38
Languageen angielski
LicenseJournal (articles only); author's original; Uznanie Autorstwa - Na Tych Samych Warunkach (CC-BY-SA); after publication
Concatenation of Finite Sequences of 27-05-2019
250,4 KB
Score (nominal)20
Score sourcejournalList
Publication indicators WoS Citations = 0; Scopus SNIP (Source Normalised Impact per Paper): 2018 = 0.169
Citation count*
Additional fields
Udział procentowyR. Ziobro: 100%
Share Share

Get link to the record

* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.
Are you sure?