http://hdl.handle.net/11320/3661 2026-06-01T18:28:58Z http://hdl.handle.net/11320/3682 Tytuł: Constructing Binary Huffman Tree Autorzy: Okazaki, Hiroyuki; Futa, Yuichi; Shidama, Yasunari Abstrakt: Huffman coding is one of a most famous entropy encoding methods for lossless data compression [16]. JPEG and ZIP formats employ variants of Huffman encoding as lossless compression algorithms. Huffman coding is a bijective map from source letters into leaves of the Huffman tree constructed by the algorithm. In this article we formalize an algorithm constructing a binary code tree, Huffman tree. Opis: This research was presented during the 2013 International Conference on Foundations of Computer Science FCS’13 in Las Vegas, USA. 2013-01-01T00:00:00Z http://hdl.handle.net/11320/3683 Tytuł: Riemann Integral of Functions from R into Real Banach Space Autorzy: Narita, Keiko; Endou, Noboru; Shidama, Yasunari Abstrakt: In this article we deal with the Riemann integral of functions from R into a real Banach space. The last theorem establishes the integrability of continuous functions on the closed interval of reals. To prove the integrability we defined uniform continuity for functions from R into a real normed space, and proved related theorems. We also stated some properties of finite sequences of elements of a real normed space and finite sequences of real numbers. In addition we proved some theorems about the convergence of sequences. We applied definitions introduced in the previous article [21] to the proof of integrability. 2013-01-01T00:00:00Z http://hdl.handle.net/11320/3681 Tytuł: Commutativeness of Fundamental Groups of Topological Groups Autorzy: Korniłowicz, Artur Abstrakt: In this article we prove that fundamental groups based at the unit point of topological groups are commutative [11]. 2013-01-01T00:00:00Z http://hdl.handle.net/11320/3684 Tytuł: On Square-Free Numbers Autorzy: Grabowski, Adam Abstrakt: In the article the formal characterization of square-free numbers is shown; in this manner the paper is the continuation of [19]. Essentially, we prepared some lemmas for convenient work with numbers (including the proof that the sequence of prime reciprocals diverges [1]) according to [18] which were absent in the Mizar Mathematical Library. Some of them were expressed in terms of clusters’ registrations, enabling automatization machinery available in the Mizar system. Our main result of the article is in the final section; we proved that the lattice of positive divisors of a positive integer n is Boolean if and only if n is square-free. 2013-01-01T00:00:00Z