Formalized Mathematics    (ISSN 1426-2630)
Volume 10, Number 1 (2002): pdf, ps, dvi.

1. Yatsuka Nakamura. Fan Homeomorphisms in the Plane, Formalized Mathematics 10(1), pages 1-19, 2002. MML Identifier: JGRAPH_4
   Summary: We will introduce four homeomorphisms (Fan morphisms) which give spoke-like distortion to the plane. They do not change the norms of vectors and preserve halfplanes invariant. These morphisms are used to regulate placement of points on the circle.

   ---

2. Yatsuka Nakamura. Half Open Intervals in Real Numbers, Formalized Mathematics 10(1), pages 21-22, 2002. MML Identifier: RCOMP_2
   Summary: Left and right half open intervals in the real line are defined. Their properties are investigated. A class of all finite union of such intervals are, in a sense, closed by operations of union, intersection and the difference of sets.

   ---

3. Adam Naumowicz, Robert Milewski. Some Remarks on Clockwise Oriented Sequences on Go-boards, Formalized Mathematics 10(1), pages 23-27, 2002. MML Identifier: JORDAN1I
   Summary: The main goal of this paper is to present alternative characterizations of clockwise oriented sequences on Go-boards.

   ---

4. Gilbert Lee, Piotr Rudnicki. Dickson's Lemma, Formalized Mathematics 10(1), pages 29-37, 2002. MML Identifier: DICKSON
   Summary: We present a Mizar formalization of the proof of Dickson's lemma following \cite{Becker93}, chapters 4.2 and 4.3.

   ---

5. Gilbert Lee, Piotr Rudnicki. On Ordering of Bags, Formalized Mathematics 10(1), pages 39-46, 2002. MML Identifier: BAGORDER
   Summary: We present a Mizar formalization of chapter 4.4 of \cite{Becker93} devoted to special orderings in additive monoids to be used for ordering terms in multivariate polynomials. We have extended the treatment to the case of infinite number of variables. It turns out that in such case admissible orderings are not necessarily well orderings.

   ---

6. Grzegorz Bancerek, Shin'nosuke Yamaguchi, Yasunari Shidama. Combining of Multi Cell Circuits, Formalized Mathematics 10(1), pages 47-64, 2002. MML Identifier: CIRCCMB2
   Summary: In this article we continue the investigations from \cite{CIRCCOMB.ABS} and \cite{FACIRC_1.ABS} of verification of a circuit design. We concentrate on the combination of multi cell circuits from given cells (circuit modules). Namely, we formalize a design of the form \\ \input CIRCCMB2.PIC and prove its stability. The formalization proposed consists in a series of schemes which allow to define multi cells circuits and prove their properties. Our goal is to achive mathematical formalization which will allow to verify designs of real circuits.

   ---

7. Grzegorz Bancerek, Shin'nosuke Yamaguchi, Katsumi Wasaki. Full Adder Circuit. Part II, Formalized Mathematics 10(1), pages 65-71, 2002. MML Identifier: FACIRC_2
   Summary: In this article we continue the investigations from \cite{FACIRC_1.ABS} of verification of a design of adder circuit. We define it as a combination of 1-bit adders using schemes from \cite{CIRCCMB2.ABS}. $n$-bit adder circuit has the following structure\\ \input FACIRC_2.PIC As the main result we prove the stability of the circuit. Further works will consist of the proof of full correctness of the circuit.

   ---