Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

## Full Adder Circuit. Part I

Grzegorz Bancerek
Institute of Mathematics, Polish Academy of Sciences
Yatsuka Nakamura
Shinshu University, Nagano

### Summary.

We continue the formalisation of circuits started by Piotr Rudnicki, Andrzej Trybulec, Pauline Kawamoto, and the second author in [12], [13], [11], [14]. The first step in proving properties of full \$n\$-bit adder circuit, i.e. 1-bit adder, is presented. We employ the notation of combining circuits introduced in [10].

This work was written while the first author visited Shinshu University, July--August 1994.

#### MML Identifier: FACIRC_1

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

#### Contents (PDF format)

1. Combining of Many Sorted Signatures
2. Combining of Circuits
3. Signatures with One Operation
4. Unsplit Condition
5. One Gate Circuits
6. Boolean Circuits

#### Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.
[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.
[8] 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.
[9] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[10] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Journal of Formalized Mathematics, 7, 1995.
[11] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, I. Journal of Formalized Mathematics, 6, 1994.
[12] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Journal of Formalized Mathematics, 6, 1994.
[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 algebras. Journal of Formalized Mathematics, 6, 1994.
[20] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[21] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[22] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[23] Edmund Woronowicz. Many-argument relations. Journal of Formalized Mathematics, 2, 1990.