Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996
Association of Mizar Users
2's Complement Circuit

Katsumi Wasaki

National College of Technology, Nagano

Pauline N. Kawamoto

Shinshu University, Nagano
Summary.

This article introduces various Boolean operators
which are used in discussing the properties and stability
of a 2's complement circuit. We present the definitions
and related theorems for the following logical operators
which include negative input/output: 'and2a', 'or2a',
'xor2a' and 'nand2a', 'nor2a', etc. We formalize
the concept of a 2's complement circuit, define the
structures of complementors/incrementors for binary
operations, and prove the stability of the circuit.
The terminology and notation used in this paper have been
introduced in the following articles
[9]
[11]
[12]
[2]
[3]
[13]
[4]
[8]
[10]
[6]
[7]
[5]
[1]

Boolean Operators

2's Complement Circuit Properties
Bibliography
 [1]
Grzegorz Bancerek and Yatsuka Nakamura.
Full adder circuit. Part I.
Journal of Formalized Mathematics,
7, 1995.
 [2]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Czeslaw Bylinski.
Finite sequences and tuples of elements of a nonempty sets.
Journal of Formalized Mathematics,
2, 1990.
 [5]
Yatsuka Nakamura and Grzegorz Bancerek.
Combining of circuits.
Journal of Formalized Mathematics,
7, 1995.
 [6]
Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.
Preliminaries to circuits, II.
Journal of Formalized Mathematics,
6, 1994.
 [7]
Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.
Introduction to circuits, II.
Journal of Formalized Mathematics,
7, 1995.
 [8]
Takaya Nishiyama and Yasuho Mizuhara.
Binary arithmetics.
Journal of Formalized Mathematics,
5, 1993.
 [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]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [13]
Edmund Woronowicz.
Manyargument relations.
Journal of Formalized Mathematics,
2, 1990.
Received October 25, 1996
[
Download a postscript version,
MML identifier index,
Mizar home page]