Formalized Mathematics    (ISSN 1426-2630)
Volume 7, Number 2 (1998): pdf, ps, dvi.
  1. Grzegorz Bancerek. The Lawson Topology, Formalized Mathematics 7(2), pages 163-168, 1998. MML Identifier: WAYBEL19
    Summary: The article includes definitions, lemmas and theorems 1.1--1.7, 1.9, 1.10 presented in Chapter III of \cite[pp.~142--146]{CCL}.
  2. Piotr Rudnicki. Kernel Projections and Quotient Lattices, Formalized Mathematics 7(2), pages 169-175, 1998. MML Identifier: WAYBEL20
    Summary: This article completes the Mizar formalization of Chapter I, Section 2 from \cite{CCL}. After presenting some preliminary material (not all of which is later used in this article) we give the proof of theorem 2.7 (i), p.60. We do not follow the hint from \cite{CCL} suggesting using the equations 2.3, p. 58. The proof is taken directly from the definition of continuous lattice. The goal of the last section is to prove the correspondence between the set of all congruences of a continuous lattice and the set of all kernel operators of the lattice which preserve directed sups (Corollary 2.13).
  3. Grzegorz Bancerek. Lawson Topology in Continuous Lattices, Formalized Mathematics 7(2), pages 177-184, 1998. MML Identifier: WAYBEL21
    Summary: The article completes Mizar formalization of Section 1 of Chapter III of \cite[pp.~145--147]{CCL}.
  4. Piotr Rudnicki. Representation Theorem for Free Continuous Lattices, Formalized Mathematics 7(2), pages 185-188, 1998. MML Identifier: WAYBEL22
    Summary: We present the Mizar formalization of theorem 4.17, Chapter I from \cite{CCL}: a free continuous lattice with $m$ generators is isomorphic to the lattice of filters of $2^X$ ($\overline{\overline{X}} = m$) which is freely generated by $\{\uparrow x : x \in X\}$ (the set of ultrafilters).
  5. Yatsuka Nakamura, Piotr Rudnicki. Oriented Chains, Formalized Mathematics 7(2), pages 189-192, 1998. MML Identifier: GRAPH_4
    Summary: In \cite{GRAPH_2.ABS} we introduced a number of notions about vertex sequences associated with undirected chains of edges in graphs. In this article, we introduce analogous concepts for oriented chains and use them to prove properties of cutting and glueing of oriented chains, and the existence of a simple oriented chain in an oriented chain.
  6. Yatsuka Nakamura. Graph Theoretical Properties of Arcs in the Plane and Fashoda Meet Theorem, Formalized Mathematics 7(2), pages 193-201, 1998. MML Identifier: JGRAPH_1
    Summary: We define a graph on an abstract set, edges of which are pairs of any two elements. For any finite sequence of a plane, we give a definition of nodic, which means that edges by a finite sequence are crossed only at terminals. If the first point and the last point of a finite sequence differs, simpleness as a chain and nodic condition imply unfoldedness and s.n.c. condition. We generalize Goboard Theorem, proved by us before, to a continuous case. We call this Fashoda Meet Theorem, which was taken from Fashoda incident of 100 years ago.
  7. Yasushi Fuwa, Yoshinori Fujisawa. Algebraic Group on Fixed-length Bit Integer and its Adaptation to IDEA Cryptography, Formalized Mathematics 7(2), pages 203-215, 1998. MML Identifier: IDEA_1
    Summary: In this article, an algebraic group on fixed-length bit integer is constructed and its adaptation to IDEA cryptography is discussed. In the first section, we present some selected theorems on integers. In the continuous section, we construct an algebraic group on fixed-length integer. In the third section, operations of IDEA Cryptograms are defined and some theorems on these operations are proved. In the fourth section, we define sequences of IDEA Cryptogram's operations and discuss their nature. Finally, we make a model of IDEA Cryptogram and prove that the ciphertext that is encrypted by IDEA encryption algorithm can be decrypted by the IDEA decryption algorithm.
  8. Artur Kornilowicz. The Definition and Basic Properties of Topological Groups, Formalized Mathematics 7(2), pages 217-225, 1998. MML Identifier: TOPGRP_1
    Summary:
  9. Adam Naumowicz, Agnieszka Julia Marasik. The Correspondence Between Lattices of Subalgebras of Universal Algebras and Many Sorted Algebras, Formalized Mathematics 7(2), pages 227-231, 1998. MML Identifier: MSSUBLAT
    Summary: The main goal of this paper is to show some properties of subalgebras of universal algebras and many sorted algebras, and then the isomorphic correspondence between lattices of such subalgebras.
  10. Christoph Schwarzweller. Introduction to Concept Lattices, Formalized Mathematics 7(2), pages 233-241, 1998. MML Identifier: CONLAT_1
    Summary: In this paper we give Mizar formalization of concept lattices. Concept lattices stem from the so-called formal concept analysis --- a part of applied mathematics that brings mathematical methods into the field of data analysis and knowledge processing. Our approach follows the one given in \cite{GanterWille}.
  11. Shunichi Kobayashi, Kui Jia. A Theory of Partitions. Part I, Formalized Mathematics 7(2), pages 243-247, 1998. MML Identifier: PARTIT1
    Summary: In this paper, we define join and meet operations between partitions. The properties of these operations are proved. Then we introduce the correspondence between partitions and equivalence relations which preserve join and meet operations. The properties of these relationships are proved.
  12. Shunichi Kobayashi, Kui Jia. A Theory of Boolean Valued Functions and Partitions, Formalized Mathematics 7(2), pages 249-254, 1998. MML Identifier: BVFUNC_1
    Summary: In this paper, we define Boolean valued functions. Some of their algebraic properties are proved. We also introduce and examine the infimum and supremum of Boolean valued functions and their properties. In the last section, relations between Boolean valued functions and partitions are discussed.
  13. Yuguang Yang, Yasunari Shidama. Trigonometric Functions and Existence of Circle Ratio, Formalized Mathematics 7(2), pages 255-263, 1998. MML Identifier: SIN_COS
    Summary: In this article, we defined {\em sinus} and {\em cosine} as the real part and the imaginary part of the exponential function on complex, and also give their series expression. Then we proved the differentiablity of {\em sinus}, {\em cosine} and the exponential function of real. Finally, we showed the existence of the circle ratio, and some formulas of {\em sinus}, {\em cosine}.
  14. Andrzej Trybulec, Yatsuka Nakamura. Some Properties of Special Polygonal Curves, Formalized Mathematics 7(2), pages 265-272, 1998. MML Identifier: SPRECT_3
    Summary: In the paper some auxiliary theorems are proved, needed in the proof of the second part of the Jordan curve theorem for special polygons. They deal mostly with characteristic points of plane non empty compacts introduced in \cite{PSCOMP_1.ABS}, operation {\em mid} introduced in \cite{JORDAN3.ABS} and the predicate ``$f$ is in the area of $g$'' ($f$ and $g$ : finite sequences of points of the plane) introduced in \cite{SPRECT_2.ABS}.
  15. Robert Milewski. Real Linear-Metric Space and Isometric Functions, Formalized Mathematics 7(2), pages 273-277, 1998. MML Identifier: VECTMETR
    Summary:
  16. Artur Kornilowicz. Introduction to Meet-Continuous Topological Lattices, Formalized Mathematics 7(2), pages 279-283, 1998. MML Identifier: YELLOW13
    Summary:
  17. Robert Milewski. Bases of Continuous Lattices, Formalized Mathematics 7(2), pages 285-294, 1998. MML Identifier: WAYBEL23
    Summary: The article is a Mizar formalization of \cite[168--169]{CCL}. We show definition and fundamental theorems from theory of basis of continuous lattices.
  18. Artur Kornilowicz. The Construction of \SCM over Ring, Formalized Mathematics 7(2), pages 295-300, 1998. MML Identifier: SCMRING1
    Summary:
  19. Artur Kornilowicz. The Basic Properties of \SCM over Ring, Formalized Mathematics 7(2), pages 301-305, 1998. MML Identifier: SCMRING2
    Summary:
  20. Shunichi Kobayashi, Yatsuka Nakamura. A Theory of Boolean Valued Functions and Quantifiers with Respect to Partitions, Formalized Mathematics 7(2), pages 307-312, 1998. MML Identifier: BVFUNC_2
    Summary: In this paper, we define the coordinate of partitions. We also introduce the universal quantifier and the existential quantifier of Boolean valued functions with respect to partitions. Some predicate calculus formulae containing such quantifiers are proved. Such a theory gives a discussion of semantics to usual predicate logic.
  21. Shunichi Kobayashi, Yatsuka Nakamura. Predicate Calculus for Boolean Valued Functions. Part I, Formalized Mathematics 7(2), pages 313-315, 1998. MML Identifier: BVFUNC_3
    Summary: In this paper, we have proved some elementary predicate calculus formulae containing the quantifiers of Boolean valued functions with respect to partitions. Such a theory is an analogy of usual predicate logic.
  22. Yoshinori Fujisawa, Yasushi Fuwa, Hidetaka Shimizu. Public-Key Cryptography and Pepin's Test for the Primality of Fermat Numbers, Formalized Mathematics 7(2), pages 317-321, 1998. MML Identifier: PEPIN
    Summary: In this article, we have proved the correctness of the Public-Key Cryptography and the Pepin's Test for the Primality of Fermat Numbers ($F(n) = 2^{2^n}+1$). It is a very important result in the IDEA Cryptography that F(4) is a prime number. At first, we prepared some useful theorems. Then, we proved the correctness of the Public-Key Cryptography. Next, we defined the Order's function and proved some properties. This function is very important in the proof of the Pepin's Test. Next, we proved some theorems about the Fermat Number. And finally, we proved the Pepin's Test using some properties of the Order's Function. And using the obtained result we have proved that F(1), F(2), F(3) and F(4) are prime number.
  23. Adam Grabowski. Lattice of Substitutions is a Heyting Algebra, Formalized Mathematics 7(2), pages 323-327, 1998. MML Identifier: HEYTING2
    Summary: