Concatenation of Finite Sequences

[1] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.Search in Google Scholar

[2] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6. Concatenation of finite sequences 1310.1007/s10817-017-9440-6.13Open DOISearch in Google Scholar

[3] Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.10.1007/s10817-015-9345-1Open DOISearch in Google Scholar

[4] Artur Kornilowicz. How to define terms in Mizar effectively. Studies in Logic, Grammar and Rhetoric, 18:67–77, 2009.Search in Google Scholar

[5] Piotr Rudnicki and Andrzej Trybulec. On the integrity of a repository of formalized mathematics. In Andrea Asperti, Bruno Buchberger, and James H. Davenport, editors, Mathematical Knowledge Management, volume 2594 of Lecture Notes in Computer Science, pages 162–174. Springer, Berlin, Heidelberg, 2003. doi:10.1007/3-540-36469-2_13.10.1007/3-540-36469-2_13Open DOISearch in Google Scholar

[6] Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825–829, 2001.Search in Google Scholar

[7] Rafał Ziobro. Fermat’s Little Theorem via divisibility of Newton’s binomial. Formalized Mathematics, 23(3):215–229, 2015. doi:10.1515/forma-2015-0018.10.1515/forma-2015-0018Open DOISearch in Google Scholar

[8] Rafał Ziobro. On subnomials. Formalized Mathematics, 24(4):261–273, 2016. doi:10.1515/forma-2016-0022.10.1515/forma-2016-0022Search in Google Scholar