## Concatenation of Finite Sequences

### Rafał Ziobro

#### 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 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
Vol27
No1
Pages1-13
Publication size in sheets0.6
Keywords in Englishfinite sequence, finite 0-sequence; concatenation
ASJC Classification2604 Applied Mathematics; 2605 Computational Mathematics
DOIDOI:10.2478/forma-2019-0001
URL http://mizar.org/fm/fm27-1/27-1.pdf
Internal identifierWTŻ/2019/38
Languageen angielski
LicenseJournal (articles only); author's original; Uznanie Autorstwa - Na Tych Samych Warunkach (CC-BY-SA); after publication
File
 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*