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

Correctness of Binary Counter Circuits

Yuguang Yang
Shinshu University, Nagano
Katsumi Wasaki
Shinshu University, Nagano
Yasushi Fuwa
Shinshu University, Nagano
Yatsuka Nakamura
Shinshu University, Nagano


This article introduces the verification of the correctness for the operations and the specification of the 3-bit counter. Both cases: without reset input and with reset input are considered. The proof was proposed by Y. Nakamura in [1].

MML Identifier: GATE_2

The terminology and notation used in this paper have been introduced in the following articles [1]

Contents (PDF format)


[1] Yatsuka Nakamura. Logic gates and logical equivalence of adders. Journal of Formalized Mathematics, 11, 1999.

Received March 13, 1999

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