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

## Combining of Multi Cell Circuits

Grzegorz Bancerek
Bialystok Technical University
Shin'nosuke Yamaguchi
Shinshu University, Nagano
Yasunari Shidama
Shinshu University, Nagano

### Summary.

In this article we continue the investigations from [10] and [2] 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.

#### MML Identifier: CIRCCMB2

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

#### Contents (PDF format)

1. One Gate Circuits
2. Defining Multi Cell Circuit Structures
3. Input of Multi Cell Circuit
4. Defining Multi Cell Circuits
5. Stability of Multi Cell Circuit

#### Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek and Yatsuka Nakamura. Full adder circuit. Part I. Journal of Formalized Mathematics, 7, 1995.
[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.
[7] 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.
[8] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[9] Jaroslaw Kotowicz. The limit of a real function at infinity. Journal of Formalized Mathematics, 2, 1990.
[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, II. Journal of Formalized Mathematics, 6, 1994.
[13] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, II. Journal of Formalized Mathematics, 7, 1995.
[14] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[15] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.
[16] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.
[17] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[18] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.