Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

Full Subtracter Circuit. Part II


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

Summary.

In this article we continue investigations from [22] of verification of a design of subtracter circuit. We define it as a combination of multi cell circuit using schemes from [6]. As the main result we prove the stability of the circuit.

MML Identifier: FSCIRC_2

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

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] Grzegorz Bancerek, Shin'nosuke Yamaguchi, and Katsumi Wasaki. Full adder circuit. Part II. Journal of Formalized Mathematics, 14, 2002.
[8] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[9] Czeslaw Bylinski. Functions from a set to a set. 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] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Journal of Formalized Mathematics, 7, 1995.
[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] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.
[15] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.
[16] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[17] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[18] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.
[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] Katsumi Wasaki and Noboru Endou. Full subtracter circuit. Part I. Journal of Formalized Mathematics, 11, 1999.
[23] Katsumi Wasaki and Pauline N. Kawamoto. 2's complement circuit. Journal of Formalized Mathematics, 8, 1996.
[24] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[25] Edmund Woronowicz. Many-argument relations. Journal of Formalized Mathematics, 2, 1990.

Received February 25, 2003


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