Volume 10, Number 1 (2002): pdf, ps, dvi.

- 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.

- 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.

- 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.

- 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.

- 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.

- 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.

- 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.