:: Correctness of Binary Counter Circuits :: by Yuguang Yang , Wasaki Katsumi , Yasushi Fuwa and Yatsuka Nakamura :: :: Received March 13, 1999 :: Copyright (c) 1999-2018 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; theorems GATE_1; 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 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) proof let s0,s1,s2,s3,s4,s5,s6,s7,ns0,ns1,ns2,ns3,ns4,ns5,ns6,ns7,q1,q2,q3,nq1, nq2,nq3 be set; assume that A1: s0 is non empty iff AND3(NOT1 q3,NOT1 q2,NOT1 q1) is not empty and A2: s1 is non empty iff AND3(NOT1 q3,NOT1 q2,q1) is not empty and A3: s2 is non empty iff AND3(NOT1 q3,q2,NOT1 q1) is not empty and A4: s3 is non empty iff AND3(NOT1 q3,q2,q1) is not empty and A5: s4 is non empty iff AND3(q3,NOT1 q2,NOT1 q1) is not empty and A6: s5 is non empty iff AND3(q3,NOT1 q2,q1) is not empty and A7: s6 is non empty iff AND3(q3,q2,NOT1 q1) is not empty and A8: s7 is non empty iff AND3(q3,q2,q1) is not empty and A9: ns0 is non empty iff AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1) is not empty and A10: ns1 is non empty iff AND3(NOT1 nq3,NOT1 nq2,nq1) is not empty and A11: ns2 is non empty iff AND3(NOT1 nq3,nq2,NOT1 nq1) is not empty and A12: ns3 is non empty iff AND3(NOT1 nq3,nq2,nq1) is not empty and A13: ns4 is non empty iff AND3(nq3,NOT1 nq2,NOT1 nq1) is not empty and A14: ns5 is non empty iff AND3(nq3,NOT1 nq2,nq1) is not empty and A15: ns6 is non empty iff AND3(nq3,nq2,NOT1 nq1) is not empty and A16: ns7 is non empty iff AND3(nq3,nq2,nq1) is not empty and A17: ( nq1 is non empty iff NOT1 q1 is not empty)&( nq2 is non empty iff XOR2(q1,q2) is not empty) and A18: nq3 is non empty iff OR2(AND2(q3, NOT1 q1), AND2(q1, XOR2(q2,q3))) is not empty; ns1 is non empty iff NOT1 nq3 is non empty & not XOR2(q1,q2) is not empty & not q1 is non empty by A10,A17; then ns1 is non empty iff (not q3 is not empty or not NOT1 q1 is not empty) & (not q1 is not empty or not XOR2(q2,q3) is not empty) & not q2 is non empty & not q1 is non empty by A18; hence ns1 is non empty iff s0 is non empty by A1; ns2 is non empty iff not AND2(q3, NOT1 q1) is non empty & not AND2(q1, XOR2(q2,q3)) is non empty & not q2 is non empty & q1 is non empty by A11,A17 ,A18,GATE_1:6; then ns2 is non empty iff (not q3 is non empty or q1 is non empty) & not q3 is non empty & not q2 is non empty & q1 is non empty; hence ns2 is non empty iff s1 is non empty by A2; ns3 is non empty iff NOT1 nq3 is non empty & XOR2(q1,q2) is non empty & not q1 is non empty by A12,A17; then ns3 is non empty iff (not q3 is non empty or not NOT1 q1 is non empty) & (not q1 is non empty or not XOR2(q2,q3) is non empty) & q2 is non empty & not q1 is non empty by A18; hence ns3 is non empty iff s2 is non empty by A3; ns4 is non empty iff (AND2(q3, NOT1 q1) is non empty or AND2(q1, XOR2( q2,q3)) is non empty) & q2 is non empty & q1 is non empty by A13,A17,A18, GATE_1:6; then ns4 is non empty iff not q3 is non empty & q2 is non empty & q1 is non empty; hence ns4 is non empty iff s3 is non empty by A4; ns5 is non empty iff nq3 is non empty & not XOR2(q1,q2) is non empty & not q1 is non empty by A14,A17; then ns5 is non empty iff (AND2(q3, NOT1 q1) is non empty or AND2(q1, XOR2( q2,q3)) is non empty) & not q2 is non empty & not q1 is non empty by A18; then ns5 is non empty iff q3 is non empty & NOT1 q2 is non empty & NOT1 q1 is non empty; hence ns5 is non empty iff s4 is non empty by A5; ns6 is non empty iff (AND2(q3, NOT1 q1) is non empty or AND2(q1, XOR2( q2,q3)) is non empty) & not q2 is non empty & q1 is non empty by A15,A17,A18, GATE_1:6; then ns6 is non empty iff q3 is non empty & not q2 is non empty & q1 is non empty; hence ns6 is non empty iff s5 is non empty by A6; ns7 is non empty iff nq3 is non empty & XOR2(q1,q2) is non empty & not q1 is non empty by A16,A17; then ns7 is non empty iff (AND2(q3, NOT1 q1) is non empty or AND2(q1, XOR2( q2,q3)) is non empty) & q2 is non empty & not q1 is non empty by A18; then ns7 is non empty iff q3 is non empty & q2 is non empty & NOT1 q1 is non empty; hence ns7 is non empty iff s6 is non empty by A7; ns0 is non empty iff not AND2(q3, NOT1 q1) is non empty & not AND2(q1, XOR2(q2,q3)) is non empty & q2 is non empty & q1 is non empty by A9,A17,A18, GATE_1:6; then ns0 is non empty iff (not q3 is non empty or q1 is non empty) & q3 is non empty & q2 is non empty & q1 is non empty; hence thesis by A8; end; theorem AND3(AND2(a,d),AND2(b,d),AND2(c,d)) is non empty iff AND2(AND3(a,b,c), d) is non empty proof a is non empty & b is non empty & c is non empty & d is non empty iff AND3(a,b,c) is non empty & d is non empty; hence thesis; end; theorem (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 ) proof A1: OR2(a,b) is non empty & OR2(c,b) is non empty iff (a is non empty or b is non empty) & (c is non empty or b is non empty); A2: OR2(a,b) is non empty & OR2(c,b) is non empty & OR2(d,b) is non empty iff (a is non empty or b is non empty ) & (c is non empty or b is non empty ) & (d is non empty or b is non empty ); not AND2(a,b) is non empty iff not (a is non empty & b is non empty); hence thesis by A1,A2; end; ::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 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) proof let s0,s1,s2,s3,s4,s5,s6,s7,ns0,ns1,ns2,ns3,ns4,ns5,ns6,ns7,q1,q2,q3,nq1, nq2,nq3,R be set; assume that A1: s0 is non empty iff AND3(NOT1 q3,NOT1 q2,NOT1 q1) is non empty and A2: s1 is non empty iff AND3(NOT1 q3,NOT1 q2,q1) is non empty and A3: s2 is non empty iff AND3(NOT1 q3,q2,NOT1 q1) is non empty and A4: s3 is non empty iff AND3(NOT1 q3,q2,q1) is non empty and A5: s4 is non empty iff AND3(q3,NOT1 q2,NOT1 q1) is non empty and A6: s5 is non empty iff AND3(q3,NOT1 q2,q1) is non empty and A7: s6 is non empty iff AND3(q3,q2,NOT1 q1) is non empty and A8: s7 is non empty iff AND3(q3,q2,q1) is non empty and A9: ns0 is non empty iff AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1) is non empty and A10: ns1 is non empty iff AND3(NOT1 nq3,NOT1 nq2,nq1) is non empty and A11: ns2 is non empty iff AND3(NOT1 nq3,nq2,NOT1 nq1) is non empty and A12: ns3 is non empty iff AND3(NOT1 nq3,nq2,nq1) is non empty and A13: ns4 is non empty iff AND3(nq3,NOT1 nq2,NOT1 nq1) is non empty and A14: ns5 is non empty iff AND3(nq3,NOT1 nq2,nq1) is non empty and A15: ns6 is non empty iff AND3(nq3,nq2,NOT1 nq1) is non empty and A16: ns7 is non empty iff AND3(nq3,nq2,nq1) is non empty and A17: nq1 is non empty iff AND2(NOT1 q1,R) is non empty and A18: nq2 is non empty iff AND2(XOR2(q1,q2),R) is non empty and A19: nq3 is non empty iff AND2(OR2(AND2(q3, NOT1 q1), AND2(q1, XOR2(q2, q3))),R) is non empty; ns1 is non empty iff not nq3 is non empty & ( not XOR2(q1,q2) is non empty or not R is non empty) & not q1 is non empty & R is non empty by A10,A17 ,A18; then ns1 is non empty iff (not q3 is non empty or not NOT1 q1 is non empty) & (not q1 is non empty or not XOR2(q2,q3) is non empty) & not q2 is non empty & not q1 is non empty & R is non empty by A19; hence ns1 is non empty iff AND2(s0,R) is non empty by A1; ns2 is non empty iff not nq3 is non empty & XOR2(q1,q2) is non empty & R is non empty & (not NOT1 q1 is non empty or not R is non empty) by A11,A17 ,A18; then ns2 is non empty iff not nq3 is non empty & XOR2(q1,q2) is non empty & R is non empty & q1 is non empty; then ns2 is non empty iff not AND2(q3, NOT1 q1) is non empty & not AND2(q1, XOR2(q2,q3)) is non empty & not q2 is non empty & q1 is non empty & R is non empty by A19; then ns2 is non empty iff (not q3 is non empty or q1 is non empty) & not q3 is non empty & not q2 is non empty & q1 is non empty & R is non empty; hence ns2 is non empty iff AND2(s1,R) is non empty by A2; ns3 is non empty iff not nq3 is non empty & XOR2(q1,q2) is non empty & R is non empty & not q1 is non empty & R is non empty by A12,A17,A18; then ns3 is non empty iff (not q3 is non empty or not NOT1 q1 is non empty) & (not q1 is non empty or not XOR2(q2,q3) is non empty) & q2 is non empty & not q1 is non empty & R is non empty by A19; hence ns3 is non empty iff AND2(s2,R) is non empty by A3; ns4 is non empty iff OR2(AND2(q3, NOT1 q1), AND2(q1, XOR2(q2,q3))) is non empty & R is non empty & not nq2 is non empty & not AND2(NOT1 q1,R) is non empty by A13,A17,A19; then ns4 is non empty iff OR2(AND2(q3, NOT1 q1), AND2(q1, XOR2(q2,q3))) is non empty & R is non empty & not XOR2(q1,q2) is non empty & q1 is non empty by A18; then ns4 is non empty iff ( q3 is non empty & NOT1 q1 is non empty or q1 is non empty & XOR2(q2,q3) is non empty ) & R is non empty & q2 is non empty & q1 is non empty; then ns4 is non empty iff not q3 is non empty & R is non empty & q2 is non empty & q1 is non empty; hence ns4 is non empty iff AND2(s3,R) is non empty by A4; ns5 is non empty iff nq3 is non empty & (not XOR2(q1,q2) is non empty or not R is non empty) & not q1 is non empty & R is non empty by A14,A17,A18; then ns5 is non empty iff OR2(AND2(q3, NOT1 q1), AND2(q1, XOR2(q2,q3))) is non empty & not q2 is non empty & not q1 is non empty & R is non empty by A19; then ns5 is non empty iff q3 is non empty & NOT1 q2 is non empty & NOT1 q1 is non empty & R is non empty; hence ns5 is non empty iff AND2(s4,R) is non empty by A5; ns6 is non empty iff nq3 is non empty & XOR2(q1,q2) is non empty & R is non empty & (not NOT1 q1 is non empty or not R is non empty) by A15,A17,A18; then ns6 is non empty iff nq3 is non empty & XOR2(q1,q2) is non empty & R is non empty & q1 is non empty; then ns6 is non empty iff ( q3 is non empty & NOT1 q1 is non empty or q1 is non empty & XOR2(q2,q3) is non empty ) & R is non empty & not q2 is non empty & q1 is non empty by A19; then ns6 is non empty iff q3 is non empty & R is non empty & not q2 is non empty & q1 is non empty; hence ns6 is non empty iff AND2(s5,R) is non empty by A6; ns7 is non empty iff nq3 is non empty & XOR2(q1,q2) is non empty & not q1 is non empty & R is non empty by A16,A17,A18; then ns7 is non empty iff OR2(AND2(q3, NOT1 q1), AND2(q1, XOR2(q2,q3))) is non empty & q2 is non empty & not q1 is non empty & R is non empty by A19; then ns7 is non empty iff q3 is non empty & q2 is non empty & NOT1 q1 is non empty & R is non empty; hence ns7 is non empty iff AND2(s6,R) is non empty by A7; ns0 is non empty iff q1 is non empty & not XOR2(q1,q2) is non empty & not OR2(AND2(q3, NOT1 q1), AND2(q1, XOR2(q2,q3))) is non empty or not R is non empty by A9,A17,A18,A19; then ns0 is non empty iff q1 is non empty & q2 is non empty & not AND2(q3, NOT1 q1) is non empty & not XOR2(q2,q3) is non empty or not R is non empty; then ns0 is non empty iff q1 is non empty & q2 is non empty & q1 is non empty & q3 is non empty or not R is non empty; hence thesis by A8; end;