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.

MML Identifier: TWOSCOMP

Contents (PDF format)

1. Boolean Operators
2. 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 non-empty 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. Many-argument relations. Journal of Formalized Mathematics, 2, 1990.