Volume 7, Number 1 (1998): pdf, ps, dvi.

- Artur Kornilowicz.
The Composition of Functors and Transformations in Alternative Categories,
Formalized Mathematics 7(1), pages 1-7, 1998. MML Identifier: FUNCTOR3

**Summary**:

- 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}.

- 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}.

- Robert Milewski.
Natural Numbers,
Formalized Mathematics 7(1), pages 19-22, 1998. MML Identifier: NAT_2

**Summary**:

- Robert Milewski.
Binary Arithmetics. Binary Sequences,
Formalized Mathematics 7(1), pages 23-26, 1998. MML Identifier: BINARI_3

**Summary**:

- Robert Milewski.
Full Trees,
Formalized Mathematics 7(1), pages 27-30, 1998. MML Identifier: BINTREE2

**Summary**:

- 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$.

- Grzegorz Bancerek.
Bases and Refinements of Topologies,
Formalized Mathematics 7(1), pages 35-43, 1998. MML Identifier: YELLOW_9

**Summary**:

- 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}.

- 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.

- Jaroslaw Gryko.
Injective Spaces,
Formalized Mathematics 7(1), pages 57-62, 1998. MML Identifier: WAYBEL18

**Summary**:

- Artur Kornilowicz.
On the Characterization of Hausdorff Spaces,
Formalized Mathematics 7(1), pages 63-68, 1998. MML Identifier: YELLOW12

**Summary**:

- 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.

- 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}.

- 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}.

- 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.

- 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}).

- 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.

- 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}.

- 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.

- Artur Kornilowicz.
The Product of the Families of the Groups,
Formalized Mathematics 7(1), pages 127-134, 1998. MML Identifier: GROUP_7

**Summary**:

- 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.

- 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.

- 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.