VOLUME 9, NUMBER 4 (2001), Formalized Mathematics, ISSN 1426-2630

Formalized Mathematics (ISSN 1426-2630)
Volume 9, Number 4 (2001): pdf, ps, dvi.

Artur Kornilowicz. On the Instructions of \SCM, Formalized Mathematics 9(4), pages 659-663, 2001. MML Identifier: AMI_6
Summary:
Artur Kornilowicz. Input and Output of Instructions, Formalized Mathematics 9(4), pages 665-671, 2001. MML Identifier: AMI_7
Summary:
Artur Kornilowicz. On the Instructions of \SCMFSA, Formalized Mathematics 9(4), pages 673-679, 2001. MML Identifier: SCMFSA10
Summary:
Adam Grabowski. Robbins Algebras vs. Boolean Algebras, Formalized Mathematics 9(4), pages 681-690, 2001. MML Identifier: ROBBINS1
Summary: In the early 1930s, Huntington proposed several axiom systems for Boolean algebras. Robbins slightly changed one of them and asked if the resulted system is still a basis for variety of Boolean algebras. The solution (afirmative answer) was given in 1996 by McCune with the help of automated theorem prover EQP/{\sc Otter}. Some simplified and restucturized versions of this proof are known. In our version of proof that all Robbins algebras are Boolean we use the results of McCune \cite{McCuneRob}, Huntington \cite{Huntington1}, \cite{Huntington2}, \cite{Huntington3} and Dahn \cite{DahnRob}.
Noboru Endou, Takashi Mitsuishi, Keiji Ohkubo. Properties of Fuzzy Relation, Formalized Mathematics 9(4), pages 691-695, 2001. MML Identifier: FUZZY_4
Summary: In this article, we introduce four fuzzy relations and the composition, and some useful properties are shown by them. In section 2, the definition of converse relation $R^{-1}$ of fuzzy relation $R$ and properties concerning it are described. In the next section, we define the composition of the fuzzy relation and show some properties. In the final section we describe the identity relation, the universe relation and the zero relation.
Yatsuka Nakamura. On Outside Fashoda Meet Theorem, Formalized Mathematics 9(4), pages 697-704, 2001. MML Identifier: JGRAPH_2
Summary: We have proven the ``Fashoda Meet Theorem'' in \cite{JGRAPH_1.ABS}. Here we prove the outside version of it. It says that if Britain and France intended to set the courses for ships to the opposite side of Africa, they must also meet.
Grzegorz Bancerek, Piotr Rudnicki. The Set of Primitive Recursive Functions, Formalized Mathematics 9(4), pages 705-720, 2001. MML Identifier: COMPUT_1
Summary: We follow \cite{Uspenski60} in defining the set of primitive recursive functions. The important helper notion is the homogeneous function from finite sequences of natural numbers into natural numbers where homogeneous means that all the sequences in the domain are of the same length. The set of all such functions is then used to define the notion of a set closed under composition of functions and under primitive recursion. We call a set primitively recursively closed iff it contains the initial functions (nullary constant function returning 0, unary successor and projection functions for all arities) and is closed under composition and primitive recursion. The set of primitive recursive functions is then defined as the smallest set of functions which is primitive recursively closed. We show that this set can be obtained by primitive recursive approximation. We finish with showing that some simple and well known functions are primitive recursive.
Jing-Chao Chen, Yatsuka Nakamura. Introduction to Turing Machines, Formalized Mathematics 9(4), pages 721-732, 2001. MML Identifier: TURING_1
Summary: A Turing machine can be viewed as a simple kind of computer, whose operations are constrainted to reading and writing symbols on a tape, or moving along the tape to the left or right. In theory, one has proven that the computability of Turing machines is equivalent to recursive functions. This article defines and verifies the Turing machines of summation and three primitive functions which are successor, zero and project functions. It is difficult to compute sophisticated functions by simple Turing machines. Therefore, we define the combination of two Turing machines.
Grzegorz Bancerek, Noboru Endou, Yuji Sakai. On the Characterizations of Compactness, Formalized Mathematics 9(4), pages 733-738, 2001. MML Identifier: YELLOW19
Summary: In the paper we show equivalence of the convergence of filters on a topological space and the convergence of nets in the space. We also give, five characterizations of compactness. Namely, for any topological space $T$ we proved that following condition are equivalent: \begin{itemize} \itemsep-3pt \item $T$ is compact, \item every ultrafilter on $T$ is convergent, \item every proper filter on $T$ has cluster point, \item every net in $T$ has cluster point, \item every net in $T$ has convergent subnet, \item every Cauchy net in $T$ is convergent. \end{itemize}
Grzegorz Bancerek, Noboru Endou. Compactness of Lim-inf Topology, Formalized Mathematics 9(4), pages 739-743, 2001. MML Identifier: WAYBEL33
Summary: Formalization of \cite{CCL}, chapter III, section 3 (3.4--3.6).
Grzegorz Bancerek. Miscellaneous Facts about Functors, Formalized Mathematics 9(4), pages 745-754, 2001. MML Identifier: YELLOW20
Summary: In the paper we show useful facts concerning reverse and inclusion functors and the restriction of functors. We also introduce a new notation for the intersection of categories and the isomorphism under arbitrary functors.
Grzegorz Bancerek. Categorial Background for Duality Theory, Formalized Mathematics 9(4), pages 755-765, 2001. MML Identifier: YELLOW21
Summary: In the paper, we develop the notation of lattice-wise categories as concrete categories (see \cite{YELLOW18.ABS}) of lattices. Namely, the categories based on \cite{ALTCAT_1.ABS} with lattices as objects and at least monotone maps between them as morphisms. As examples, we introduce the categories {\it UPS}, {\it CONT}, and {\it ALG} with complete, continuous, and algebraic lattices, respectively, as objects and directed suprema preserving maps as morphisms. Some useful schemes to construct categories of lattices and functors between them are also presented.
Grzegorz Bancerek. Duality Based on the Galois Connection. Part I, Formalized Mathematics 9(4), pages 767-778, 2001. MML Identifier: WAYBEL34
Summary: In the paper, we investigate the duality of categories of complete lattices and maps preserving suprema or infima according to \cite[p. 179--183; 1.1--1.12]{CCL}. The duality is based on the concept of the Galois connection.
Grzegorz Bancerek, Artur Kornilowicz. Yet Another Construction of Free Algebra, Formalized Mathematics 9(4), pages 779-785, 2001. MML Identifier: MSAFREE3
Summary:
Robert Milewski. Upper and Lower Sequence of a Cage, Formalized Mathematics 9(4), pages 787-790, 2001. MML Identifier: JORDAN1E
Summary:
Barbara Dzienis. On Polynomials with Coefficients in a Ring of Polynomials, Formalized Mathematics 9(4), pages 791-794, 2001. MML Identifier: POLYNOM6
Summary: The main result of the paper is, that the ring of polynomials with $o_1$ variables and coefficients in the ring of polynomials with $o_2$ variables and coefficient in a ring $L$ is isomorphic with the ring with $o_1+o_2$ variables, and coefficients in $L$.
Adam Naumowicz. On Cosets in Segre's Product of Partial Linear Spaces, Formalized Mathematics 9(4), pages 795-800, 2001. MML Identifier: PENCIL_2
Summary: This paper is a continuation of \cite{PENCIL_1.ABS}. We prove that the family of cosets in the Segre's product of partial linear spaces remains invariant under automorphisms.
Yatsuka Nakamura. On the Simple Closed Curve Property of the Circle and the Fashoda Meet Theorem, Formalized Mathematics 9(4), pages 801-808, 2001. MML Identifier: JGRAPH_3
Summary: First, we prove the fact that the circle is the simple closed curve, which was defined as a curve homeomorphic to the square. For this proof, we introduce a mapping which is a homeomorphism from 2-dimensional plane to itself. This mapping maps the square to the circle. Secondly, we prove the Fashoda meet theorem for the circle using this homeomorphism.
Freek Wiedijk. Pythagorean Triples, Formalized Mathematics 9(4), pages 809-812, 2001. MML Identifier: PYTHTRIP
Summary: A Pythagorean triple is a set of positive integers $\{ a,b,c \}$ with $a^2 + b^2 = c^2$. We prove that every Pythagorean triple is of the form $$a = n^2 - m^2 \qquad b = 2mn \qquad c = n^2 + m^2$$ or is a multiple of such a triple. Using this characterization we show that for every $n > 2$ there exists a Pythagorean triple $X$ with $n\in X$. Also we show that even the set of {\em simplified\/} Pythagorean triples is infinite.
Adam Naumowicz. Some Remarks on Finite Sequences on Go-boards, Formalized Mathematics 9(4), pages 813-816, 2001. MML Identifier: JORDAN1F
Summary: This paper shows some properties of finite sequences on Go-boards. It also provides the partial correspondence between two ways of decomposition of curves induced by cages.
Robert Milewski. Upper and Lower Sequence on the Cage. Part II, Formalized Mathematics 9(4), pages 817-823, 2001. MML Identifier: JORDAN1G
Summary:
Tetsuya Tsunetou, Grzegorz Bancerek, Yatsuka Nakamura. Zero-Based Finite Sequences, Formalized Mathematics 9(4), pages 825-829, 2001. MML Identifier: AFINSQ_1
Summary:
Andrzej Trybulec. More on the External Approximation of a~Continuum, Formalized Mathematics 9(4), pages 831-841, 2001. MML Identifier: JORDAN1H
Summary: The main goal was to prove two facts: \begin{itemize} \itemsep-3pt \item the gauge is the Go-Board of a corresponding cage, \item the left components of the complement of the curve determined by a cage are monotonic wrt the index of the approximation. \end{itemize} Some auxiliary facts are proved, too. At the end the new notion needed for the internal approximation are defined and some useful lemmas are proved.
Andrzej Trybulec. More on the Finite Sequences on the Plane, Formalized Mathematics 9(4), pages 843-847, 2001. MML Identifier: TOPREAL8
Summary: We continue proving lemmas needed for the proof of the Jordan curve theorem. The main goal was to prove the last theorem being a mutation of the first theorem in \cite{GOBOARD3.ABS}.
Christoph Schwarzweller. More on Multivariate Polynomials: Monomials and Constant Polynomials, Formalized Mathematics 9(4), pages 849-855, 2001. MML Identifier: POLYNOM7
Summary: In this article we give some technical concepts for multivariate polynomials with arbitrary number of variables. Monomials and constant polynomials are introduced and their properties with respect to the eval functor are shown. In addition, the multiplication of polynomials with coefficients is defined and investigated.
Hisayoshi Kunimune, Grzegorz Bancerek, Yatsuka Nakamura. On State Machines of Calculating Type, Formalized Mathematics 9(4), pages 857-864, 2001. MML Identifier: FSM_2
Summary: In this article, we show the properties of the calculating type state machines. In the first section, we have defined calculating type state machines of which the state transition only depends on the first input. We have also proved theorems of the state machines. In the second section, we defined Moore machines with final states. We also introduced the concept of result of the Moore machines. In the last section, we proved the correctness of several calculating type of Moore machines.
Mariusz Giero. Hierarchies and Classifications of Sets, Formalized Mathematics 9(4), pages 865-869, 2001. MML Identifier: TAXONOM2
Summary: This article is a continuation of \cite{TAXONOM1.ABS} article. Further properties of classification of sets are proved. The notion of hierarchy of a set is introduced. Properties of partitions and hierarchies are shown. The main theorem says that for each hierarchy there exists a classification which union equals to the considered hierarchy.