Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

Full Subtracter Circuit. Part I


Katsumi Wasaki
Shinshu University, Nagano
Noboru Endou
Shinshu University, Nagano

Summary.

We formalize the concept of the full subtracter circuit, define the structures of bit subtract/borrow units for binary operations, and prove the stability of the circuit.

MML Identifier: FSCIRC_1

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

Contents (PDF format)

  1. Bit Subtract and Borrow Circuit
  2. Bit Subtracter with Borrow 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] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Journal of Formalized Mathematics, 7, 1995.
[5] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, II. Journal of Formalized Mathematics, 6, 1994.
[6] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, II. Journal of Formalized Mathematics, 7, 1995.
[7] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.
[8] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.
[9] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[10] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.
[11] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[12] Katsumi Wasaki and Pauline N. Kawamoto. 2's complement circuit. Journal of Formalized Mathematics, 8, 1996.
[13] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[14] Edmund Woronowicz. Many-argument relations. Journal of Formalized Mathematics, 2, 1990.

Received March 13, 1999


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