Formalized Mathematics    (ISSN 1426-2630)
Volume 9, Number 1 (2001): pdf, ps, dvi.
  1. Jing-Chao Chen. Recursive Euclide Algorithm, Formalized Mathematics 9(1), pages 1-4, 2001. MML Identifier: SCMP_GCD
    Summary: The earlier SCM computer did not contain recursive function, so Trybulec and Nakamura proved the correctness of the Euclid's algorithm only by way of an iterative program. However, the recursive method is a very important programming method, furthermore, for some algorithms, for example Quicksort, only by employing a recursive method (note push-down stack is essentially also a recursive method) can they be implemented. The main goal of the article is to test the recursive function of the SCMPDS computer by proving the correctness of the Euclid's algorithm by way of a recursive program. In this article, we observed that the memory required by the recursive Euclide algorithm is variable but it is still autonomic. Although the algorithm here is more complicated than the non-recursive algorithm, its focus is that the SCMPDS computer will be able to implement many algorithms like Quicksort which the SCM computer cannot do.
  2. Adam Grabowski. Scott-Continuous Functions. Part II, Formalized Mathematics 9(1), pages 5-11, 2001. MML Identifier: WAYBEL24
    Summary:
  3. Jaroslaw Gryko, Artur Kornilowicz. Some Properties of Isomorphism between Relational Structures. On the Product of Topological Spaces, Formalized Mathematics 9(1), pages 13-18, 2001. MML Identifier: YELLOW14
    Summary:
  4. Czeslaw Bylinski, Mariusz Zynel. Cages -- the External Approximation of Jordan's Curve, Formalized Mathematics 9(1), pages 19-24, 2001. MML Identifier: JORDAN9
    Summary: On the Euclidean plane Jordan's curve may be approximated with a polygonal path of sides parallel to coordinate axes, either externally, or internally. The paper deals with the external approximation, and the existence of a {\em Cage} -- an external polygonal path -- is proved.
  5. Robert Milewski. Components and Basis of Topological Spaces, Formalized Mathematics 9(1), pages 25-29, 2001. MML Identifier: YELLOW15
    Summary: This article contains many facts about components and basis of topological spaces.
  6. Artur Kornilowicz. Properties of the External Approximation of Jordan's Curve, Formalized Mathematics 9(1), pages 31-34, 2001. MML Identifier: JORDAN10
    Summary:
  7. Freek Wiedijk. Irrationality of $e$, Formalized Mathematics 9(1), pages 35-39, 2001. MML Identifier: IRRAT_1
    Summary: We prove the irrationality of square roots of prime numbers and of the number $e$. In order to be able to prove the last, a proof is given that {\tt number\_e = exp(1)} as defined in the Mizar library, that is that $$\lim_{n\rightarrow\infty} (1+{1\over n})^n = \sum_{k=0}^\infty {1\over k!}$$
  8. Artur Kornilowicz, Jaroslaw Gryko. Injective Spaces. Part II, Formalized Mathematics 9(1), pages 41-47, 2001. MML Identifier: WAYBEL25
    Summary:
  9. Shunichi Kobayashi. Propositional Calculus for Boolean Valued Functions. Part VI, Formalized Mathematics 9(1), pages 49-50, 2001. MML Identifier: BVFUNC10
    Summary: In this paper, we proved some elementary propositional calculus formulae for Boolean valued functions.
  10. Shunichi Kobayashi, Yatsuka Nakamura. Predicate Calculus for Boolean Valued Functions. Part III, Formalized Mathematics 9(1), pages 51-53, 2001. MML Identifier: BVFUNC11
    Summary: In this paper, we proved some elementary predicate calculus formulae containing the quantifiers of Boolean valued functions with respect to partitions. Such a theory is an analogy of usual predicate logic.
  11. Christoph Schwarzweller. A Characterization of Concept Lattices. Dual Concept Lattices, Formalized Mathematics 9(1), pages 55-59, 2001. MML Identifier: CONLAT_2
    Summary: In this article we continue the formalization of concept lattices following \cite{GanterWille}. We give necessary and sufficient conditions for a complete lattice to be isomorphic to a given formal context. As a by-product we get that a lattice is complete if and only if it is isomorphic to a concept lattice. In addition we introduce dual formal concepts and dual concept lattices and prove that the dual of a concept lattice over a formal context is isomorphic to the concept lattice over the dual formal context.
  12. Shunichi Kobayashi, Yatsuka Nakamura. Predicate Calculus for Boolean Valued Functions. Part IV, Formalized Mathematics 9(1), pages 61-63, 2001. MML Identifier: BVFUNC12
    Summary:
  13. Shunichi Kobayashi, Yatsuka Nakamura. Predicate Calculus for Boolean Valued Functions. Part V, Formalized Mathematics 9(1), pages 65-70, 2001. MML Identifier: BVFUNC13
    Summary: In this paper, we proved some elementary predicate calculus formulae containing the quantifiers of Boolean valued functions with respect to partitions. Such a theory is an analogy of usual predicate logic.
  14. Yoshinori Fujisawa, Yasushi Fuwa. Definitions of Radix-$2^k$ Signed-Digit Number and its Adder Algorithm, Formalized Mathematics 9(1), pages 71-75, 2001. MML Identifier: RADIX_1
    Summary: In this article, a radix-$2^k$ signed-digit number (Radix-$2^k$ SD number) is defined and based on it a high-speed adder algorithm is discussed. \par The processes of coding and encoding for public-key cryptograms require a great deal of addition operations of natural number of many figures. This results in a~long time for the encoding and decoding processes. It is possible to reduce the processing time using the high-speed adder algorithm.\par In the first section of this article, we prepared some useful theorems for natural numbers and integers. In the second section, we defined the concept of radix-$2^k$, a set named $k$-SD and proved some properties about them. In the third section, we provide some important functions for generating Radix-$2^k$ SD numbers from natural numbers and natural numbers from Radix-$2^k$ SD numbers. In the fourth section, we defined the carry and data components of addition with Radix-$2^k$ SD numbers and some properties about them. In the fifth section, we defined a theorem for checking whether or not a natural number can be expressed as $n$ digits Radix-$2^k$ SD number. \par In the last section, a high-speed adder algorithm on Radix-$2^k$ SD numbers is proposed and we provided some properties. In this algorithm, the carry of each digit has an effect on only the next digit. Properties of the relationships of the results of this algorithm to the operations of natural numbers are also given.
  15. Grzegorz Bancerek. Retracts and Inheritance, Formalized Mathematics 9(1), pages 77-85, 2001. MML Identifier: YELLOW16
    Summary:
  16. Grzegorz Bancerek. Technical Preliminaries to Algebraic Specifications, Formalized Mathematics 9(1), pages 87-93, 2001. MML Identifier: ALGSPEC1
    Summary:
  17. Piotr Rudnicki, Andrzej Trybulec. Multivariate Polynomials with Arbitrary Number of Variables, Formalized Mathematics 9(1), pages 95-110, 2001. MML Identifier: POLYNOM1
    Summary: The goal of this article is to define multivariate polynomials in arbitrary number of indeterminates and then to prove that they constitute a ring (over appropriate structure of coefficients).\par The introductory section includes quite a number of auxiliary lemmas related to many different parts of the MML. The second section characterizes the sequence flattening operation, introduced in \cite{DTCONSTR.ABS}, but so far lacking theorems about its fundamental properties.\par We first define formal power series in arbitrary number of variables. The auxiliary concept on which the construction of formal power series is based is the notion of a bag. A bag of a set $X$ is a natural function on $X$ which is zero almost everywhere. The elements of $X$ play the role of formal variables and a bag gives their exponents thus forming a power product. Series are defined for an ordered set of variables (we use ordinal numbers). A series in $o$ variables over a structure $S$ is a function assigning an element of the carrier of $S$ (coefficient) to each bag of $o$.\par We define the operations of addition, complement and multiplication for formal power series and prove their properties which depend on assumed properties of the structure from which the coefficients are taken. (We would like to note that proving associativity of multiplication turned out to be technically complicated.)\par Polynomial is defined as a formal power series with finite number of non zero coefficients. In conclusion, the ring of polynomials is defined.
  18. Grzegorz Bancerek. Continuous Lattices of Maps between T$_0$ Spaces, Formalized Mathematics 9(1), pages 111-117, 2001. MML Identifier: WAYBEL26
    Summary: Formalization of \cite[pp. 128--130]{CCL}, chapter II, section 4 (4.1 -- 4.9).
  19. Shunichi Kobayashi. Predicate Calculus for Boolean Valued Functions. Part VI, Formalized Mathematics 9(1), pages 119-121, 2001. MML Identifier: BVFUNC14
    Summary: In this paper, we proved some elementary predicate calculus formulae containing the quantifiers of Boolean valued functions with respect to partitions. Such a theory is an analogy of usual predicate logic.
  20. Shunichi Kobayashi. Predicate Calculus for Boolean Valued Functions. Part VII, Formalized Mathematics 9(1), pages 123-125, 2001. MML Identifier: BVFUNC15
    Summary:
  21. Shunichi Kobayashi. Predicate Calculus for Boolean Valued Functions. Part VIII, Formalized Mathematics 9(1), pages 127-129, 2001. MML Identifier: BVFUNC16
    Summary:
  22. Shunichi Kobayashi. Predicate Calculus for Boolean Valued Functions. Part IX, Formalized Mathematics 9(1), pages 131-133, 2001. MML Identifier: BVFUNC17
    Summary:
  23. Richard Krueger, Piotr Rudnicki, Paul Shelley. Asymptotic Notation. Part I: Theory, Formalized Mathematics 9(1), pages 135-142, 2001. MML Identifier: ASYMPT_0
    Summary: The widely used textbook by Brassard and Bratley \cite{BraBra96} includes a chapter devoted to asymptotic notation (Chapter 3, pp. 79--97). We have attempted to test how suitable the current version of Mizar is for recording this type of material in its entirety. A more detailed report on this experiment will be available separately. This article presents the development of notions and a follow-up article \cite{ASYMPT_1.ABS} includes examples and solutions to problems. The preliminaries introduce a number of properties of real sequences, some operations on real sequences, and a characterization of convergence. The remaining sections in this article correspond to sections of Chapter 3 of \cite{BraBra96}. Section 2 defines the $O$ notation and proves the threshold, maximum, and limit rules. Section 3 introduces the $\Omega$ and $\Theta$ notations and their analogous rules. Conditional asymptotic notation is defined in Section 4 where smooth functions are also discussed. Section 5 defines some operations on asymptotic notation (we have decided not to introduce the asymptotic notation for functions of several variables as it is a straightforward generalization of notions for unary functions).
  24. Richard Krueger, Piotr Rudnicki, Paul Shelley. Asymptotic Notation. Part II: Examples and Problems, Formalized Mathematics 9(1), pages 143-154, 2001. MML Identifier: ASYMPT_1
    Summary: The widely used textbook by Brassard and Bratley \cite{BraBra96} includes a chapter devoted to asymptotic notation (Chapter 3, pp. 79--97). We have attempted to test how suitable the current version of Mizar is for recording this type of material in its entirety. This article is a follow-up to \cite{ASYMPT_0.ABS} in which we introduced the basic notions and general theory. This article presents a Mizar formalization of examples and solutions to problems from Chapter 3 of \cite{BraBra96} (some of the examples and solved problems are also in \cite{ASYMPT_0.ABS}). Not all problems have been solved as some required solutions not amenable for formalization.
  25. Shunichi Kobayashi. Predicate Calculus for Boolean Valued Functions. Part X, Formalized Mathematics 9(1), pages 155-156, 2001. MML Identifier: BVFUNC18
    Summary:
  26. Shunichi Kobayashi. Predicate Calculus for Boolean Valued Functions. Part XI, Formalized Mathematics 9(1), pages 157-159, 2001. MML Identifier: BVFUNC19
    Summary:
  27. Shunichi Kobayashi. Four Variable Predicate Calculus for Boolean Valued Functions. Part I, Formalized Mathematics 9(1), pages 161-165, 2001. MML Identifier: BVFUNC20
    Summary:
  28. Shunichi Kobayashi. Four Variable Predicate Calculus for Boolean Valued Functions. Part II, Formalized Mathematics 9(1), pages 167-170, 2001. MML Identifier: BVFUNC21
    Summary:
  29. Grzegorz Bancerek, Adam Naumowicz. Function Spaces in the Category of Directed Suprema Preserving Maps, Formalized Mathematics 9(1), pages 171-177, 2001. MML Identifier: WAYBEL27
    Summary: Formalization of \cite[pp. 115--117]{ccl}, chapter II, section 2 (2.5 -- 2.10).
  30. Takashi Mitsuishi, Katsumi Wasaki, Yasunari Shidama. Property of Complex Functions, Formalized Mathematics 9(1), pages 179-184, 2001. MML Identifier: CFUNCT_1
    Summary: This article introduces properties of complex function, calculations of them, boundedness and constant.
  31. Takashi Mitsuishi, Katsumi Wasaki, Yasunari Shidama. Property of Complex Sequence and Continuity of Complex Function, Formalized Mathematics 9(1), pages 185-190, 2001. MML Identifier: CFCONT_1
    Summary: This article introduces properties of complex sequence and continuity of complex function. The first section shows convergence of complex sequence and constant complex sequence. In the next section, definition of continuity of complex function and properties of continuous complex function are shown.
  32. Noboru Endou, Katsumi Wasaki, Yasunari Shidama. Scalar Multiple of Riemann Definite Integral, Formalized Mathematics 9(1), pages 191-196, 2001. MML Identifier: INTEGRA2
    Summary: The goal of this article is to prove a scalar multiplicity of Riemann definite integral. Therefore, we defined a scalar product to the subset of real space, and we proved some relating lemmas. At last, we proved a scalar multiplicity of Riemann definite integral. As a result, a linearity of Riemann definite integral was proven by unifying the previous article \cite{INTEGRA1.ABS}.
  33. Noboru Endou, Katsumi Wasaki, Yasunari Shidama. Darboux's Theorem, Formalized Mathematics 9(1), pages 197-200, 2001. MML Identifier: INTEGRA3
    Summary: In this article, we have proved the Darboux's theorem. This theorem is important to prove the Riemann integrability. We can replace an upper bound and a lower bound of a function which is the definition of Riemann integration with convergence of sequence by Darboux's theorem.
  34. Shunichi Kobayashi. Five Variable Predicate Calculus for Boolean Valued Functions. Part I, Formalized Mathematics 9(1), pages 201-204, 2001. MML Identifier: BVFUNC22
    Summary:
  35. Shunichi Kobayashi. Six Variable Predicate Calculus for Boolean Valued Functions. Part I, Formalized Mathematics 9(1), pages 205-208, 2001. MML Identifier: BVFUNC23
    Summary:
  36. Jing-Chao Chen, Piotr Rudnicki. The Construction and Computation of for-loop Programs for SCMPDS, Formalized Mathematics 9(1), pages 209-219, 2001. MML Identifier: SCMPDS_7
    Summary: This article defines two for-loop statements for SCMPDS. One is called for-up, which corresponds to ``for (i=x; i$<$0; i+=n) S'' in C language. Another is called for-down, which corresponds to ``for (i=x; i$>$0; i-=n) S''. Here, we do not present their unconditional halting (called parahalting) property, because we have not found that there exists a useful for-loop statement with unconditional halting, and the proof of unconditional halting is much simpler than that of conditional halting. It is hard to formalize all halting conditions, but some cases can be formalized. We choose loop invariants as halting conditions to prove halting problem of for-up/down statements. When some variables (except the loop control variable) keep undestroyed on a set for the loop invariant, and the loop body is halting for this condition, the corresponding for-up/down is halting and computable under this condition. The computation of for-loop statements can be realized by evaluating its body. At the end of the article, we verify for-down statements by two examples for summing.
  37. Shunichi Kobayashi. Predicate Calculus for Boolean Valued Functions. Part XII, Formalized Mathematics 9(1), pages 221-235, 2001. MML Identifier: BVFUNC24
    Summary: In this paper, we proved some elementary predicate calculus formulae containing the quantifiers of Boolean valued functions with respect to partitions. Such a theory is an analogy of ordinary predicate logic.