:: Correctness of Binary Counter Circuits :: by Yuguang Yang , Wasaki Katsumi , Yasushi Fuwa and Yatsuka Nakamura :: :: Received March 13, 1999 :: Copyright (c) 1999-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, GATE_1; notations XBOOLE_0, GATE_1; constructors XBOOLE_0, GATE_1; registrations GATE_1; requirements BOOLE; begin :: Correctness of Binary Counter Circuits reserve a,b,c,d for set; ::Correctness of 3-bit binary counter without reset input ::state transition: s0 (000) -> s1 (001)-> s2 (010) -> ... ->s7 (111) -> s0 (000). theorem :: GATE_2:1 for s0,s1,s2,s3,s4,s5,s6,s7,ns0,ns1,ns2,ns3,ns4,ns5,ns6,ns7,q1,q2,q3, nq1, nq2,nq3 being set holds (s0 is non empty iff AND3(NOT1 q3,NOT1 q2,NOT1 q1) is not empty)& (s1 is non empty iff AND3(NOT1 q3,NOT1 q2,q1) is not empty)& (s2 is non empty iff AND3(NOT1 q3,q2,NOT1 q1) is not empty)& (s3 is non empty iff AND3(NOT1 q3,q2,q1) is not empty)& (s4 is non empty iff AND3(q3,NOT1 q2,NOT1 q1 ) is not empty)& (s5 is non empty iff AND3(q3,NOT1 q2,q1) is not empty)& (s6 is non empty iff AND3(q3,q2,NOT1 q1) is not empty)& (s7 is non empty iff AND3(q3, q2,q1) is not empty)& (ns0 is non empty iff AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1) is not empty)& (ns1 is non empty iff AND3(NOT1 nq3,NOT1 nq2,nq1) is not empty)& ( ns2 is non empty iff AND3(NOT1 nq3,nq2,NOT1 nq1) is not empty)& (ns3 is non empty iff AND3(NOT1 nq3,nq2,nq1) is not empty)& (ns4 is non empty iff AND3(nq3, NOT1 nq2,NOT1 nq1) is not empty)& (ns5 is non empty iff AND3(nq3,NOT1 nq2,nq1) is not empty)& (ns6 is non empty iff AND3(nq3,nq2,NOT1 nq1) is not empty)& (ns7 is non empty iff AND3(nq3,nq2,nq1) is not empty)& (nq1 is non empty iff (NOT1 q1) is not empty)& (nq2 is non empty iff XOR2(q1,q2) is not empty)& (nq3 is non empty iff OR2(AND2(q3, NOT1 q1), AND2(q1, XOR2(q2,q3))) is not empty) implies ( ns1 is non empty iff s0 is non empty)& (ns2 is non empty iff s1 is non empty)& (ns3 is non empty iff s2 is non empty)& (ns4 is non empty iff s3 is non empty)& (ns5 is non empty iff s4 is non empty)& (ns6 is non empty iff s5 is non empty)& (ns7 is non empty iff s6 is non empty)& (ns0 is non empty iff s7 is non empty); theorem :: GATE_2:2 AND3(AND2(a,d),AND2(b,d),AND2(c,d)) is non empty iff AND2(AND3(a,b,c), d) is non empty; theorem :: GATE_2:3 (not AND2(a,b) is non empty iff OR2(NOT1 a, NOT1 b) is non empty)& ( OR2(a,b) is non empty & OR2(c,b) is non empty iff OR2(AND2(a,c),b) is non empty ) & (OR2(a,b) is non empty & OR2(c,b) is non empty & OR2(d,b) is non empty iff OR2(AND3(a,c,d),b) is non empty)& (OR2(a,b) is non empty & (a is non empty iff c is non empty) implies OR2(c,b) is non empty ); ::Correctness of 3-bit binary counter with reset input R ::initial state s*(xxx) -> s0(000) [reset] ::state transition: s0 (000) -> s1 (001)-> s2 (010) -> ... ->s7 (111) -> s0 (000). theorem :: GATE_2:4 for s0,s1,s2,s3,s4,s5,s6,s7,ns0,ns1,ns2,ns3,ns4,ns5,ns6,ns7,q1,q2,q3, nq1, nq2,nq3,R being set holds (s0 is non empty iff AND3(NOT1 q3,NOT1 q2,NOT1 q1) is non empty)& (s1 is non empty iff AND3(NOT1 q3,NOT1 q2,q1) is non empty)& (s2 is non empty iff AND3(NOT1 q3,q2,NOT1 q1) is non empty)& (s3 is non empty iff AND3(NOT1 q3,q2,q1) is non empty)& (s4 is non empty iff AND3(q3,NOT1 q2, NOT1 q1) is non empty)& (s5 is non empty iff AND3(q3,NOT1 q2,q1) is non empty)& (s6 is non empty iff AND3(q3,q2,NOT1 q1) is non empty)& (s7 is non empty iff AND3(q3,q2,q1) is non empty)& (ns0 is non empty iff AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1) is non empty)& (ns1 is non empty iff AND3(NOT1 nq3,NOT1 nq2,nq1) is non empty)& (ns2 is non empty iff AND3(NOT1 nq3,nq2,NOT1 nq1) is non empty)& (ns3 is non empty iff AND3(NOT1 nq3,nq2,nq1) is non empty)& (ns4 is non empty iff AND3(nq3,NOT1 nq2,NOT1 nq1) is non empty)& (ns5 is non empty iff AND3(nq3,NOT1 nq2,nq1) is non empty)& (ns6 is non empty iff AND3(nq3,nq2,NOT1 nq1) is non empty)& (ns7 is non empty iff AND3(nq3,nq2,nq1) is non empty)& (nq1 is non empty iff AND2(NOT1 q1,R) is non empty)& (nq2 is non empty iff AND2(XOR2(q1,q2) ,R) is non empty)& (nq3 is non empty iff AND2(OR2(AND2(q3, NOT1 q1), AND2(q1, XOR2(q2,q3))),R) is non empty) implies (ns1 is non empty iff AND2(s0,R) is non empty)& (ns2 is non empty iff AND2(s1,R) is non empty)& (ns3 is non empty iff AND2(s2,R) is non empty)& (ns4 is non empty iff AND2(s3,R) is non empty)& (ns5 is non empty iff AND2(s4,R) is non empty)& (ns6 is non empty iff AND2(s5,R) is non empty)& (ns7 is non empty iff AND2(s6,R) is non empty)& (ns0 is non empty iff OR2(s7,NOT1 R) is non empty);