Segments of Natural Numbers and Finite Sequences
Grzegorz Bancerek, Krzysztof Hryniewiecki · 1990
Summary. We define the notion of an initial segment of natural numbers and prove a number of their properties. Using this notion we introduce finite sequences, subsequences, the empty sequence, a sequence of a domain, and the operation of concatenation of two sequences. MML Identifier:FINSEQ_1. WWW:http://mizar.org/JFM/Vol1/finseq_1.html