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

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

Bartlomiej Skorulski. Lim-Inf Convergence, Formalized Mathematics 9(2), pages 237-240, 2001. MML Identifier: WAYBEL28
Summary: This work continues the formalization of \cite{CCL}. Theorems from Chapter III, Section 3, pp. 158--159 are proved.
Grzegorz Bancerek, Adam Naumowicz. The Characterization of the Continuity of Topologies, Formalized Mathematics 9(2), pages 241-247, 2001. MML Identifier: WAYBEL29
Summary: Formalization of \cite[pp. 128--130]{CCL}, chapter II, section 4 (4.10, 4.11).
Artur Kornilowicz. Meet Continuous Lattices Revisited, Formalized Mathematics 9(2), pages 249-254, 2001. MML Identifier: WAYBEL30
Summary: This work is a continuation of formalization of \cite{CCL}. Theorems from Chapter III, Section 2, pp. 153--156 are proved.
Robert Milewski. Weights of Continuous Lattices, Formalized Mathematics 9(2), pages 255-259, 2001. MML Identifier: WAYBEL31
Summary: This work is a continuation of formalization of \cite{CCL}. Theorems from Chapter III, Section 4, pp. 170--171 are proved.
Marek Dudzicz. Representation Theorem for Finite Distributive Lattices, Formalized Mathematics 9(2), pages 261-264, 2001. MML Identifier: LATTICE7
Summary: In the article the representation theorem for finite distributive lattice as rings of sets is presented. Auxiliary concepts are introduced. Namely, the concept of the height of an element, the maximal element in a chain, immediate predecessor of an element and ring of sets. Besides the scheme of induction in finite lattice is proved.
Anna Justyna Milewska. The Field of Complex Numbers, Formalized Mathematics 9(2), pages 265-269, 2001. MML Identifier: COMPLFLD
Summary: This article contains the definition and many facts about the field of complex numbers.
Noboru Endou, Katsumi Wasaki, Yasunari Shidama. Integrability of Bounded Total Functions, Formalized Mathematics 9(2), pages 271-274, 2001. MML Identifier: INTEGRA4
Summary: All these results have been obtained by Darboux's theorem in our previous article \cite{INTEGRA3.ABS}. In addition, we have proved the first mean value theorem to Riemann integral.
Yasushi Fuwa, Yoshinori Fujisawa. High-Speed Algorithms for RSA Cryptograms, Formalized Mathematics 9(2), pages 275-279, 2001. MML Identifier: RADIX_2
Summary: In this article, we propose a new high-speed processing method for encoding and decoding the RSA cryptogram that is a kind of public-key cryptogram. This cryptogram is not only used for encrypting data, but also for such purposes as authentication. However, the encoding and decoding processes take a long time because they require a great deal of calculations. As a result, this cryptogram is not suited for practical use. Until now, we proposed a high-speed algorithm of addition using radix-$2^k$ signed-digit numbers and clarified correctness of it (\cite{RADIX_1.ABS}). In this article, we defined two new operations for a high-speed coding and encoding processes on public-key cryptograms based on radix-$2^k$ signed-digit (SD) numbers. One is calculation of $(a*b)$ mod $c$ ($a,b,c$ are natural numbers). Another one is calculation of $(a^b)$ mod $c$ ($a,b,c$ are natural numbers). Their calculations are realized repetition of addition. We propose a high-speed algorithm of their calculations using proposed addition algorithm and clarify the correctness of them. In the first section, we prepared some useful theorems for natural numbers and integers and so on. In the second section, we proved some properties of addition operation using a radix-$2^k$ SD numbers. In the third section, we defined some functions on the relation between a finite sequence of k-SD and a finite sequence of ${\Bbb N}$ and proved some properties about them. In the fourth section, algorithm of calculation of $(a*b)$ mod $c$ based on radix-$2^k$ SD numbers is proposed and its correctness is clarified. In the last section, algorithm of calculation of $(a^b)$ mod $c$ based on radix-$2^k$ SD numbers is proposed and we clarified its correctness.
Noboru Endou, Katsumi Wasaki, Yasunari Shidama. Definition of Integrability for Partial Functions from $\Bbb R$ to $\Bbb R$ and Integrability for Continuous Functions, Formalized Mathematics 9(2), pages 281-284, 2001. MML Identifier: INTEGRA5
Summary: In this article, we defined the Riemann definite integral of partial function from ${\Bbb R}$ to ${\Bbb R}$. Then we have proved the integrability for the continuous function and differentiable function. Moreover, we have proved an elementary theorem of calculus.
Noboru Endou, Katsumi Wasaki, Yasunari Shidama. Introduction to Several Concepts of Convexity and Semicontinuity for Function from $\Bbb R$ to $\Bbb R$, Formalized Mathematics 9(2), pages 285-289, 2001. MML Identifier: RFUNCT_4
Summary: This article is an introduction to convex analysis. In the beginning, we have defined the concept of strictly convexity and proved some basic properties between convexity and strictly convexity. Moreover, we have defined concepts of other convexity and semicontinuity, and proved their basic properties.
Andrzej Trybulec, Piotr Rudnicki, Artur Kornilowicz. Standard Ordering of Instruction Locations, Formalized Mathematics 9(2), pages 291-301, 2001. MML Identifier: AMISTD_1
Summary:
Artur Kornilowicz. On the Composition of Macro Instructions of Standard Computers, Formalized Mathematics 9(2), pages 303-316, 2001. MML Identifier: AMISTD_2
Summary:
Artur Kornilowicz. The Properties of Instructions of SCM over Ring, Formalized Mathematics 9(2), pages 317-322, 2001. MML Identifier: SCMRING3
Summary:
Josef Urban. Basic Facts about Inaccessible and Measurable Cardinals, Formalized Mathematics 9(2), pages 323-329, 2001. MML Identifier: CARD_FIL
Summary: Inaccessible, strongly inaccessible and measurable cardinals are defined, and it is proved that a measurable cardinal is strongly inaccessible. Filters on sets are defined, some facts related to the section about cardinals are proved. Existence of the Ulam matrix on non-limit cardinals is proved.
Christoph Schwarzweller, Andrzej Trybulec. The Evaluation of Multivariate Polynomials, Formalized Mathematics 9(2), pages 331-338, 2001. MML Identifier: POLYNOM2
Summary:
Robert Milewski. The Ring of Polynomials, Formalized Mathematics 9(2), pages 339-346, 2001. MML Identifier: POLYNOM3
Summary:
Xiquan Liang. Solving Roots of Polynomial Equations of Degree 2 and 3 with Real Coefficients, Formalized Mathematics 9(2), pages 347-350, 2001. MML Identifier: POLYEQ_1
Summary: In this paper, we describe the definition of the first, second, and third degree algebraic equations and their properties. In Section 1, we defined the simple first-degree and second-degree (quadratic) equation and discussed the relation between the roots of each equation and their coefficients. Also, we clarified the form of the root within the range of real numbers. Furthermore, the extraction of the root using the discriminant of equation is clarified. In Section 2, we defined the third-degree (cubic) equation and clarified the relation between the three roots of this equation and its coefficient. Also, the form of these roots for various conditions is discussed. This solution is known as the Cardano solution.
Takashi Mitsuishi, Noboru Endou, Yasunari Shidama. The Concept of Fuzzy Set and Membership Function and Basic Properties of Fuzzy Set Operation, Formalized Mathematics 9(2), pages 351-356, 2001. MML Identifier: FUZZY_1
Summary: This article introduces the fuzzy theory. At first, the definition of fuzzy set characterized by membership function is described. Next, definitions of empty fuzzy set and universal fuzzy set and basic operations of these fuzzy sets are shown. At last, exclusive sum and absolute difference which are special operation are introduced.
Takashi Mitsuishi, Katsumi Wasaki, Yasunari Shidama. Basic Properties of Fuzzy Set Operation and Membership Function, Formalized Mathematics 9(2), pages 357-362, 2001. MML Identifier: FUZZY_2
Summary: This article introduces the fuzzy theory. The definition of the difference set, algebraic product and algebraic sum of fuzzy set is shown. In addition, basic properties of those operations are described. Basic properties of fuzzy set are a~little different from those of crisp set.
Anna Justyna Milewska. The Hahn Banach Theorem in the Vector Space over the Field of Complex Numbers, Formalized Mathematics 9(2), pages 363-371, 2001. MML Identifier: HAHNBAN1
Summary: This article contains the Hahn Banach theorem in the vector space over the field of complex numbers.
Bartlomiej Skorulski. The Tichonov Theorem, Formalized Mathematics 9(2), pages 373-376, 2001. MML Identifier: YELLOW17
Summary:
Ewa Grdzka. On the Order-consistent Topology of Complete and Uncomplete Lattices, Formalized Mathematics 9(2), pages 377-382, 2001. MML Identifier: WAYBEL32
Summary: This paper is a continuation of the formalisation of \cite{CCL} pp.~108--109. Order-consistent and upper topologies are defined. The theorem that the Scott and the upper topologies are order-consistent is proved. Remark 1.4 and example 1.5(2) are generalized for proving this theorem.
Adam Naumowicz. On Segre's Product of Partial Line Spaces, Formalized Mathematics 9(2), pages 383-390, 2001. MML Identifier: PENCIL_1
Summary: In this paper the concept of partial line spaces is presented. We also construct the Segre's product for a family of partial line spaces indexed by an arbitrary nonempty set.
Robert Milewski. The Evaluation of Polynomials, Formalized Mathematics 9(2), pages 391-395, 2001. MML Identifier: POLYNOM4
Summary:
Jing-Chao Chen. The Construction and Computation of While-Loop Programs for SCMPDS, Formalized Mathematics 9(2), pages 397-405, 2001. MML Identifier: SCMPDS_8
Summary: This article defines two while-loop statements on SCMPDS, i.e. ``while$<$0'' and ``while$>$0'', which resemble the while-statements of the common high language such as C. We previously presented a number of tricks for computing while-loop statements on SCMFSA, e.g. step-while. However, after inspecting a few realistic examples, we found that they are neither very useful nor of generalization. To cover much more computation cases of while-loop statements, we generalize the computation model of while-loop statements, based on the principle of Hoare's axioms on the verification of programs.
Jing-Chao Chen. Insert Sort on SCMPDS, Formalized Mathematics 9(2), pages 407-412, 2001. MML Identifier: SCPISORT
Summary: The goal of this article is to examine the effectiveness of ``for-loop'' and ``while-loop'' statements on SCMPDS by insert sort. In this article, first of all, we present an approach to compute the execution result of ``for-loop'' program by ``loop-invariant'', based on Hoare's axioms for program verification. Secondly, we extend the fundamental properties of the finite sequence and complex instructions of SCMPDS. Finally, we prove the correctness of the insert sort program described in the article.
Jing-Chao Chen. Quick Sort on SCMPDS, Formalized Mathematics 9(2), pages 413-418, 2001. MML Identifier: SCPQSORT
Summary: Proving the correctness of quick sort is much more complicated than proving the correctness of the insert sort. Its difficulty is determined mainly by the following points: \begin{itemize} \item Quick sort needs to use a push-down stack. \item It contains three nested loops. \item A subroutine of this algorithm, ``Partition'', has no loop-invariant. \end{itemize} This means we cannot justify the correctness of the ``Partition'' subroutine by the Hoare's axiom on program verification. This article is organized as follows. First, we present several fundamental properties of ``while'' program and finite sequence. Second, we define the ``Partition'' subroutine on SCMPDS, the task of which is to split a sequence into a smaller and a larger subsequence. The definition of quick sort on SCMPDS follows. Finally, we describe the basic property of the ``Partition'' and quick sort, and prove their correctness.
Jing-Chao Chen. Justifying the Correctness of the Fibonacci Sequence and the Euclide Algorithm by Loop-Invariant, Formalized Mathematics 9(2), pages 419-427, 2001. MML Identifier: SCPINVAR
Summary: If a loop-invariant exists in a loop program, computing its result by loop-invariant is simpler and easier than computing its result by the inductive method. For this purpose, the article describes the premise and the final computation result of the program such as ``while$<$0'', ``while$>$0'', ``while$<>$0'' by loop-invariant. To test the effectiveness of the computation method given in this article, by using loop-invariant of the loop programs mentioned above, we justify the correctness of the following three examples: Summing $n$ integers (used for testing ``while$>$0''), Fibonacci sequence (used for testing ``while$<$0''), Greatest Common Divisor, i.e. Euclide algorithm (used for testing ``while$<>$0'').
Marta Pruszynska, Marek Dudzicz. On the Isomorphism between Finite Chains, Formalized Mathematics 9(2), pages 429-430, 2001. MML Identifier: ORDERS_4
Summary:
Mariusz Lapinski. The J\'onsson Theorem about the Representation of Modular Lattices, Formalized Mathematics 9(2), pages 431-438, 2001. MML Identifier: LATTICE8
Summary: Formalization of \cite[pp. 192--199]{Gratzer}, chapter IV. Partition Lattices, theorem 8.