Formalized Mathematics    (ISSN 1426-2630)
Volume 5, Number 2 (1996): pdf, ps, dvi.
  1. Grzegorz Bancerek. Ideals, Formalized Mathematics 5(2), pages 149-156, 1996. MML Identifier: FILTER_2
    Summary: The dual concept to filters (see \cite{FILTER_0.ABS}, \cite{FILTER_1.ABS}) i.e. ideals of a lattice is introduced.
  2. Grzegorz Bancerek. Categorial Categories and Slice Categories, Formalized Mathematics 5(2), pages 157-165, 1996. MML Identifier: CAT_5
    Summary: By categorial categories we mean categories with categories as objects and morphisms of the form $(C_1, C_2, F)$, where $C_1$ and $C_2$ are categories and $F$ is a functor from $C_1$ into $C_2$.
  3. Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, Pauline N. Kawamoto. Preliminaries to Circuits, I, Formalized Mathematics 5(2), pages 167-172, 1996. MML Identifier: PRE_CIRC
    Summary: This article is the first in a series of four articles (continued in \cite{MSAFREE2.ABS},\cite{CIRCUIT1.ABS},\cite{CIRCUIT2.ABS}) about modelling circuits by many-sorted algebras.\par Here, we introduce some auxiliary notations and prove auxiliary facts about many sorted sets, many sorted functions and trees.
  4. Miroslava Kaloper , Piotr Rudnicki. Minimization of finite state machines, Formalized Mathematics 5(2), pages 173-184, 1996. MML Identifier: FSM_1
    Summary: We have formalized deterministic finite state machines closely following the textbook \cite{ddq}, pp. 88--119 up to the minimization theorem. In places, we have changed the approach presented in the book as it turned out to be too specific and inconvenient. Our work also revealed several minor mistakes in the book. After defining a structure for an outputless finite state machine, we have derived the structures for the transition assigned output machine (Mealy) and state assigned output machine (Moore). The machines are then proved similar, in the sense that for any Mealy (Moore) machine there exists a Moore (Mealy) machine producing essentially the same response for the same input. The rest of work is then done for Mealy machines. Next, we define equivalence of machines, equivalence and $k$-equivalence of states, and characterize a process of constructing for a given Mealy machine, the machine equivalent to it in which no two states are equivalent. The final, minimization theorem states: \begin{quotation} \noindent {\bf Theorem 4.5:} Let {\bf M}$_1$ and {\bf M}$_2$ be reduced, connected finite-state machines. Then the state graphs of {\bf M}$_1$ and {\bf M}$_2$ are isomorphic if and only if {\bf M}$_1$ and {\bf M}$_2$ are equivalent. \end{quotation} and it is the last theorem in this article.
  5. Grzegorz Bancerek. Subtrees, Formalized Mathematics 5(2), pages 185-190, 1996. MML Identifier: TREES_9
    Summary: The concepts of root tree, the set of successors of a node in decorated tree and sets of subtrees are introduced.
  6. Grzegorz Bancerek. Terms Over Many Sorted Universal Algebra, Formalized Mathematics 5(2), pages 191-198, 1996. MML Identifier: MSATERM
    Summary: Pure terms (without constants) over a signature of many sorted universal algebra and terms with constants from algebra are introduced. Facts on evaluation of a term in some valuation are proved.
  7. Marian Przemski. On the Decomposition of the Continuity, Formalized Mathematics 5(2), pages 199-204, 1996. MML Identifier: DECOMP_1
    Summary: This article is devoted to functions of general topological spaces. A function from $X$ to $Y$ is $A$-continuous if the counterimage of every open set $V$ of $Y$ belongs to $A$, where $A$ is a collection of subsets of $X$. We give the following characteristics of the continuity, called decomposition of continuity: A function $f$ is continuous if and only if it is both $A$-continuous and $B$-continuous.
  8. Andrzej Trybulec. A Scheme for Extensions of Homomorphisms of Manysorted Algebras, Formalized Mathematics 5(2), pages 205-209, 1996. MML Identifier: MSAFREE1
    Summary: The aim of this work is to provide a bridge between the theory of context-free grammars developed in \cite{LANG1.ABS}, \cite{DTCONSTR.ABS} and universally free manysorted algebras(\cite{MSAFREE.ABS}. The third scheme proved in the article allows to prove that two homomorphisms equal on the set of free generators are equal. The first scheme is a slight modification of the scheme in \cite{DTCONSTR.ABS} and the second is rather technical, but since it was useful for me, perhaps it might be useful for somebody else. The concept of flattening of a many sorted function $F$ between two manysorted sets $A$ and $B$ (with common set of indices $I$) is introduced for $A$ with mutually disjoint components (pairwise disjoint function -- the concept introduced in \cite{PROB_2.ABS}). This is a function on the union of $A$, that is equal to $F$ on every component of $A$. A trivial many sorted algebra over a signature $S$ is defined with sorts being singletons of corresponding sort symbols. It has mutually disjoint sorts.}
  9. Adam Grabowski. The Correspondence Between Homomorphisms of Universal Algebra \& Many Sorted Algebra, Formalized Mathematics 5(2), pages 211-214, 1996. MML Identifier: MSUHOM_1
    Summary: The aim of the article is to check the compatibility of the homomorphism of universal algebras introduced in \cite{ALG_1.ABS} and the corresponding concept for many sorted algebras introduced in \cite{MSUALG_3.ABS}.
  10. Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, Pauline N. Kawamoto. Preliminaries to Circuits, II, Formalized Mathematics 5(2), pages 215-220, 1996. MML Identifier: MSAFREE2
    Summary: This article is the second in a series of four articles (started with \cite{PRE_CIRC.ABS} and continued in \cite{CIRCUIT1.ABS}, \cite{CIRCUIT2.ABS}) about modelling circuits by many sorted algebras.\par First, we introduce some additional terminology for many sorted signatures. The vertices of such signatures are divided into input vertices and inner vertices. A many sorted signature is called {\em circuit like} if each sort is a result sort of at most one operation. Next, we introduce some notions for many sorted algebras and many sorted free algebras. Free envelope of an algebra is a free algebra generated by the sorts of the algebra. Evaluation of an algebra is defined as a homomorphism from the free envelope of the algebra into the algebra. We define depth of elements of free many sorted algebras.\par A many sorted signature is said to be monotonic if every finitely generated algebra over it is locally finite (finite in each sort). Monotonic signatures are used (see \cite{CIRCUIT1.ABS},\cite{CIRCUIT2.ABS}) in modelling backbones of circuits without directed cycles.
  11. Artur Kornilowicz. On the Group of Automorphisms of Universal Algebra \& Many Sorted Algebra, Formalized Mathematics 5(2), pages 221-226, 1996. MML Identifier: AUTALG_1
    Summary: The aim of the article is to check the compatibility of the automorphisms of universal algebras introduced in \cite{ALG_1.ABS} and the corresponding concept for many sorted algebras introduced in \cite{MSUALG_3.ABS}.
  12. Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, Pauline N. Kawamoto. Introduction to Circuits, I, Formalized Mathematics 5(2), pages 227-232, 1996. MML Identifier: CIRCUIT1
    Summary: This article is the third in a series of four articles (preceded by \cite{PRE_CIRC.ABS},\cite{MSAFREE2.ABS} and continued in \cite{CIRCUIT2.ABS}) about modelling circuits by many sorted algebras.\par A circuit is defined as a locally-finite algebra over a circuit-like many sorted signature. For circuits we define notions of input function and of circuit state which are later used (see \cite{CIRCUIT2.ABS}) to define circuit computations. For circuits over monotonic signatures we introduce notions of vertex size and vertex depth that characterize certain graph properties of circuit's signature in terms of elements of its free envelope algebra. The depth of a finite circuit is defined as the maximal depth over its vertices.
  13. Alexander Yu. Shibakov, Andrzej Trybulec. The Cantor Set, Formalized Mathematics 5(2), pages 233-236, 1996. MML Identifier: CANTOR_1
    Summary: The aim of the paper is to define some basic notions of the theory of topological spaces like basis and prebasis, and to prove their simple properties. The definition of the Cantor set is given in terms of countable product of $\{0,1\}$ and a collection of its subsets to serve as a prebasis.
  14. Oleg Okhotnikov. Logical Equivalence of Formulae, Formalized Mathematics 5(2), pages 237-240, 1996. MML Identifier: CQC_THE3
    Summary:
  15. Czeslaw Bylinski. Some Properties of Restrictions of Finite Sequences, Formalized Mathematics 5(2), pages 241-245, 1996. MML Identifier: FINSEQ_5
    Summary: The aim of the paper is to define some basic notions of restrictions of finite sequences.
  16. Czeslaw Bylinski, Yatsuka Nakamura. Special Polygons, Formalized Mathematics 5(2), pages 247-252, 1996. MML Identifier: SPPOL_2
    Summary:
  17. Jozef Bialas. The One-Dimensional Lebesgue Measure, Formalized Mathematics 5(2), pages 253-258, 1996. MML Identifier: MEASURE7
    Summary: The paper is the crowning of a series of articles written in the Mizar language, being a formalization of notions needed for the description of the one-dimensional Lebesgue measure. The formalization of the notion as classical as the Lebesgue measure determines the powers of the PC Mizar system as a tool for the strict, precise notation and verification of the correctness of deductive theories. Following the successive articles \cite{SUPINF_1.ABS}, \cite{SUPINF_2.ABS}, \cite{MEASURE1.ABS}, \cite{MEASURE6.ABS} constructed so that the final one should include the definition and the basic properties of the Lebesgue measure, we observe one of the paths relatively simple in the sense of the definition, enabling us the formal introduction of this notion. This way, although toilsome, since such is the nature of formal theories, is greatly instructive. It brings home the proper succession of the introduction of the definitions of intermediate notions and points out to those elements of the theory which determine the essence of the complexity of the notion being introduced.\par The paper includes the definition of the $\sigma$-field of Lebesgue measurable sets, the definition of the Lebesgue measure and the basic set of the theorems describing its properties.
  18. Andrzej Trybulec. Categories without Uniqueness of \bf cod and \bf dom, Formalized Mathematics 5(2), pages 259-267, 1996. MML Identifier: ALTCAT_1
    Summary: Category theory had been formalized in Mizar quite early \cite{CAT_1.ABS}. This had been done closely to the handbook of S. McLane \cite{MACLANE:1}. In this paper we use a different approach. Category is a triple $$\langle O, {\{ \langle o_1,o_2 \rangle \}}_{o_1,o_2 \in O}, {\{ \circ_{o_1,o_2,o_3}\}}_{o_1,o_2,o_3 \in O} \rangle$$ where $\circ_{o_1,o_2,o_3}: \langle o_2,o_3 \rangle \times \langle o_1,o_2 \rangle \to \langle o_1, o_3 \rangle$ that satisfies usual conditions (associativity and the existence of the identities). This approach is closer to the way in which categories are presented in homological algebra (e.g. \cite{BALCERZYK}, pp.58-59). We do not assume that $\langle o_1,o_2 \rangle$'s are mutually disjoint. If $f$ is simultaneously a morphism from $o_1$ to $o_2$ and $o_1'$ to $o_2$ ($o_1 \neq o_1'$) than different compositions are used ($\circ_{o_1,o_2,o_3}$ or $\circ_{o_1',o_2,o_3}$) to compose it with a morphism $g$ from $o_2$ to $o_3$. The operation $g\cdot f$ has actually six arguments (two visible and four hidden: three objects and the category).\par We introduce some simple properties of categories. Perhaps more than necessary. It is partially caused by the formalization. The functional categories are characterized by the following properties: \begin{itemize} \item quasi-functional that means that morphisms are functions (rather meaningless, if it stands alone) \item semi-functional that means that the composition of morphism is the composition of functions, provided they are functions. \item pseudo-functional that means that the composition of morphisms is the composition of functions. \end{itemize} For categories pseudo-functional is just quasi-functional and semi-functional, but we work in a bit more general setting. Similarly the concept of a discrete category is split into two: \begin{itemize} \item quasi-discrete that means that $\langle o_1,o_2 \rangle$ is empty for $o_1 \neq o_2$ and \item pseudo-discrete that means that $\langle o, o \rangle$ is trivial, i.e. consists of the identity only, in a category. \end{itemize}\par We plan to follow Semadeni-Wiweger book \cite{SEMAD}, in the development the category theory in Mizar. However, the beginning is not very close to \cite{SEMAD}, because of the approach adopted and because we work in Tarski-Grothendieck set theory.
  19. Artur Kornilowicz. Extensions of Mappings on Generator Set, Formalized Mathematics 5(2), pages 269-272, 1996. MML Identifier: EXTENS_1
    Summary: The aim of the article is to prove the fact that if extensions of mappings on generator set are equal then these mappings are equal. The article contains the properties of epimorphisms and monomorphisms between Many Sorted Algebras.
  20. Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, Pauline N. Kawamoto. Introduction to Circuits, II, Formalized Mathematics 5(2), pages 273-278, 1996. MML Identifier: CIRCUIT2
    Summary: This article is the last in a series of four articles (preceded by \cite{PRE_CIRC.ABS}, \cite{MSAFREE2.ABS}, \cite{CIRCUIT1.ABS}) about modelling circuits by many sorted algebras.\par The notion of a circuit computation is defined as a sequence of circuit states. For a state of a circuit the next state is given by executing operations at circuit vertices in the current state, according to denotations of the operations. The values at input vertices at each state of a computation are provided by an external sequence of input values. The process of how input values propagate through a circuit is described in terms of a homomorphism of the free envelope algebra of the circuit into itself. We prove that every computation of a circuit over a finite monotonic signature and with constant input values stabilizes after executing the number of steps equal to the depth of the circuit.
  21. Artur Kornilowicz. Definitions and Basic Properties of Boolean \& Union of Many Sorted Sets, Formalized Mathematics 5(2), pages 279-281, 1996. MML Identifier: MBOOLEAN
    Summary: In the first part of this article I have proved theorems about boolean of many sorted sets which are corresponded to theorems about boolean of sets, whereas the second part of this article contains propositions about union of many sorted sets. Boolean as well as union of many sorted sets are defined as boolean and union on every sorts.
  22. Yatsuka Nakamura, Grzegorz Bancerek. Combining of Circuits, Formalized Mathematics 5(2), pages 283-295, 1996. MML Identifier: CIRCCOMB
    Summary: We continue the formalisation of circuits started in \cite{PRE_CIRC.ABS},\cite{MSAFREE2.ABS},\cite{CIRCUIT1.ABS}, \cite{CIRCUIT2.ABS}. Our goal was to work out the notation of combining circuits which could be employed to prove the properties of real circuits.