http://hdl.handle.net/11320/7831 2026-06-01T21:33:54Z http://hdl.handle.net/11320/7843 Tytuł: Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm Autorzy: Okazaki, Hiroyuki; Nagao, Koh-ichi; Futa, Yuichi Abstrakt: In this article we formalize in Mizar [1], [2] the maximum number of steps taken by some number theoretical algorithms, “right–to–left binary algorithm” for modular exponentiation and “Euclidean algorithm” [5]. For any natural numbers a, b, n, “right–to–left binary algorithm” can calculate the natural number, see (Def. 2), AlgoBPow(a, n, m) := ab mod n and for any integers a, b, “Euclidean algorithm” can calculate the non negative integer gcd(a, b). We have not formalized computational complexity of algorithms yet, though we had already formalize the “Euclidean algorithm” in [7].For “right-to-left binary algorithm”, we formalize the theorem, which says that the required number of the modular squares and modular products in this algorithms are ⌊1+log2 n⌋ and for “Euclidean algorithm”, we formalize the Lamé’s theorem [6], which says the required number of the divisions in this algorithm is at most 5 log10 min(|a|, |b|). Our aim is to support the implementation of number theoretic tools and evaluating computational complexities of algorithms to prove the security of cryptographic systems. 2019-01-01T00:00:00Z http://hdl.handle.net/11320/7842 Tytuł: Tarski Geometry Axioms. Part IV – Right Angle Autorzy: Coghetto, Roland; Grabowski, Adam Abstrakt: In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during Tarski Formalization Project by M. Beeson (the so-called Section 8A of SST). 2019-01-01T00:00:00Z http://hdl.handle.net/11320/7840 Tytuł: Continuity of Multilinear Operator on Normed Linear Spaces Autorzy: Nakasho, Kazuhisa; Shidama, Yasunari Abstrakt: In this article, various definitions of contuity of multilinear operators on normed linear spaces are discussed in the Mizar formalism [4], [1] and [2]. In the first chapter, several basic theorems are prepared to handle the norm of the multilinear operator, and then it is formalized that the linear space of bounded multilinear operators is a complete Banach space.In the last chapter, the continuity of the multilinear operator on finite normed spaces is addressed. Especially, it is formalized that the continuity at the origin can be extended to the continuity at every point in its whole domain. We referred to [5], [11], [8], [9] in this formalization. 2019-01-01T00:00:00Z http://hdl.handle.net/11320/7841 Tytuł: Fubini’s Theorem Autorzy: Endou, Noboru Abstrakt: Fubini theorem is an essential tool for the analysis of high-dimensional space [8], [2], [3], a theorem about the multiple integral and iterated integral. The author has been working on formalizing Fubini’s theorem over the past few years [4], [6] in the Mizar system [7], [1]. As a result, Fubini’s theorem (30) was proved in complete form by this article. 2019-01-01T00:00:00Z