http://hdl.handle.net/11320/3584 2026-06-01T07:20:24Z http://hdl.handle.net/11320/3641 Tytuł: Introduction to Rational Functions Autorzy: Schwarzweller, Christoph Abstrakt: In this article we formalize rational functions as pairs of polynomials and define some basic notions including the degree and evaluation of rational functions [8]. The main goal of the article is to provide properties of rational functions necessary to prove a theorem on the stability of networks. 2012-01-01T00:00:00Z http://hdl.handle.net/11320/3640 Tytuł: Extended Euclidean Algorithm and CRT Algorithm Autorzy: Okazaki, Hiroyuki; Aoki, Yosiki; Shidama, Yasunari Abstrakt: In this article we formalize some number theoretical algorithms, Euclidean Algorithm and Extended Euclidean Algorithm [9]. Besides the a gcd b, Extended Euclidean Algorithm can calculate a pair of two integers (x, y) that holds ax + by = a gcd b. In addition, we formalize an algorithm that can compute a solution of the Chinese remainder theorem by using Extended Euclidean Algorithm. Our aim is to support the implementation of number theoretic tools. Our formalization of those algorithms is based on the source code of the NZMATH, a number theory oriented calculation system developed by Tokyo Metropolitan University [8]. 2012-01-01T00:00:00Z http://hdl.handle.net/11320/3636 Tytuł: Formalization of the Data Encryption Standard Autorzy: Okazaki, Hiroyuki; Shidama, Yasunari Abstrakt: In this article we formalize DES (the Data Encryption Standard), that was the most widely used symmetric cryptosystem in the world. DES is a block cipher which was selected by the National Bureau of Standards as an official Federal Information Processing Standard for the United States in 1976 [15]. 2012-01-01T00:00:00Z http://hdl.handle.net/11320/3635 Tytuł: Higher-Order Partial Differentiation Autorzy: Endou, Noboru; Okazaki, Hiroyuki; Shidama, Yasunari Abstrakt: In this article, we shall extend the formalization of [10] to discuss higher-order partial differentiation of real valued functions. The linearity of this operator is also proved (refer to [10], [12] and [13] for partial differentiation). 2012-01-01T00:00:00Z