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.
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]
-
One Gate Circuits
-
Defining Multi Cell Circuit Structures
-
Input of Multi Cell Circuit
-
Defining Multi Cell Circuits
-
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.
Received March 22, 2002
[
Download a postscript version,
MML identifier index,
Mizar home page]