:: Correctness of Johnson 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; begin :: Correctness of Johnson Counter Circuits. :: 2-bit Johnson Counter (2JC). :: state transition; s0(00) -> s1(01) -> s3(11) -> s2(10) -> s0... :: minor loop; none theorem :: GATE_3:1 ::2JC: for s0,s1,s2,s3,ns0,ns1,ns2,ns3,q1,q2,nq1,nq2 being set holds (s0 is not empty iff AND2(NOT1 q2, NOT1 q1) is not empty)& (s1 is not empty iff AND2( NOT1 q2, q1) is not empty)& (s2 is not empty iff AND2( q2, NOT1 q1) is not empty)& (s3 is not empty iff AND2( q2, q1) is not empty) & (ns0 is not empty iff AND2(NOT1 nq2,NOT1 nq1) is not empty)& (ns1 is not empty iff AND2(NOT1 nq2, nq1) is not empty)& (ns2 is not empty iff AND2( nq2,NOT1 nq1) is not empty)& ( ns3 is not empty iff AND2( nq2, nq1) is not empty) & (nq1 is not empty iff NOT1 q2 is not empty)& (nq2 is not empty iff q1 is not empty) implies (ns1 is not empty iff s0 is not empty)& (ns3 is not empty iff s1 is not empty)& (ns2 is not empty iff s3 is not empty)& (ns0 is not empty iff s2 is not empty); :: 2-bit Johnson Counter with a Reset input (2JCWR). :: initial state; s*(xx) -> s0(00) [reset] :: state transition; s0(00) -> s1(01) -> s3(11) -> s2(10) -> s0... :: minor loop; none theorem :: GATE_3:2 ::2JCWR: for s0,s1,s2,s3,ns0,ns1,ns2,ns3,q1,q2,nq1,nq2,R being set holds (s0 is not empty iff AND2(NOT1 q2, NOT1 q1) is not empty)& (s1 is not empty iff AND2( NOT1 q2, q1) is not empty)& (s2 is not empty iff AND2( q2, NOT1 q1) is not empty)& (s3 is not empty iff AND2( q2, q1) is not empty) & (ns0 is not empty iff AND2(NOT1 nq2,NOT1 nq1) is not empty)& (ns1 is not empty iff AND2(NOT1 nq2, nq1) is not empty)& (ns2 is not empty iff AND2( nq2,NOT1 nq1) is not empty)& ( ns3 is not empty iff AND2( nq2, nq1) is not empty) & (nq1 is not empty iff AND2 (NOT1 q2, R) is not empty)& (nq2 is not empty iff AND2( q1, R) is not empty) implies (ns1 is not empty iff AND2(s0, R) is not empty)& (ns3 is not empty iff AND2(s1, R) is not empty)& (ns2 is not empty iff AND2(s3, R) is not empty)& ( ns0 is not empty iff OR2(AND2(s2, R),NOT1 R) is not empty); :: 3-bit Johnson Counter (3JC). :: state transition; s0(000) -> s1(001) -> s3(011) -> s7(111) -> :: -> s6(110) -> s4(100) -> s0(000) ... :: minor loop; s2(010) -> s5(101) -> s2(010) -> s5(101) ... theorem :: GATE_3:3 ::3JC: 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 not empty iff AND3(NOT1 q3, NOT1 q2, NOT1 q1 ) is not empty)& (s1 is not empty iff AND3(NOT1 q3, NOT1 q2, q1) is not empty)& (s2 is not empty iff AND3(NOT1 q3, q2, NOT1 q1) is not empty)& (s3 is not empty iff AND3(NOT1 q3, q2, q1) is not empty)& (s4 is not empty iff AND3( q3, NOT1 q2 , NOT1 q1) is not empty)& (s5 is not empty iff AND3( q3, NOT1 q2, q1) is not empty)& (s6 is not empty iff AND3( q3, q2, NOT1 q1) is not empty)& (s7 is not empty iff AND3( q3, q2, q1) is not empty) & (ns0 is not empty iff AND3(NOT1 nq3 ,NOT1 nq2,NOT1 nq1) is not empty)& (ns1 is not empty iff AND3(NOT1 nq3,NOT1 nq2 , nq1) is not empty)& (ns2 is not empty iff AND3(NOT1 nq3, nq2,NOT1 nq1) is not empty)& (ns3 is not empty iff AND3(NOT1 nq3, nq2, nq1) is not empty)& (ns4 is not empty iff AND3( nq3,NOT1 nq2,NOT1 nq1) is not empty)& (ns5 is not empty iff AND3( nq3,NOT1 nq2, nq1) is not empty)& (ns6 is not empty iff AND3( nq3, nq2, NOT1 nq1) is not empty)& (ns7 is not empty iff AND3( nq3, nq2, nq1) is not empty) & (nq1 is not empty iff NOT1 q3 is not empty)& (nq2 is not empty iff q1 is not empty)& (nq3 is not empty iff q2 is not empty) implies (ns1 is not empty iff s0 is not empty)& (ns3 is not empty iff s1 is not empty)& (ns7 is not empty iff s3 is not empty)& (ns6 is not empty iff s7 is not empty)& (ns4 is not empty iff s6 is not empty)& (ns0 is not empty iff s4 is not empty) & (ns2 is not empty iff s5 is not empty)& (ns5 is not empty iff s2 is not empty); :: 3-bit Johnson Counter with a Reset input (3JCWR). :: initial state; s*(xxx) -> s0(000) [reset] :: state transition; s0(000) -> s1(001) -> s3(011) -> s7(111) -> :: -> s6(110) -> s4(100) -> s0(000) ... :: minor loop; s2(010) -> s5(101) -> s2(010) -> s5(101) ... theorem :: GATE_3:4 ::3JCWR: 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 not empty iff AND3(NOT1 q3, NOT1 q2, NOT1 q1) is not empty)& (s1 is not empty iff AND3(NOT1 q3, NOT1 q2, q1) is not empty )& (s2 is not empty iff AND3(NOT1 q3, q2, NOT1 q1) is not empty)& (s3 is not empty iff AND3(NOT1 q3, q2, q1) is not empty)& (s4 is not empty iff AND3( q3, NOT1 q2, NOT1 q1) is not empty)& (s5 is not empty iff AND3( q3, NOT1 q2, q1) is not empty)& (s6 is not empty iff AND3( q3, q2, NOT1 q1) is not empty)& (s7 is not empty iff AND3( q3, q2, q1) is not empty) & (ns0 is not empty iff AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1) is not empty)& (ns1 is not empty iff AND3(NOT1 nq3,NOT1 nq2, nq1) is not empty)& (ns2 is not empty iff AND3(NOT1 nq3, nq2,NOT1 nq1) is not empty)& (ns3 is not empty iff AND3(NOT1 nq3, nq2, nq1) is not empty)& (ns4 is not empty iff AND3( nq3,NOT1 nq2,NOT1 nq1) is not empty)& (ns5 is not empty iff AND3( nq3,NOT1 nq2, nq1) is not empty)& (ns6 is not empty iff AND3( nq3, nq2,NOT1 nq1) is not empty)& (ns7 is not empty iff AND3( nq3, nq2, nq1) is not empty) & (nq1 is not empty iff AND2(NOT1 q3, R) is not empty)& (nq2 is not empty iff AND2( q1, R) is not empty)& (nq3 is not empty iff AND2( q2, R) is not empty) implies (ns1 is not empty iff AND2(s0, R) is not empty)& (ns3 is not empty iff AND2(s1, R) is not empty)& (ns7 is not empty iff AND2(s3, R) is not empty)& (ns6 is not empty iff AND2(s7, R) is not empty)& (ns4 is not empty iff AND2(s6, R) is not empty)& (ns0 is not empty iff OR2(AND2(s4, R),NOT1 R) is not empty) & (ns2 is not empty iff AND2(s5, R) is not empty)& (ns5 is not empty iff AND2(s2, R) is not empty); :: 4-bit Johnson Counter (4JC). :: state transition; s0(0000) -> s1(0001) -> s3(0011) -> s7(0111) -> :: ->s15(1111) ->s14(1110) ->s12(1100) -> s8(1000) -> s0.. :: minor loop; s2(0010) -> s5(0101) ->s11(1011) -> s6(0110) -> :: ->s13(1101) ->s10(1010) -> s4(0100) -> s9(1001) -> s2.. theorem :: GATE_3:5 ::4JC: for s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15, ns0,ns1,ns2 ,ns3,ns4,ns5,ns6,ns7,ns8,ns9,ns10,ns11,ns12,ns13,ns14,ns15, q1,q2,q3,q4,nq1,nq2 ,nq3,nq4 being set holds (s0 is not empty iff AND4(NOT1 q4, NOT1 q3, NOT1 q2, NOT1 q1) is not empty)& (s1 is not empty iff AND4(NOT1 q4, NOT1 q3, NOT1 q2, q1 ) is not empty)& (s2 is not empty iff AND4(NOT1 q4, NOT1 q3, q2, NOT1 q1) is not empty)& (s3 is not empty iff AND4(NOT1 q4, NOT1 q3, q2, q1) is not empty)& (s4 is not empty iff AND4(NOT1 q4, q3, NOT1 q2, NOT1 q1) is not empty)& (s5 is not empty iff AND4(NOT1 q4, q3, NOT1 q2, q1) is not empty)& (s6 is not empty iff AND4(NOT1 q4, q3, q2, NOT1 q1) is not empty)& (s7 is not empty iff AND4( NOT1 q4, q3, q2, q1) is not empty)& (s8 is not empty iff AND4( q4, NOT1 q3, NOT1 q2, NOT1 q1) is not empty)& (s9 is not empty iff AND4( q4, NOT1 q3, NOT1 q2, q1) is not empty)& (s10 is not empty iff AND4( q4, NOT1 q3, q2, NOT1 q1) is not empty)& (s11 is not empty iff AND4( q4, NOT1 q3, q2, q1) is not empty)& ( s12 is not empty iff AND4( q4, q3, NOT1 q2, NOT1 q1) is not empty)& (s13 is not empty iff AND4( q4, q3, NOT1 q2, q1) is not empty)& (s14 is not empty iff AND4( q4, q3, q2, NOT1 q1) is not empty)& (s15 is not empty iff AND4( q4, q3, q2, q1) is not empty) & (ns0 is not empty iff AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1) is not empty)& (ns1 is not empty iff AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, nq1) is not empty)& (ns2 is not empty iff AND4(NOT1 nq4, NOT1 nq3, nq2, NOT1 nq1) is not empty)& (ns3 is not empty iff AND4(NOT1 nq4, NOT1 nq3, nq2, nq1) is not empty)& (ns4 is not empty iff AND4(NOT1 nq4, nq3, NOT1 nq2, NOT1 nq1) is not empty)& (ns5 is not empty iff AND4(NOT1 nq4, nq3, NOT1 nq2, nq1) is not empty)& (ns6 is not empty iff AND4(NOT1 nq4, nq3, nq2, NOT1 nq1) is not empty)& (ns7 is not empty iff AND4(NOT1 nq4, nq3, nq2, nq1) is not empty)& (ns8 is not empty iff AND4( nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1) is not empty)& (ns9 is not empty iff AND4( nq4, NOT1 nq3, NOT1 nq2, nq1) is not empty)& (ns10 is not empty iff AND4( nq4, NOT1 nq3, nq2, NOT1 nq1) is not empty)& (ns11 is not empty iff AND4( nq4, NOT1 nq3, nq2, nq1) is not empty)& (ns12 is not empty iff AND4( nq4, nq3, NOT1 nq2, NOT1 nq1) is not empty)& (ns13 is not empty iff AND4( nq4, nq3, NOT1 nq2, nq1) is not empty)& (ns14 is not empty iff AND4( nq4, nq3, nq2, NOT1 nq1) is not empty)& (ns15 is not empty iff AND4( nq4, nq3, nq2, nq1) is not empty) & (nq1 is not empty iff NOT1 q4 is not empty)& (nq2 is not empty iff q1 is not empty)& (nq3 is not empty iff q2 is not empty)& (nq4 is not empty iff q3 is not empty) implies (ns1 is not empty iff s0 is not empty )& (ns3 is not empty iff s1 is not empty )& (ns7 is not empty iff s3 is not empty )& (ns15 is not empty iff s7 is not empty )& (ns14 is not empty iff s15 is not empty)& ( ns12 is not empty iff s14 is not empty)& (ns8 is not empty iff s12 is not empty )& (ns0 is not empty iff s8 is not empty ) & (ns5 is not empty iff s2 is not empty )& (ns11 is not empty iff s5 is not empty )& (ns6 is not empty iff s11 is not empty)& (ns13 is not empty iff s6 is not empty )& (ns10 is not empty iff s13 is not empty)& (ns4 is not empty iff s10 is not empty)& (ns9 is not empty iff s4 is not empty)& (ns2 is not empty iff s9 is not empty); :: 4-bit Johnson Counter with a Reset input (4JCWR). :: initial state; s*(xxxx) -> s0(0000) [reset] :: state transition; s0(0000) -> s1(0001) -> s3(0011) -> s7(0111) -> :: ->s15(1111) ->s14(1110) ->s12(1100) -> s8(1000) -> s0.. :: minor loop; s2(0010) -> s5(0101) ->s11(1011) -> s6(0110) -> :: ->s13(1101) ->s10(1010) -> s4(0100) -> s9(1001) -> s2.. theorem :: GATE_3:6 ::4JCRW: for s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15, ns0,ns1,ns2 ,ns3,ns4,ns5,ns6,ns7,ns8,ns9,ns10,ns11,ns12,ns13,ns14,ns15, q1,q2,q3,q4,nq1,nq2 ,nq3,nq4,R being set holds (s0 is not empty iff AND4(NOT1 q4, NOT1 q3, NOT1 q2, NOT1 q1) is not empty)& (s1 is not empty iff AND4(NOT1 q4, NOT1 q3, NOT1 q2, q1 ) is not empty)& (s2 is not empty iff AND4(NOT1 q4, NOT1 q3, q2, NOT1 q1) is not empty)& (s3 is not empty iff AND4(NOT1 q4, NOT1 q3, q2, q1) is not empty)& (s4 is not empty iff AND4(NOT1 q4, q3, NOT1 q2, NOT1 q1) is not empty)& (s5 is not empty iff AND4(NOT1 q4, q3, NOT1 q2, q1) is not empty)& (s6 is not empty iff AND4(NOT1 q4, q3, q2, NOT1 q1) is not empty)& (s7 is not empty iff AND4( NOT1 q4, q3, q2, q1) is not empty)& (s8 is not empty iff AND4( q4, NOT1 q3, NOT1 q2, NOT1 q1) is not empty)& (s9 is not empty iff AND4( q4, NOT1 q3, NOT1 q2, q1) is not empty)& (s10 is not empty iff AND4( q4, NOT1 q3, q2, NOT1 q1) is not empty)& (s11 is not empty iff AND4( q4, NOT1 q3, q2, q1) is not empty)& ( s12 is not empty iff AND4( q4, q3, NOT1 q2, NOT1 q1) is not empty)& (s13 is not empty iff AND4( q4, q3, NOT1 q2, q1) is not empty)& (s14 is not empty iff AND4( q4, q3, q2, NOT1 q1) is not empty)& (s15 is not empty iff AND4( q4, q3, q2, q1) is not empty) & (ns0 is not empty iff AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1) is not empty)& (ns1 is not empty iff AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, nq1) is not empty)& (ns2 is not empty iff AND4(NOT1 nq4, NOT1 nq3, nq2, NOT1 nq1) is not empty)& (ns3 is not empty iff AND4(NOT1 nq4, NOT1 nq3, nq2, nq1) is not empty)& (ns4 is not empty iff AND4(NOT1 nq4, nq3, NOT1 nq2, NOT1 nq1) is not empty)& (ns5 is not empty iff AND4(NOT1 nq4, nq3, NOT1 nq2, nq1) is not empty)& (ns6 is not empty iff AND4(NOT1 nq4, nq3, nq2, NOT1 nq1) is not empty)& (ns7 is not empty iff AND4(NOT1 nq4, nq3, nq2, nq1) is not empty)& (ns8 is not empty iff AND4( nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1) is not empty)& (ns9 is not empty iff AND4( nq4, NOT1 nq3, NOT1 nq2, nq1) is not empty)& (ns10 is not empty iff AND4( nq4, NOT1 nq3, nq2, NOT1 nq1) is not empty)& (ns11 is not empty iff AND4( nq4, NOT1 nq3, nq2, nq1) is not empty)& (ns12 is not empty iff AND4( nq4, nq3, NOT1 nq2, NOT1 nq1) is not empty)& (ns13 is not empty iff AND4( nq4, nq3, NOT1 nq2, nq1) is not empty)& (ns14 is not empty iff AND4( nq4, nq3, nq2, NOT1 nq1) is not empty)& (ns15 is not empty iff AND4( nq4, nq3, nq2, nq1) is not empty) & (nq1 is not empty iff AND2(NOT1 q4,R) is not empty)& (nq2 is not empty iff AND2( q1,R) is not empty)& (nq3 is not empty iff AND2( q2,R) is not empty)& (nq4 is not empty iff AND2( q3,R) is not empty) implies (ns1 is not empty iff AND2(s0,R) is not empty)& (ns3 is not empty iff AND2(s1,R) is not empty)& (ns7 is not empty iff AND2(s3,R) is not empty)& (ns15 is not empty iff AND2(s7,R) is not empty)& (ns14 is not empty iff AND2(s15,R) is not empty)& (ns12 is not empty iff AND2(s14,R) is not empty)& (ns8 is not empty iff AND2(s12,R) is not empty)& (ns0 is not empty iff OR2(AND2(s8,R),NOT1 R) is not empty) & (ns5 is not empty iff AND2(s2,R) is not empty)& (ns11 is not empty iff AND2(s5,R) is not empty)& (ns6 is not empty iff AND2(s11,R) is not empty)& (ns13 is not empty iff AND2(s6,R) is not empty)& (ns10 is not empty iff AND2(s13,R) is not empty)& (ns4 is not empty iff AND2(s10,R) is not empty)& (ns9 is not empty iff AND2(s4, R) is not empty)& (ns2 is not empty iff AND2(s9,R) is not empty);