Formalized Mathematics    (ISSN 1426-2630)
Volume 6, Number 1 (1997): pdf, ps, dvi.
  1. Yatsuka Nakamura, Andrzej Trybulec. Adjacency Concept for Pairs of Natural Numbers, Formalized Mathematics 6(1), pages 1-3, 1997. MML Identifier: GOBRD10
    Summary: First, we introduce the concept of adjacency for a pair of natural numbers. Second, we extend the concept for two pairs of natural numbers. The pairs represent points of a lattice in a plane. We show that if some property is infectious among adjacent points, and some points have the property, then all points have the property.
  2. Adam Grabowski. Inverse Limits of Many Sorted Algebras, Formalized Mathematics 6(1), pages 5-8, 1997. MML Identifier: MSALIMIT
    Summary: This article introduces the construction of an inverse limit of many sorted algebras. A few preliminary notions such as an ordered family of many sorted algebras and a binding of family are formulated. Definitions of a set of many sorted signatures and a set of signature morphisms are also given.
  3. Artur Kornilowicz. On the Trivial Many Sorted Algebras and Many Sorted Congruences, Formalized Mathematics 6(1), pages 9-15, 1997. MML Identifier: MSUALG_9
    Summary: This paper contains properties of many sorted functions between two many sorted sets. Other theorems describe trivial many sorted algebras. In the last section there are theorems about many sorted congruences, which are defined on many sorted algebras. I have also proved facts about natural epimorphism.
  4. Adam Grabowski. Examples of Category Structures, Formalized Mathematics 6(1), pages 17-20, 1997. MML Identifier: MSINST_1
    Summary: This article contains definitions of two category structures: the category of many sorted signatures and the category of many sorted algebras. Some facts about these structures are proved.
  5. Andrzej Trybulec, Yatsuka Nakamura, Noriko Asamoto. On the Compositions of Macro Instructions. Part I, Formalized Mathematics 6(1), pages 21-27, 1997. MML Identifier: SCMFSA6A
    Summary:
  6. Piotr Rudnicki, Andrzej Trybulec. Memory Handling for \SCMFSA, Formalized Mathematics 6(1), pages 29-36, 1997. MML Identifier: SF_MASTR
    Summary: We introduce some terminology for reasoning about memory used in programs in general and in macro instructions (introduced in \cite{SCMFSA6A.ABS}) in particular. The usage of integer locations and of finite sequence locations by a program is treated separately. We define some functors for selecting memory locations needed for local (temporary) variables in macro instructions. Some semantic properties of the introduced notions are given in terms of executions of macro instructions.
  7. Yatsuka Nakamura, Andrzej Trybulec. Some Topological Properties of Cells in $\calE^2_\rmT$, Formalized Mathematics 6(1), pages 37-40, 1997. MML Identifier: GOBRD11
    Summary: We examine the topological property of cells (rectangles) in a plane. First, some Fraenkel expressions of cells are shown. Second, it is proved that cells are closed. The last theorem asserts that the closure of the interior of a cell is the same as itself.
  8. Noriko Asamoto, Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec. On the Composition of Macro Instructions. Part II, Formalized Mathematics 6(1), pages 41-47, 1997. MML Identifier: SCMFSA6B
    Summary: We define the semantics of macro instructions (introduced in \cite{SCMFSA6A.ABS}) in terms of executions of ${\bf SCM}_{\rm FSA}$. In a similar way, we define the semantics of macro composition. Several attributes of macro instructions are introduced (paraclosed, parahalting, keeping 0) and their usage enables a systematic treatment of the composition of macro intructions. This article is continued in \cite{SCMFSA6C.ABS}.
  9. Yatsuka Nakamura, Andrzej Trybulec. The First Part of Jordan's Theorem for Special Polygons, Formalized Mathematics 6(1), pages 49-51, 1997. MML Identifier: GOBRD12
    Summary: We prove here the first part of Jordan's theorem for special polygons, i.e., the complement of a special polygon is the union of two components (a left component and a right component). At this stage, we do not know if the two components are different from each other.
  10. Noriko Asamoto, Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec. On the Composition of Macro Instructions. Part III, Formalized Mathematics 6(1), pages 53-57, 1997. MML Identifier: SCMFSA6C
    Summary: This article is a continuation of \cite{SCMFSA6A.ABS} and \cite{SCMFSA6C.ABS}. First, we recast the semantics of the macro composition in more convenient terms. Then, we introduce terminology and basic properties of macros constructed out of single instructions of ${\bf SCM}_{\rm FSA}$. We give the complete semantics of composing a macro instruction with an instruction and for composing two machine instructions (this is also done in terms of macros). The introduced terminology is tested on the simple example of a macro for swapping two integer locations.
  11. Noriko Asamoto. Constant Assignment Macro Instructions of \SCMFSA. Part II, Formalized Mathematics 6(1), pages 59-63, 1997. MML Identifier: SCMFSA7B
    Summary:
  12. Noriko Asamoto. Conditional Branch Macro Instructions of \SCMFSA. Part I, Formalized Mathematics 6(1), pages 65-72, 1997. MML Identifier: SCMFSA8A
    Summary:
  13. Noriko Asamoto. Conditional Branch Macro Instructions of \SCMFSA. Part II, Formalized Mathematics 6(1), pages 73-80, 1997. MML Identifier: SCMFSA8B
    Summary:
  14. Grzegorz Bancerek. Bounds in Posets and Relational Substructures, Formalized Mathematics 6(1), pages 81-91, 1997. MML Identifier: YELLOW_0
    Summary: Notation and facts necessary to start with the formalization of continuous lattices according to \cite{CCL} are introduced.
  15. Grzegorz Bancerek. Directed Sets, Nets, Ideals, Filters, and Maps, Formalized Mathematics 6(1), pages 93-107, 1997. MML Identifier: WAYBEL_0
    Summary: Notation and facts necessary to start with the formalization of continuous lattices according to \cite{CCL} are introduced. The article contains among other things, the definition of directed and filtered subsets of a poset (see 1.1 in \cite[p.~2]{CCL}), the definition of nets on the poset (see 1.2 in \cite[p.~2]{CCL}), the definition of ideals and filters and the definition of maps preserving arbitrary and directed sups and arbitrary and filtered infs (1.9 also in \cite[p.~4]{CCL}). The concepts of semilattices, sup-semiletices and poset lattices (1.8 in \cite[p.~4]{CCL}) are also introduced. A number of facts concerning the above notion and including remarks 1.4, 1.5, and 1.10 from \cite[pp.~3--5]{CCL} is presented.
  16. Piotr Rudnicki, Andrzej Trybulec. Fixpoints in Complete Lattices, Formalized Mathematics 6(1), pages 109-115, 1997. MML Identifier: KNASTER
    Summary: Theorem (5) states that if an iterate of a function has a unique fixpoint then it is also the fixpoint of the function. It has been included here in response to P. Andrews claim that such a proof in set theory takes thousands of lines when one starts with the axioms. While probably true, such a claim is misleading about the usefulness of proof-checking systems based on set theory.\par Next, we prove the existence of the least and the greatest fixpoints for $\subseteq$-monotone functions from a powerset to a powerset of a set. Scheme {\it Knaster} is the Knaster theorem about the existence of fixpoints, cf. \cite{lns82}. Theorem (11) is the Banach decomposition theorem which is then used to prove the Schr\"{o}der-Bernstein theorem (12) (we followed Paulson's development of these theorems in Isabelle \cite{lcp95}). It is interesting to note that the last theorem when stated in Mizar in terms of cardinals becomes trivial to prove as in the Mizar development of cardinals the $\leq$ relation is synonymous with $\subseteq$.\par Section 3 introduces the notion of the lattice of a lattice subset provided the subset has lubs and glbs.\par The main theorem of Section 4 is the Tarski theorem (43) that every monotone function $f$ over a complete lattice $L$ has a complete lattice of fixpoints. As the consequence of this theorem we get the existence of the least fixpoint equal to $f^\beta(\bot_L)$ for some ordinal $\beta$ with cardinality not bigger than the cardinality of the carrier of $L$, cf. \cite{lns82}, and analogously the existence of the greatest fixpoint equal to $f^\beta(\top_L)$.\par Section 5 connects the fixpoint properties of monotone functions over complete lattices with the fixpoints of $\subseteq$-monotone functions over the lattice of subsets of a set (Boolean lattice).
  17. Adam Grabowski, Robert Milewski. Boolean Posets, Posets under Inclusion and Products of Relational Structures, Formalized Mathematics 6(1), pages 117-121, 1997. MML Identifier: YELLOW_1
    Summary: In the paper some notions useful in formalization of \cite{CCL} are introduced, e.g. the definition of the poset of subsets of a set with inclusion as an ordering relation. Using the theory of many sorted sets authors formulate the definition of product of relational structures.
  18. Mariusz Zynel, Czeslaw Bylinski. Properties of Relational Structures, Posets, Lattices and Maps, Formalized Mathematics 6(1), pages 123-130, 1997. MML Identifier: YELLOW_2
    Summary: In the paper we present some auxiliary facts concerning posets and maps between them. Our main purpose, however is to give an account on complete lattices and lattices of ideals. A sufficient condition that a lattice might be complete, the fixed-point theorem and two remarks upon images of complete lattices in monotone maps, introduced in \cite[pp. 8--9]{CCL}, can be found in Section~7. Section~8 deals with lattices of ideals. We examine the meet and join of two ideals. In order to show that the lattice of ideals is complete, the infinite intersection of ideals is investigated.
  19. Czeslaw Bylinski. Galois Connections, Formalized Mathematics 6(1), pages 131-143, 1997. MML Identifier: WAYBEL_1
    Summary: The paper is the Mizar encoding of the chapter 0 section 3 of \cite{CCL} In the paper the following concept are defined: Galois connections, Heyting algebras, and Boolean algebras.
  20. Artur Kornilowicz. Cartesian Products of Relations and Relational Structures, Formalized Mathematics 6(1), pages 145-152, 1997. MML Identifier: YELLOW_3
    Summary: In this paper the definitions of cartesian products of relations and relational structures are introduced. Facts about these notions are proved. This work is the continuation of formalization of \cite{CCL}.
  21. Artur Kornilowicz. Definitions and Properties of the Join and Meet of Subsets, Formalized Mathematics 6(1), pages 153-158, 1997. MML Identifier: YELLOW_4
    Summary: This paper is the continuation of formalization of \cite{CCL}. The definitions of meet and join of subsets of relational structures are introduced. The properties of these notions are proved.
  22. Artur Kornilowicz. Meet--Continuous Lattices, Formalized Mathematics 6(1), pages 159-167, 1997. MML Identifier: WAYBEL_2
    Summary: The aim of this work is the formalization of Chapter 0 Section 4 of \cite{CCL}. In this paper the definition of meet-continuous lattices is introduced. Theorem 4.2 and Remark 4.3 are proved.
  23. Grzegorz Bancerek. The ``Way-Below'' Relation, Formalized Mathematics 6(1), pages 169-176, 1997. MML Identifier: WAYBEL_3
    Summary: In the paper the ``way-below" relation, in symbols $x \ll y$, is introduced. Some authors prefer the term ``relatively compact" or ``way inside", since in the poset of open sets of a topology it is natural to read $U \ll V$ as ``$U$ is relatively compact in $V$". A compact element of a poset (or an element isolated from below) is defined to be way below itself. So, the compactness in the poset of open sets of a topology is equivalent to the compactness in that topology.\par The article includes definitions, facts and examples 1.1--1.8 presented in \cite[pp.~38--42]{CCL}.