:: Correctness of Binary Counter Circuits
:: by Yuguang Yang , Wasaki Katsumi , Yasushi Fuwa and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999-2019 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;
thus (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
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;
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;
thus (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
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;
end;