Formalized Mathematics    (ISSN 0777-4028)
Volume 5, Number 1 (1996): pdf, ps, dvi.
  1. Yasushi Tanaka. On the Decomposition of the States of SCM, Formalized Mathematics 5(1), pages 1-8, 1996. MML Identifier: AMI_5
    Summary: This article continues the development of the basic terminology for the {\bf SCM} as defined in \cite{AMI_1.ABS},\cite{AMI_2.ABS}, \cite{AMI_3.ABS}. There is developed of the terminology for discussing static properties of instructions (i.e. not related to execution), for data locations, instruction locations, as well as for states and partial states of {\bf SCM}. The main contribution of the article consists in characterizing {\bf SCM} computations starting in states containing autonomic finite partial states.
  2. Grzegorz Bancerek, Piotr Rudnicki. On Defining Functions on Binary Trees, Formalized Mathematics 5(1), pages 9-13, 1996. MML Identifier: BINTREE1
    Summary: This article is a continuation of an article on defining functions on trees (see \cite{DTCONSTR.ABS}). In this article we develop terminology specialized for binary trees, first defining binary trees and binary grammars. We recast the induction principle for the set of parse trees of binary grammars and the scheme of defining functions inductively with the set as domain. We conclude with defining the scheme of defining such functions by lambda-like expressions.
  3. Grzegorz Bancerek, Piotr Rudnicki. A Compiler of Arithmetic Expressions for SCM, Formalized Mathematics 5(1), pages 15-20, 1996. MML Identifier: SCM_COMP
    Summary: We define a set of binary arithmetic expressions with the following operations: $+$, $-$, $\cdot$, {\tt mod}, and {\tt div} and formalize the common meaning of the expressions in the set of integers. Then, we define a compile function that for a given expression results in a program for the {\bf SCM} machine defined by Nakamura and Trybulec in \cite{AMI_1.ABS}. We prove that the generated program when loaded into the machine and executed computes the value of the expression. The program uses additional memory and runs in time linear in length of the expression.
  4. Jozef Bialas. Some Properties of the Intervals, Formalized Mathematics 5(1), pages 21-26, 1996. MML Identifier: MEASURE6
    Summary:
  5. Yasuho Mizuhara, Takaya Nishiyama. Binary Arithmetics, Addition and Subtraction of Integers, Formalized Mathematics 5(1), pages 27-29, 1996. MML Identifier: BINARI_2
    Summary: This article is a continuation of \cite{BINARITH.ABS} and presents the concepts of binary arithmetic operations for integers. There is introduced 2's complement representation of integers and natural numbers to integers are expanded. The binary addition and subtraction for integers are defined and theorems on the relationship between binary and numerical operations presented.
  6. Agnieszka Julia Marasik. Boolean Properties of Lattices, Formalized Mathematics 5(1), pages 31-35, 1996. MML Identifier: BOOLEALG
    Summary:
  7. Andrzej Trybulec. Many Sorted Algebras, Formalized Mathematics 5(1), pages 37-42, 1996. MML Identifier: MSUALG_1
    Summary: The basic purpose of the paper is to prepare preliminaries of the theory of many sorted algebras. The concept of the signature of a many sorted algebra is introduced as well as the concept of many sorted algebra itself. Some auxiliary related notions are defined. The correspondence between (1 sorted) universal algebras \cite{UNIALG_1.ABS} and many sorted algebras with one sort only is described by introducing two functors mapping one into the other. The construction is done this way that the composition of both functors is the identity on universal algebras.
  8. Artur Kornilowicz. On the Group of Inner Automorphisms, Formalized Mathematics 5(1), pages 43-45, 1996. MML Identifier: AUTGROUP
    Summary:
  9. Ewa Burakowska. Subalgebras of Many Sorted Algebra. Lattice of Subalgebras, Formalized Mathematics 5(1), pages 47-54, 1996. MML Identifier: MSUALG_2
    Summary:
  10. Beata Madras. Products of Many Sorted Algebras, Formalized Mathematics 5(1), pages 55-60, 1996. MML Identifier: PRALG_2
    Summary: Product of two many sorted universal algebras and product of family of many sorted universal algebras are defined in this article. Operations on functions, such that commute, Frege, are also introduced.
  11. Malgorzata Korolkiewicz. Homomorphisms of Many Sorted Algebras, Formalized Mathematics 5(1), pages 61-65, 1996. MML Identifier: MSUALG_3
    Summary: The aim of this article is to present the definition and some properties of homomorphisms of many sorted algebras. Some auxiliary properties of many sorted functions also have been shown.
  12. Beata Perkowska. Free Many Sorted Universal Algebra, Formalized Mathematics 5(1), pages 67-74, 1996. MML Identifier: MSAFREE
    Summary:
  13. Mariusz Zynel, Adam Guzowski. \Tzero\ Topological Spaces, Formalized Mathematics 5(1), pages 75-77, 1996. MML Identifier: T_0TOPSP
    Summary:
  14. Malgorzata Korolkiewicz. Many Sorted Quotient Algebra, Formalized Mathematics 5(1), pages 79-84, 1996. MML Identifier: MSUALG_4
    Summary: This article introduces the construction of a many sorted quotient algebra. A few preliminary notions such as a many sorted relation, a many sorted equivalence relation, a many sorted congruence and the set of all classes of a many sorted relation are also formulated.
  15. Grzegorz Bancerek. Quantales, Formalized Mathematics 5(1), pages 85-91, 1996. MML Identifier: QUANTAL1
    Summary: The concepts of Girard quantales (see \cite{GIRARD:TCS50} and \cite{YETTER}) and Blikle nets (see \cite{BLIKLE}) are introduced.
  16. Agnieszka Sakowicz, Jaroslaw Gryko, Adam Grabowski. Sequences in $\calE^N_\rmT$, Formalized Mathematics 5(1), pages 93-96, 1996. MML Identifier: TOPRNS_1
    Summary:
  17. Yatsuka Nakamura, Czeslaw Bylinski. Extremal Properties of Vertices on Special Polygons. Part I, Formalized Mathematics 5(1), pages 97-102, 1996. MML Identifier: SPPOL_1
    Summary: First, extremal properties of endpoints of line segments in n-dimensional Euclidean space are discussed. Some topological properties of line segments are also discussed. Secondly, extremal properties of vertices of special polygons which consist of horizontal and vertical line segments in 2-dimensional Euclidean space, are also derived.
  18. Yasushi Tanaka. Relocatability, Formalized Mathematics 5(1), pages 103-108, 1996. MML Identifier: RELOC
    Summary: This article defines the concept of relocating the program part of a finite partial state of {\bf SCM} (data part stays intact). The relocated program differs from the original program in that all jump instructions are adjusted by the relocation factor and other instructions remain unchanged. The main theorem states that if a program computes a function then the relocated program computes the same function, and vice versa.
  19. Zbigniew Karno. Maximal Anti-Discrete Subspaces of Topological Spaces, Formalized Mathematics 5(1), pages 109-118, 1996. MML Identifier: TEX_4
    Summary: Let $X$ be a topological space and let $A$ be a subset of $X$. $A$ is said to be {\em anti-discrete}\/ provided for every open subset $G$ of $X$ either $A \cap G = \emptyset$ or $A \subseteq G$; equivalently, for every closed subset $F$ of $X$ either $A \cap F = \emptyset$ or $A \subseteq F$. An anti-discrete subset $M$ of $X$ is said to be {\em maximal anti-discrete}\/ provided for every anti-discrete subset $A$ of $X$ if $M \subseteq A$ then $M = A$. A subspace of $X$ is {\em maximal anti-discrete}\/ iff its carrier is maximal anti-discrete in $X$. The purpose is to list a few properties of maximal anti-discrete sets and subspaces in Mizar formalism.\par It is shown that every $x \in X$ is contained in a unique maximal anti-discrete subset M$(x)$ of $X$, denoted in the text by MaxADSet($x$). Such subset can be defined by $${\rm M}(x) = \bigcap\ \{ S \subseteq X : x \in S,\ {\rm and}\ S \ {\rm is}\ {\rm open}\ {\rm or}\ {\rm closed}\ {\rm in}\ X\}.$$ It has the following remarkable properties: (1) $y \in {\rm M}(x)$ iff ${\rm M}(y) = {\rm M}(x)$, (2) either ${\rm M}(x) \cap {\rm M}(y) = \emptyset$ or ${\rm M}(x) = {\rm M}(y)$, (3) ${\rm M}(x) = {\rm M}(y)$ iff $\overline{\{x\}} = \overline{\{y\}}$, and (4) ${\rm M}(x) \cap {\rm M}(y) = \emptyset$ iff $\overline{\{x\}} \neq \overline{\{y\}}$. It follows from these properties that $\{{\rm M}(x) : x \in X\}$ is the $T_{0}$-partition of $X$ defined by M.H.~Stone in \cite{STONE:3}.\par Moreover, it is shown that the operation M defined on all subsets of $X$ by $${\rm M}(A) = \bigcup\ \{{\rm M}(x) : x \in A\},$$ denoted in the text by MaxADSet($A$), satisfies the Kuratowski closure axioms (see e.g., \cite{KURAT:2}), i.e., (1) ${\rm M}(A \cup B) = {\rm M}(A) \cup {\rm M}(B)$, (2) ${\rm M}(A) = {\rm M}({\rm M}(A))$, (3) $A \subseteq {\rm M}(A)$,and (4) ${\rm M}(\emptyset) = \emptyset$. Note that this operation commutes with the usual closure operation of $X$, and if $A$ is an open (or a closed) subset of $X$, then ${\rm M}(A) = A$.
  20. Zbigniew Karno. On Kolmogorov Topological Spaces, Formalized Mathematics 5(1), pages 119-124, 1996. MML Identifier: TSP_1
    Summary: Let $X$ be a topological space. $X$ is said to be {\em $T_{0}$-space}\/ (or {\em Kolmogorov space}) provided for every pair of distinct points $x,\,y \in X$ there exists an open subset of $X$ containing exactly one of these points; equivalently, for every pair of distinct points $x,\,y \in X$ there exists a closed subset of $X$ containing exactly one of these points (see \cite{ALEX-HOPF}, \cite{KURAT:2}, \cite{ENGEL:1}).\par The purpose is to list some of the standard facts on Kolmogorov spaces, using Mizar formalism. As a sample we formulate the following characteristics of such spaces: {\em $X$ is a Kolmogorov space iff for every pair of distinct points $x,\,y \in X$ the closures $\overline{\{x\}}$ and $\overline{\{y\}}$ are distinct}.\par There is also reviewed analogous facts on Kolmogorov subspaces of topological spaces. In the presented approach $T_{0}$-subsets are introduced and some of their properties developed.
  21. Zbigniew Karno. Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space, Formalized Mathematics 5(1), pages 125-130, 1996. MML Identifier: TSP_2
    Summary: Let $X$ be a topological space. $X$ is said to be {\em $T_{0}$-space}\/ (or {\em Kolmogorov space}) provided for every pair of distinct points $x,\,y \in X$ there exists an open subset of $X$ containing exactly one of these points (see \cite{ALEX-HOPF}, \cite{KURAT:2}, \cite{ENGEL:1}). Such spaces and subspaces were investigated in Mizar formalism in \cite{TSP_1.ABS}. A Kolmogorov subspace $X_{0}$ of a topological space $X$ is said to be {\em maximal}\/ provided for every Kolmogorov subspace $Y$ of $X$ if $X_{0}$ is subspace of $Y$ then the topological structures of $Y$ and $X_{0}$ are the same.\par M.H.~Stone proved in \cite{STONE:3} that every topological space can be made into a Kolmogorov space by identifying points with the same closure (see also \cite{THRON:1}). The purpose is to generalize the Stone result, using Mizar System. It is shown here that: (1) {\em in every topological space $X$ there exists a maximal Kolmogorov subspace $X_{0}$ of $X$}, and (2) {\em every maximal Kolmogorov subspace $X_{0}$ of $X$ is a continuous retract of $X$}. Moreover, {\em if $r : X \rightarrow X_{0}$ is a continuous retraction of $X$ onto a maximal Kolmogorov subspace $X_{0}$ of $X$, then $r^{-1}(x) = {\rm MaxADSet}(x)$ for any point $x$ of $X$ belonging to $X_{0}$, where ${\rm MaxADSet}(x)$ is a unique maximal anti-discrete subset of $X$ containing $x$} (see \cite{TEX_4.ABS} for the precise definition of the set ${\rm MaxADSet}(x)$). The retraction $r$ from the last theorem is defined uniquely, and it is denoted in the text by ``Stone-retraction". It has the following two remarkable properties: $r$ is open, i.e., sends open sets in $X$ to open sets in $X_{0}$, and $r$ is closed, i.e., sends closed sets in $X$ to closed sets in $X_{0}$.\par These results may be obtained by the methods described by R.H. Warren in \cite{WARREN:1}.
  22. Michal Muzalewski. Projective Planes, Formalized Mathematics 5(1), pages 131-136, 1996. MML Identifier: PROJPL_1
    Summary: The line of points $a$, $b$, denoted by $a\cdot b$ and the point of lines $A$, $B$ denoted by $A\cdot B$ are defined. A few basic theorems related to these notions are proved. An inspiration for such approach comes from so called Leibniz program. Let us recall that the Leibniz program is a program of algebraization of geometry using purely geometric notions. Leibniz formulated his program in opposition to algebraization method developed by Descartes.
  23. Yozo Toda. The Formalization of Simple Graphs, Formalized Mathematics 5(1), pages 137-144, 1996. MML Identifier: SGRAPH1
    Summary: A graph is simple when \begin{itemize} \parskip -1mm \item it is non-directed, \item there is at most one edge between two vertices, \item there is no loop of length one. \end{itemize} A formalization of simple graphs is given from scratch. There is already an article \cite{GRAPH_1.ABS}, dealing with the similar subject. It is not used as a starting-point, because \cite{GRAPH_1.ABS} formalizes directed non-empty graphs. Given a set of vertices, edge is defined as an (unordered) pair of different two vertices and graph as a pair of a set of vertices and a set of edges.\par The following concepts are introduced: \begin{itemize} \parskip -1mm \item simple graph structure, \item the set of all simple graphs, \item equality relation on graphs. \item the notion of degrees of vertices; the number of edges connected to, or the number of adjacent vertices, \item the notion of subgraphs, \item path, cycle, \item complete and bipartite complete graphs, \end{itemize}\par Theorems proved in this articles include: \begin{itemize} \parskip -1mm \item the set of simple graphs satisfies a certain minimality condition, \item equivalence between two notions of degrees. \end{itemize}
  24. Katarzyna Zawadzka. Solvable Groups, Formalized Mathematics 5(1), pages 145-147, 1996. MML Identifier: GRSOLV_1
    Summary: The concept of solvable group is introduced. Some theorems concerning heirdom of solvability are proved.