VOLUME 12, NUMBER 1 (2004), Formalized Mathematics, ISSN 1898-9934 (Online), ISSN 1426-2630 (Print)

Formalized Mathematics (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 12, Number 1 (2004): pdf.

Yatsuka Nakamura. Sorting Operators for Finite Sequences, Formalized Mathematics 12(1), pages 1-4, 2004. MML Identifier: RFINSEQ2
Summary: Two kinds of sorting operators, descendent one and ascendent one are introduced for finite sequences of reals. They are also called rearrangement of finite sequences of reals. Maximum and minimum values of finite sequences of reals are also defined. We also discuss relations between these concepts.
Masaaki Niimura, Yasushi Fuwa. Magnitude Relation Properties of Radix-$2^k$ SD Number, Formalized Mathematics 12(1), pages 5-8, 2004. MML Identifier: RADIX_5
Summary: In this article, magnitude relation properties of Radix-$2^k$ SD number are discussed. Until now, the Radix-$2^k$ SD Number has been proposed for the high-speed calculations for RSA Cryptograms. In RSA Cryptograms, many modulo calculations are used, and modulo calculations need a comparison between two numbers.\par In this article, we discuss magnitude relation of Radix-$2^k$ SD Number. In the first section, we present some useful theorems for operations of Radix-$2^k$ SD Number. In the second section, we prove some properties of the primary numbers expressed by Radix-$2^k$ SD Number such as 0, 1, and Radix(k). In the third section, we prove primary magnitude relations between two Radix-$2^k$ SD Numbers. In the fourth section, we define Max/Min numbers in some cases. And in the last section, we prove some relations between the addition of Max/Min numbers.
Masaaki Niimura, Yasushi Fuwa. High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number, Formalized Mathematics 12(1), pages 9-13, 2004. MML Identifier: RADIX_6
Summary: In RSA Cryptograms, many modulo calculations are used, but modulo calculation is based on many subtractions and it takes long a time to calculate it. In this article, we explain a new modulo calculation algorithm using a table. And we prove that upper 3 digits of Radix-$2^k$ SD numbers are enough to specify the answer. \par In the first section, we present some useful theorems for operations of Radix-$2^k$ SD Number. In the second section, we define Upper 3 Digits of Radix-$2^k$ SD number and prove that property. In the third section, we prove some property connected with the minimum digits of Radix-$2^k$ SD number. In the fourth section, we identify the range of modulo arithmetic result and prove that the Upper 3 Digits indicate two possible answers. And in the last section, we define a function to select true answer from the results of Upper 3 Digits.
Takashi Mitsuishi, Grzegorz Bancerek. Transitive Closure of Fuzzy Relations, Formalized Mathematics 12(1), pages 15-20, 2004. MML Identifier: LFUZZY_1
Summary:
Adam Grabowski. Basic Properties of Rough Sets and Rough Membership Function, Formalized Mathematics 12(1), pages 21-28, 2004. MML Identifier: ROUGHS_1
Summary: We present basic concepts concerning rough set theory. We define tolerance and approximation spaces and rough membership function. Different rough inclusions as well as the predicate of rough equality of sets are also introduced.
Yatsuka Nakamura. Correctness of Non Overwriting Programs. Part I, Formalized Mathematics 12(1), pages 29-32, 2004. MML Identifier: PRGCOR_1
Summary: Non overwriting program is a program where each variable used in it is written only just one time, but the control variables used for ``for-statement'' are exceptional. Contrarily, variables are allowed to be read many times. There are other restrictions for the non overwriting program. For statements, only the following are allowed: ``substituting-statement'', ``if-else-statement'', ``for-statement'' (with break and without break), function (correct one) -- ``call-statement'' and ``return-statement''. Grammar of non overwriting program is like the one of the C-language. For type of variables, ``int'', ``real", ``char'' and ``float'' can be used, and array of them can also be used. For operation, ``+'', ``$-$'' and ``*'' are used for a type ``int''; ``+'', ``$-$'', ``*'' and ``/'' are used for a type ``float''. User can also define structures like in C. Non overwriting program can be translated to (predicative) logic formula in definition part to define functions. If a new function is correctly defined, a corresponding program is correct, if it does not use arrays. If it uses arrays, area check is necessary in the following theorem.\par Semantic correctness is shown by some theorems following the definition. These theorems must tie up the result of the program and mathematical concepts introduced before. Correctness is proven {\it function-wise}. We must use only {\it correctness-proven} functions to define a new function (to write a new program as a form of a function). Here, we present two programs of division function of two natural numbers and of two integers. An algorithm is checked for each case by proving correctness of the definitions. We also perform an area check of the index of arrays used in one of the programs.
Artur Kornilowicz. A Tree of Execution of a Macroinstruction, Formalized Mathematics 12(1), pages 33-37, 2004. MML Identifier: AMISTD_3
Summary: A tree of execution of a macroinstruction is defined. It is a tree decorated by the instruction locations of a computer. Successors of each vertex are determined by the set of all possible values of the instruction counter after execution of the instruction placed in the location indicated by given vertex.
Yasunari Shidama. Banach Space of Bounded Linear Operators, Formalized Mathematics 12(1), pages 39-48, 2004. MML Identifier: LOPBAN_1
Summary: In this article, the basic properties of linear spaces which are defined as the set of all linear operators from one linear space to another, are described. Especially, the Banach space is introduced. This is defined by the set of all bounded linear operators.
Piotr Rudnicki. Little Bezout Theorem (Factor Theorem), Formalized Mathematics 12(1), pages 49-58, 2004. MML Identifier: UPROOTS
Summary: We present a formalization of the factor theorem for univariate polynomials, also called the (little) Bezout theorem: Let $r$ belong to a commutative ring $L$ and $p(x)$ be a polynomial over $L$. Then $x-r$ divides $p(x)$ iff $p(r) = 0$. We also prove some consequences of this theorem like that any non zero polynomial of degree $n$ over an algebraically closed integral domain has $n$ (non necessarily distinct) roots.
Broderick Arneson, Piotr Rudnicki. Primitive Roots of Unity and Cyclotomic Polynomials, Formalized Mathematics 12(1), pages 59-67, 2004. MML Identifier: UNIROOTS
Summary: We present a formalization of roots of unity, define cyclotomic polynomials and demonstrate the relationship between cyclotomic polynomials and unital polynomials.
Broderick Arneson, Matthias Baaz, Piotr Rudnicki. Witt's Proof of the Wedderburn Theorem, Formalized Mathematics 12(1), pages 69-75, 2004. MML Identifier: WEDDWITT
Summary: We present a formalization of Witt's proof of the Wedderburn theorem following Chapter 5 of {\em Proofs from THE BOOK} by Martin Aigner and G\"{u}nter M. Ziegler, 2nd ed., Springer 1999.