Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

Full Adder Circuit. Part II


Grzegorz Bancerek
Bialystok Technical University
Shin'nosuke Yamaguchi
Shinshu University, Nagano
Katsumi Wasaki
Shinshu University, Nagano

Summary.

In this article we continue the investigations from [5] of verification of a design of adder circuit. We define it as a combination of 1-bit adders using schemes from [6]. $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.

MML Identifier: FACIRC_2

The terminology and notation used in this paper have been introduced in the following articles [17] [16] [22] [21] [2] [18] [23] [1] [7] [8] [4] [10] [11] [3] [19] [24] [15] [9] [20] [13] [14] [12] [5]

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. Curried and uncurried functions. Journal of Formalized Mathematics, 2, 1990.
[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[5] Grzegorz Bancerek and Yatsuka Nakamura. Full adder circuit. Part I. Journal of Formalized Mathematics, 7, 1995.
[6] Grzegorz Bancerek, Shin'nosuke Yamaguchi, and Yasunari Shidama. Combining of multi cell circuits. Journal of Formalized Mathematics, 14, 2002.
[7] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[8] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[9] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[10] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.
[11] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[12] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Journal of Formalized Mathematics, 7, 1995.
[13] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, II. Journal of Formalized Mathematics, 6, 1994.
[14] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, II. Journal of Formalized Mathematics, 7, 1995.
[15] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.
[16] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.
[17] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[18] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[19] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.
[20] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.
[21] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[22] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[23] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[24] Edmund Woronowicz. Many-argument relations. Journal of Formalized Mathematics, 2, 1990.

Received March 22, 2002

[ Download a postscript version, MML identifier index, Mizar home page]