Formalized Mathematics    (ISSN 1426-2630)
Volume 8, Number 1 (1999): pdf, ps, dvi.
  1. Yatsuka Nakamura, Andrzej Trybulec, Czeslaw Bylinski. Bounded Domains and Unbounded Domains, Formalized Mathematics 8(1), pages 1-13, 1999. MML Identifier: JORDAN2C
    Summary: First, notions of inside components and outside components are introduced for any subset of $n$-dimensional Euclid space. Next, notions of the bounded domain and the unbounded domain are defined using the above components. If the dimension is larger than 1, and if a subset is bounded, a unbounded domain of the subset coincides with an outside component (which is unique) of the subset. For a sphere in $n$-dimensional space, the similar fact is true for a bounded domain. In 2 dimensional space, any rectangle also has such property. We discussed relations between the Jordan property and the concept of boundary, which are necessary to find points in domains near a curve. In the last part, we gave the sufficient criterion for belonging to the left component of some clockwise oriented finite sequences.
  2. Andrzej Trybulec. Rotating and Reversing, Formalized Mathematics 8(1), pages 15-20, 1999. MML Identifier: REVROT_1
    Summary: Quite a number of lemmas for the Jordan curve theorem, as yet in the case of the special polygonal curves, have been proved. By ``special" we mean, that it is a polygonal curve with edges parallel to axes and actually the lemmas have been proved, mostly, for the triangulations i.e. for finite sequences that define the curve. Moreover some of the results deal only with a special case: \begin{itemize} \item[-] finite sequences are clockwise oriented, \item[-] the first member of the sequence is the member with the lowest ordinate among those with the highest abscissa (N-min $f,$ where $f$ is a finite sequence, in the Mizar jargon). \end{itemize} In the change of the orientation one has to reverse the sequence (the operation introduced in \cite{FINSEQ_5.ABS}) and to change the second restriction one has to rotate the sequence (the operation introduced in \cite{FINSEQ_6.ABS}). The goal of the paper is to prove, mostly simple, facts about the relationship between properties and attributes of the finite sequence and its rotation (similar results about reversing had been proved in \cite{FINSEQ_5.ABS}). Some of them deal with recounting parameters, others with properties that are invariant under the rotation. We prove also that the finite sequence is either clockwise oriented or it is such after reversing. Everything is proved for the so called standard finite sequences, which means that if a point belongs to it then every point with the same abscissa or with the same ordinate, that belongs to the polygon, belongs also to the finite sequence. It does not seem that this requirement causes serious technical obstacles.
  3. Andrzej Trybulec, Yatsuka Nakamura. On the Components of the Complement of a Special Polygonal Curve, Formalized Mathematics 8(1), pages 21-23, 1999. MML Identifier: SPRECT_4
    Summary: By the special polygonal curve we meana simple closed curve, that is a polygone and moreover has edges parallel to axes. We continue the formalization of the Takeuti-Nakamura proof \cite{TAKE-NAKA} of the Jordan curve theorem. In the paper we prove that the complement of the special polygonal curve consists of at least two components. With the theorem which has at most two components we completed the theorem that a special polygonal curve cuts the plane into exactly two components.
  4. Czeslaw Bylinski. Gauges, Formalized Mathematics 8(1), pages 25-27, 1999. MML Identifier: JORDAN8
    Summary:
  5. Christoph Schwarzweller. The Ring of Integers, Euclidean Rings and Modulo Integers, Formalized Mathematics 8(1), pages 29-34, 1999. MML Identifier: INT_3
    Summary: In this article we introduce the ring of Integers, Euclidean rings and Integers modulo $p$. In particular we prove that the Ring of Integers is an Euclidean ring and that the Integers modulo $p$ constitutes a field if and only if $p$ is a prime.
  6. Yatsuka Nakamura. Logic Gates and Logical Equivalence of Adders, Formalized Mathematics 8(1), pages 35-45, 1999. MML Identifier: GATE_1
    Summary: This is an experimental article which shows that logical correctness of logic circuits can be easily proven by the Mizar system. First, we define the notion of logic gates. Then we prove that an MSB carry of `4 Bit Carry Skip Adder' is equivalent to an MSB carry of a normal 4 bit adder. In the last theorem, we show that outputs of the `4 Bit Carry Look Ahead Adder' are equivalent to the corresponding outputs of the normal 4 bits adder. The policy here is as follows: when the functional (semantic) correctness of a system is already proven, and the correspondence of the system to a (normal) logic circuit is given, it is enough to prove the correctness of the new circuit if we only prove the logical equivalence between them. Although the article is very fundamental (it contains few environment files), it can be applied to real problems. The key of the method introduced here is to put the specification of the logic circuit into the Mizar propositional formulae, and to use the strong inference ability of the Mizar checker. The proof is done formally so that the automation of the proof writing is possible. Even in the 5.3.07 version of Mizar, it can handle a formulae of more than 100 lines, and a formula which contains more than 100 variables. This means that the Mizar system is enough to prove logical correctness of middle scaled logic circuits.
  7. Bartlomiej Skorulski. The Sequential Closure Operator in Sequential and Frechet Spaces, Formalized Mathematics 8(1), pages 47-54, 1999. MML Identifier: FRECHET2
    Summary:
  8. Adam Grabowski. Properties of the Product of Compact Topological Spaces, Formalized Mathematics 8(1), pages 55-59, 1999. MML Identifier: BORSUK_3
    Summary:
  9. Artur Kornilowicz. Compactness of the Bounded Closed Subsets of $\calE^2_\rmT$, Formalized Mathematics 8(1), pages 61-68, 1999. MML Identifier: TOPREAL6
    Summary: This paper contains theorems which describe the correspondence between topological properties of real numbers subsets introduced in \cite{RCOMP_1.ABS} and introduced in \cite{PRE_TOPC.ABS}, \cite{COMPTS_1.ABS}. We also show the homeomorphism between the cartesian product of two $R^1$ and ${\cal E}^2_{\rm T}$. The compactness of the bounded closed subset of ${\cal E}^2_{\rm T}$ is proven.
  10. Adam Grabowski. Hilbert Positive Propositional Calculus, Formalized Mathematics 8(1), pages 69-72, 1999. MML Identifier: HILBERT1
    Summary:
  11. Artur Kornilowicz. Homeomorphism between [:$\calE^i_\rmT, \calE^j_\rmT$:] and $\calE^i+j_\rmT$, Formalized Mathematics 8(1), pages 73-76, 1999. MML Identifier: TOPREAL7
    Summary: In this paper we introduce the cartesian product of two metric spaces. As the distance between two points in the product we take maximal distance between coordinates of these points. In the main theorem we show the homeomorphism between [:${\cal E}^i_{\rm T}, {\cal E}^j_{\rm T}$:] and ${\cal E}^{i+j}_{\rm T}$.
  12. Katsumi Wasaki, Noboru Endou. Full Subtracter Circuit. Part I, Formalized Mathematics 8(1), pages 77-81, 1999. MML Identifier: FSCIRC_1
    Summary: We formalize the concept of the full subtracter circuit, define the structures of bit subtract/borrow units for binary operations, and prove the stability of the circuit.
  13. Yuguang Yang, Katsumi Wasaki, Yasushi Fuwa, Yatsuka Nakamura. Correctness of Binary Counter Circuits, Formalized Mathematics 8(1), pages 83-85, 1999. MML Identifier: GATE_2
    Summary: This article introduces the verification of the correctness for the operations and the specification of the 3-bit counter. Both cases: without reset input and with reset input are considered. The proof was proposed by Y. Nakamura in \cite{GATE_1.ABS}.
  14. Yuguang Yang, Katsumi Wasaki, Yasushi Fuwa, Yatsuka Nakamura. Correctness of Johnson Counter Circuits, Formalized Mathematics 8(1), pages 87-91, 1999. MML Identifier: GATE_3
    Summary: This article introduces the verification of the correctness for the operations and the specification of the Johnson counter. We formalize the concepts of 2-bit, 3-bit and 4-bit Johnson counter circuits with a reset input, and define the specification of the state transitions without the minor loop.
  15. Noboru Endou, Artur Kornilowicz. The Definition of the Riemann Definite Integral and some Related Lemmas, Formalized Mathematics 8(1), pages 93-102, 1999. MML Identifier: INTEGRA1
    Summary: This article introduces the Riemann definite integral on the closed interval of real. We present the definitions and related lemmas of the closed interval. We formalize the concept of the Riemann definite integral and the division of the closed interval of real, and prove the additivity of the integral.
  16. Takashi Mitsuishi, Yuguang Yang. Properties of the Trigonometric Function, Formalized Mathematics 8(1), pages 103-106, 1999. MML Identifier: SIN_COS2
    Summary: This article introduces the monotone increasing and the monotone decreasing of {\em sinus} and {\em cosine}, and definitions of hyperbolic {\em sinus}, hyperbolic {\em cosine} and hyperbolic {\em tangent}, and some related formulas about them.
  17. Shunichi Kobayashi, Yatsuka Nakamura. Predicate Calculus for Boolean Valued Functions. Part II, Formalized Mathematics 8(1), pages 107-109, 1999. MML Identifier: BVFUNC_4
    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.
  18. Shunichi Kobayashi, Yatsuka Nakamura. Propositional Calculus for Boolean Valued Functions. Part I, Formalized Mathematics 8(1), pages 111-113, 1999. MML Identifier: BVFUNC_5
    Summary: In this paper, we have proved some elementary propositional calculus formulae for Boolean valued functions.
  19. Shunichi Kobayashi, Yatsuka Nakamura. Propositional Calculus for Boolean Valued Functions. Part II, Formalized Mathematics 8(1), pages 115-117, 1999. MML Identifier: BVFUNC_6
    Summary: In this paper, we have proved some elementary propositional calculus formulae for Boolean valued functions.
  20. Jing-Chao Chen. Insert Sort on \SCMFSA, Formalized Mathematics 8(1), pages 119-127, 1999. MML Identifier: SCMISORT
    Summary: This article describes the insert sorting algorithm using macro instructions such as if-Macro (conditional branch macro instructions), for-loop macro instructions and While-Macro instructions etc. From the viewpoint of initialization, we generalize the halting and computing problem of the While-Macro. Generally speaking, it is difficult to judge whether the While-Macro is halting or not by way of loop inspection. For this reason, we introduce a practical and simple method, called body-inspection. That is, in many cases, we can prove the halting problem of the While-Macro by only verifying the nature of the body of the While-Macro, rather than the While-Macro itself. In fact, we have used this method in justifying the halting of the insert sorting algorithm. Finally, we prove that the insert sorting algorithm given in the article is autonomic and its computing result is correct.
  21. Yuguang Yang, Katsumi Wasaki, Yasushi Fuwa, Yatsuka Nakamura. Correctness of a Cyclic Redundancy Check Code Generator, Formalized Mathematics 8(1), pages 129-132, 1999. MML Identifier: GATE_4
    Summary: We prove the correctness of the division circuit and the CRC (cyclic redundancy checks) circuit by verifying the contents of the register after one shift. Circuits with 12-bit register and 16-bit register are taken as examples. All the proofs are done formally.
  22. Andrzej Trybulec. Defining by Structural Induction in the Positive Propositional Language, Formalized Mathematics 8(1), pages 133-137, 1999. MML Identifier: HILBERT2
    Summary: The main goal of the paper consists in proving schemes for defining by structural induction in the language defined by Adam Grabowski \cite{HILBERT1.ABS}. The article consists of four parts. Besides the preliminaries where we prove some simple facts still missing in the library, they are: \item{-} ``About the language'' in which the consequences of the fact that the algebra of formulae is free are formulated, \item{-} ``Defining by structural induction'' in which two schemes are proved, \item{-} ``The tree of the subformulae'' in which a scheme proved in the previous section is used to define the tree of subformulae; also some simple facts about the tree are proved.
  23. Czeslaw Bylinski. Some Properties of Cells on Go-Board, Formalized Mathematics 8(1), pages 139-146, 1999. MML Identifier: GOBRD13
    Summary:
  24. Shunichi Kobayashi. Propositional Calculus for Boolean Valued Functions. Part III, Formalized Mathematics 8(1), pages 147-148, 1999. MML Identifier: BVFUNC_7
    Summary: In this paper, we have proved some elementary propositional calculus formulae for Boolean valued functions.
  25. Shunichi Kobayashi. Propositional Calculus for Boolean Valued Functions. Part IV, Formalized Mathematics 8(1), pages 149-150, 1999. MML Identifier: BVFUNC_8
    Summary: In this paper, we have proved some elementary propositional calculus formulae for Boolean valued functions.
  26. Akihiko Uchibori, Noboru Endou. Basic Properties of Genetic Algorithm, Formalized Mathematics 8(1), pages 151-160, 1999. MML Identifier: GENEALG1
    Summary: We defined the set of the gene, the space treated by the genetic algorithm and the individual of the space. Moreover, we defined some genetic operators such as one point crossover and two points crossover, and the validity of many characters were proven.
  27. Shunichi Kobayashi. Propositional Calculus for Boolean Valued Functions. Part V, Formalized Mathematics 8(1), pages 161-162, 1999. MML Identifier: BVFUNC_9
    Summary: In this paper, we have proved some elementary propositional calculus formulae for Boolean valued functions.
  28. Artur Kornilowicz. Properties of Left and Right Components, Formalized Mathematics 8(1), pages 163-168, 1999. MML Identifier: GOBRD14
    Summary:
  29. Christoph Schwarzweller. Noetherian Lattices, Formalized Mathematics 8(1), pages 169-174, 1999. MML Identifier: LATTICE6
    Summary: In this article we define noetherian and co-noetherian lattices and show how some properties concerning upper and lower neighbours, irreducibility and density can be improved when restricted to these kinds of lattices. In addition we define atomic lattices.
  30. Jing-Chao Chen. A Small Computer Model with Push-Down Stack, Formalized Mathematics 8(1), pages 175-182, 1999. MML Identifier: SCMPDS_1
    Summary: The SCMFSA computer can prove the correctness of many algorithms. Unfortunately, it cannot prove the correctness of recursive algorithms. For this reason, this article improves the SCMFSA computer and presents a Small Computer Model with Push-Down Stack (called SCMPDS for short). In addition to conventional arithmetic and "goto" instructions, we increase two new instructions such as "return" and "save instruction-counter" in order to be able to design recursive programs.
  31. Jing-Chao Chen. The SCMPDS Computer and the Basic Semantics of its Instructions, Formalized Mathematics 8(1), pages 183-191, 1999. MML Identifier: SCMPDS_2
    Summary: The article defines the SCMPDS computer and its instructions. The SCMPDS computer consists of such instructions as conventional arithmetic, ``goto'', ``return'' and ``save instruction-counter'' (``saveIC'' for short). The address used in the ``goto'' instruction is an offset value rather than a pointer in the standard sense. Thus, we don't define halting instruction directly but define it by ``goto 0'' instruction. The ``saveIC'' and ``return'' equal almost call and return statements in the usual high programming language. Theoretically, the SCMPDS computer can implement all algorithms described by the usual high programming language including recursive routine. In addition, we describe the execution semantics and halting properties of each instruction.
  32. Jing-Chao Chen. Computation and Program Shift in the SCMPDS Computer, Formalized Mathematics 8(1), pages 193-199, 1999. MML Identifier: SCMPDS_3
    Summary: A finite partial state is said to be autonomic if the computation results in any two states containing it are same on its domain. On the basis of this definition, this article presents some computation results about autonomic finite partial states of the SCMPDS computer. Because the instructions of the SCMPDS computer are more complicated than those of the SCMFSA computer, the results given by this article are weaker than those reported previously by the article on the SCMFSA computer. The second task of this article is to define the notion of program shift. The importance of this notion is that the computation of some program blocks can be simplified by shifting a program block to the initial position.
  33. Jing-Chao Chen. The Construction and Shiftability of Program Blocks for SCMPDS, Formalized Mathematics 8(1), pages 201-210, 1999. MML Identifier: SCMPDS_4
    Summary: In this article, a program block is defined as a finite sequence of instructions stored consecutively on initial positions. Based on this definition,any program block with more than two instructions can be viewed as the combination of two smaller program blocks. To describe the computation of a program block by the result of its two sub-blocks, we introduce the notions of paraclosed, parahalting, valid, and shiftable, the meaning of which may be stated as follows: \begin{itemize} \item[-] a program is paraclosed if and only if any state containing it is closed, \item[-] a program is parahalting if and only if any state containing it is halting, \item[-] in a program block, a jumping instruction is valid if its jumping offset is valid, \item[-] a program block is shiftable if it does not contain any return and saveIC instructions, and each instruction in it is valid. \end{itemize} When a program block is shiftable, its computing result does not depend on its storage position.
  34. Jing-Chao Chen. Computation of Two Consecutive Program Blocks for SCMPDS, Formalized Mathematics 8(1), pages 211-217, 1999. MML Identifier: SCMPDS_5
    Summary: In this article, a program block without halting instructions is called No-StopCode program block. If a program consists of two blocks, where the first block is parahalting (i.e. halt for all states) and No-StopCode, and the second block is parahalting and shiftable, it can be computed by combining the computation results of the two blocks. For a program which consists of a instruction and a block, we obtain a similar conclusion. For a large amount of programs, the computation method given in the article is useful, but it is not suitable to recursive programs.
  35. Jing-Chao Chen. The Construction and Computation of Conditional Statements for SCMPDS, Formalized Mathematics 8(1), pages 219-234, 1999. MML Identifier: SCMPDS_6
    Summary: We construct conditional statements like the usual high level program language by program blocks of SCMPDS. Roughly speaking, the article justifies such a fact that when the condition of a conditional statement is true (false), and the true (false) branch is shiftable, parahalting and does not contain any halting instruction, and the false branch is shiftable, then it is halting and its computation result equals that of the true (false) branch. The parahalting means some program halts for all states, this is strong condition. For this reason, we introduce the notions of "is\_closed\_on" and "is\_halting\_on". The predicate "A is\_closed\_on B" denotes program A is closed on state B, and "A is\_halting\_on B" denotes program A is halting on state B. We obtain a similar theorem to the above fact by replacing parahalting by "is\_closed\_on" and "is\_halting\_on".