Formalized Mathematics    (ISSN 1426-2630)
Volume 7, Number 1 (1998): pdf, ps, dvi.
  1. Artur Kornilowicz. The Composition of Functors and Transformations in Alternative Categories, Formalized Mathematics 7(1), pages 1-7, 1998. MML Identifier: FUNCTOR3
    Summary:
  2. Robert Milewski. Completely-Irreducible Elements, Formalized Mathematics 7(1), pages 9-12, 1998. MML Identifier: WAYBEL16
    Summary: The article is a translation of \cite[92--93]{CCL}.
  3. Adam Grabowski. Scott-Continuous Functions, Formalized Mathematics 7(1), pages 13-18, 1998. MML Identifier: WAYBEL17
    Summary: The article is a translation of \cite[pp. 112--113]{CCL}.
  4. Robert Milewski. Natural Numbers, Formalized Mathematics 7(1), pages 19-22, 1998. MML Identifier: NAT_2
    Summary:
  5. Robert Milewski. Binary Arithmetics. Binary Sequences, Formalized Mathematics 7(1), pages 23-26, 1998. MML Identifier: BINARI_3
    Summary:
  6. Robert Milewski. Full Trees, Formalized Mathematics 7(1), pages 27-30, 1998. MML Identifier: BINTREE2
    Summary:
  7. Adam Naumowicz, Mariusz Lapinski. On \Tone\ Reflex of Topological Space, Formalized Mathematics 7(1), pages 31-34, 1998. MML Identifier: T_1TOPSP
    Summary: This article contains a definition of $T_{1}$ reflex of a topological space as a quotient space which is $T_{1}$ and fulfils the condition that every continuous map $f$ from a topological space $T$ into $S$ being $T_{1}$ space can be considered as a superposition of two continuous maps: the first from $T$ onto its $T_{1}$ reflex and the last from $T_{1}$ reflex of $T$ into $S$.
  8. Grzegorz Bancerek. Bases and Refinements of Topologies, Formalized Mathematics 7(1), pages 35-43, 1998. MML Identifier: YELLOW_9
    Summary:
  9. Artur Kornilowicz. The Properties of Product of Relational Structures, Formalized Mathematics 7(1), pages 45-52, 1998. MML Identifier: YELLOW10
    Summary: This work contains useful facts about the product of relational structures. It continues the formalization of \cite{CCL}.
  10. Adam Naumowicz. On the Characterization of Modular and Distributive Lattices, Formalized Mathematics 7(1), pages 53-55, 1998. MML Identifier: YELLOW11
    Summary: This article contains definitions of the ``pentagon'' lattice $N_5$ and the ``diamond'' lattice $M_3$. It is followed by the characterization of modular and distributive lattices depending on the possible shape of substructures. The last part treats of interval-like sublattices of any lattice.
  11. Jaroslaw Gryko. Injective Spaces, Formalized Mathematics 7(1), pages 57-62, 1998. MML Identifier: WAYBEL18
    Summary:
  12. Artur Kornilowicz. On the Characterization of Hausdorff Spaces, Formalized Mathematics 7(1), pages 63-68, 1998. MML Identifier: YELLOW12
    Summary:
  13. Christoph Schwarzweller. The Field of Quotients Over an Integral Domain, Formalized Mathematics 7(1), pages 69-79, 1998. MML Identifier: QUOFIELD
    Summary: We introduce the field of quotients over an integral domain following the well-known construction using pairs over integral domains. In addition we define ring homomorphisms and prove some basic facts about fields of quotients including their universal property.
  14. Bartlomiej Skorulski. First-countable, Sequential, and Frechet Spaces, Formalized Mathematics 7(1), pages 81-86, 1998. MML Identifier: FRECHET
    Summary: This article contains a definition of three classes of topological spaces: first-countable, Frechet, and sequential. Next there are some facts about them, that every first-countable space is Frechet and every Frechet space is sequential. Next section contains a formalized construction of topological space which is Frechet but not first-countable. This article is based on \cite[pp. 73--81]{ENGEL:1}.
  15. Piotr Rudnicki. On the Composition of Non-parahalting Macro Instructions, Formalized Mathematics 7(1), pages 87-92, 1998. MML Identifier: SFMASTR1
    Summary: An attempt to use the {\tt Times} macro, \cite{SCMFSA8C.ABS}, was the origin of writing this article. First, the semantics of the macro composition as developed in \cite{SCMFSA6A.ABS}, \cite{SCMFSA6B.ABS}, \cite{SCMFSA6C.ABS} is extended to the case of macro instructions which are not always halting. Next, several functors extending the memory handling for {\SCMFSA}, \cite{SF_MASTR.ABS}, are defined; they are convenient when writing more complicated programs. After this preparatory work, we define a macro instruction computing the Fibonacci sequence (see the SCM program computing the same sequence in \cite{FIB_FUSC.ABS}) and prove its correctness. The semantics of the {\tt Times} macro is given in \cite{SCMFSA8C.ABS} only for the case when the iterated instruction is parahalting; this is remedied in \cite{SFMASTR2.ABS}.
  16. Piotr Rudnicki. The while Macro Instructions of \SCMFSA. Part II, Formalized Mathematics 7(1), pages 93-100, 1998. MML Identifier: SCMFSA9A
    Summary: An attempt to use the {\tt while} macro, \cite{SCMFSA_9.ABS}, was the origin of writing this article. The {\tt while} semantics, as given by J.-C.~Chen, is slightly extended by weakening its correctness conditions and this forced a quite straightforward remake of a number of theorems from \cite{SCMFSA_9.ABS}. Numerous additional properties of the {\tt while} macro are then proven. In the last section, we define a macro instruction computing the {\tt fusc} function (see the SCM program computing the same function in \cite{FIB_FUSC.ABS}) and prove its correctness.
  17. Piotr Rudnicki. Another times Macro Instruction, Formalized Mathematics 7(1), pages 101-105, 1998. MML Identifier: SFMASTR2
    Summary: The semantics of the {\tt times} macro is given in \cite{SCMFSA8C.ABS} only for the case when the body of the macro is parahalting. We remedy this by defining a new {\tt times} macro instruction in terms of {\tt while} (see \cite{SCMFSA_9.ABS}, \cite{SCMFSA9A.ABS}). The semantics of the new {\tt times} macro is given in a way analogous to the semantics of {\tt while} macros. The new {\tt times} uses an anonymous variable to control the number of its executions. We present two examples: a trivial one and a remake of the macro for the Fibonacci sequence (see \cite{SFMASTR1.ABS}).
  18. Piotr Rudnicki. The for (going up) Macro Instruction, Formalized Mathematics 7(1), pages 107-114, 1998. MML Identifier: SFMASTR3
    Summary: We define a {\tt for} type (going up) macro instruction in terms of the {\tt while} macro. This gives an iterative macro with an explicit control variable. The {\tt for} macro is used to define a macro for the selection sort acting on a finite sequence location of {\SCMFSA}. On the way, a macro for finding a minimum in a section of an array is defined.
  19. Yatsuka Nakamura, Adam Grabowski. Bounding Boxes for Special Sequences in $\calE^2$, Formalized Mathematics 7(1), pages 115-121, 1998. MML Identifier: JORDAN5D
    Summary: This is the continuation of the proof of the Jordan Theorem according to \cite{TAKE-NAKA}.
  20. Yoshinori Fujisawa, Yasushi Fuwa, Hidetaka Shimizu. Euler's Theorem and Small Fermat's Theorem, Formalized Mathematics 7(1), pages 123-126, 1998. MML Identifier: EULER_2
    Summary: This article is concerned with Euler's theorem and small Fermat's theorem that play important roles in public-key cryptograms. In the first section, we present some selected theorems on integers. In the following section, we remake definitions about the finite sequence of natural, the function of natural times finite sequence of natural and $\pi$ of the finite sequence of natural. We also prove some basic theorems that concern these redefinitions. Next, we define the function of modulus for finite sequence of natural and some fundamental theorems about this function are proved. Finally, Euler's theorem and small Fermat's theorem are proved.
  21. Artur Kornilowicz. The Product of the Families of the Groups, Formalized Mathematics 7(1), pages 127-134, 1998. MML Identifier: GROUP_7
    Summary:
  22. Yatsuka Nakamura. On the Dividing Function of the Simple Closed Curve into Segments, Formalized Mathematics 7(1), pages 135-138, 1998. MML Identifier: JORDAN7
    Summary: At the beginning, the concept of the segment of the simple closed curve in 2-dimensional Euclidean space is defined. Some properties of segments are shown in the succeeding theorems. At the end, the existence of the function which can divide the simple closed curve into segments is shown. We can make the diameter of segments as small as we want.
  23. Jing-Chao Chen, Yatsuka Nakamura. Initialization Halting Concepts and Their Basic Properties of \SCMFSA, Formalized Mathematics 7(1), pages 139-151, 1998. MML Identifier: SCM_HALT
    Summary: Up to now, many properties of macro instructions of {\SCMFSA} are described by the parahalting concepts. However, many practical programs are not always halting while they are halting for initialization states. For this reason, we propose initialization halting concepts. That a program is initialization halting (called ``InitHalting'' for short) means it is halting for initialization states. In order to make the halting proof of more complicated programs easy, we present ``InitHalting'' basic properties of the compositions of the macro instructions, if-Macro (conditional branch macro instructions) and Times-Macro (for-loop macro instructions) etc.
  24. Jing-Chao Chen, Yatsuka Nakamura. Bubble Sort on \SCMFSA, Formalized Mathematics 7(1), pages 153-161, 1998. MML Identifier: SCMBSORT
    Summary: We present the bubble sorting algorithm using macro instructions such as the if-Macro (conditional branch macro instructions) and the Times-Macro (for-loop macro instructions) etc. The correctness proof of the program should include the proof of autonomic, halting and the correctness of the program result. In the three terms, we justify rigorously the correctness of the bubble sorting algorithm. In order to prove it is autonomic, we use the following theorem: if all variables used by the program are initialized, it is autonomic. This justification method probably reveals that autonomic concept is not important.