[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. <em>Formalized Mathematics</em>, 1(<bold>1</bold>):107–114, 1990.
[4] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, <em>Intelligent Computer Mathematics</em>, volume 9150 of <em>Lecture Notes in Computer Science</em>, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi: <a href="https://doi.org/10.1007/978-3-319-20615-817." target="_blank" rel="noopener noreferrer" class="text-signal-blue hover:underline">10.1007/978-3-319-20615-817.</a><pub-id pub-id-type="doi"><a href="https://doi.org/10.1007/978-3-319-20615-817" target="_blank" rel="noopener noreferrer" class="text-signal-blue hover:underline">10.1007/978-3-319-20615-817</a></pub-id>
[10] Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. <em>Introduction to algorithms</em>. MIT Press, 3. ed. edition, 2009. ISBN 0-262-53305-7, 978-0-262-53305-8, 978-0-262-03384-8. <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="http://scans.hebis.de/HEBCGI/show.pl?21502893_toc.pdf">http://scans.hebis.de/HEBCGI/show.pl?21502893_toc.pdf</ext-link>.
[17] Konrad Raczkowski and Paweł Sadowski. Equivalence relations and classes of abstraction. <em>Formalized Mathematics</em>, 1(<bold>3</bold>):441–444, 1990.
[19] Bernd S. W. Schröder. <em>Ordered Sets: An Introduction</em>. Birkhäuser Boston, 2003. ISBN 978-1-4612-6591-7. <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://books.google.de/books?id=hg8GCAAAQBAJ">https://books.google.de/books?id=hg8GCAAAQBAJ</ext-link>.
[20] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. <em>Formalized Mathematics</em>, 1(<bold>3</bold>):569–573, 1990.