environ vocabulary GATE_1; notation GATE_1; constructors GATE_1, XBOOLE_0; 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 iff $AND2(NOT1 q2, NOT1 q1))& ($s1 iff $AND2(NOT1 q2, q1))& ($s2 iff $AND2( q2, NOT1 q1))& ($s3 iff $AND2( q2, q1)) & ($ns0 iff $AND2(NOT1 nq2,NOT1 nq1))& ($ns1 iff $AND2(NOT1 nq2, nq1))& ($ns2 iff $AND2( nq2,NOT1 nq1))& ($ns3 iff $AND2( nq2, nq1)) & ($nq1 iff $NOT1 q2)& ($nq2 iff $q1) implies ($ns1 iff $s0)& ($ns3 iff $s1)& ($ns2 iff $s3)& ($ns0 iff $s2); :: 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 iff $AND2(NOT1 q2, NOT1 q1))& ($s1 iff $AND2(NOT1 q2, q1))& ($s2 iff $AND2( q2, NOT1 q1))& ($s3 iff $AND2( q2, q1)) & ($ns0 iff $AND2(NOT1 nq2,NOT1 nq1))& ($ns1 iff $AND2(NOT1 nq2, nq1))& ($ns2 iff $AND2( nq2,NOT1 nq1))& ($ns3 iff $AND2( nq2, nq1)) & ($nq1 iff $AND2(NOT1 q2, R))& ($nq2 iff $AND2( q1, R)) implies ($ns1 iff $AND2(s0, R))& ($ns3 iff $AND2(s1, R))& ($ns2 iff $AND2(s3, R))& ($ns0 iff $OR2(AND2(s2, R),NOT1 R)); :: 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 iff $AND3(NOT1 q3, NOT1 q2, NOT1 q1))& ($s1 iff $AND3(NOT1 q3, NOT1 q2, q1))& ($s2 iff $AND3(NOT1 q3, q2, NOT1 q1))& ($s3 iff $AND3(NOT1 q3, q2, q1))& ($s4 iff $AND3( q3, NOT1 q2, NOT1 q1))& ($s5 iff $AND3( q3, NOT1 q2, q1))& ($s6 iff $AND3( q3, q2, NOT1 q1))& ($s7 iff $AND3( q3, q2, q1)) & ($ns0 iff $AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1))& ($ns1 iff $AND3(NOT1 nq3,NOT1 nq2, nq1))& ($ns2 iff $AND3(NOT1 nq3, nq2,NOT1 nq1))& ($ns3 iff $AND3(NOT1 nq3, nq2, nq1))& ($ns4 iff $AND3( nq3,NOT1 nq2,NOT1 nq1))& ($ns5 iff $AND3( nq3,NOT1 nq2, nq1))& ($ns6 iff $AND3( nq3, nq2,NOT1 nq1))& ($ns7 iff $AND3( nq3, nq2, nq1)) & ($nq1 iff $NOT1 q3)& ($nq2 iff $q1)& ($nq3 iff $q2) implies ($ns1 iff $s0)& ($ns3 iff $s1)& ($ns7 iff $s3)& ($ns6 iff $s7)& ($ns4 iff $s6)& ($ns0 iff $s4) & ($ns2 iff $s5)& ($ns5 iff $s2); :: 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 iff $AND3(NOT1 q3, NOT1 q2, NOT1 q1))& ($s1 iff $AND3(NOT1 q3, NOT1 q2, q1))& ($s2 iff $AND3(NOT1 q3, q2, NOT1 q1))& ($s3 iff $AND3(NOT1 q3, q2, q1))& ($s4 iff $AND3( q3, NOT1 q2, NOT1 q1))& ($s5 iff $AND3( q3, NOT1 q2, q1))& ($s6 iff $AND3( q3, q2, NOT1 q1))& ($s7 iff $AND3( q3, q2, q1)) & ($ns0 iff $AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1))& ($ns1 iff $AND3(NOT1 nq3,NOT1 nq2, nq1))& ($ns2 iff $AND3(NOT1 nq3, nq2,NOT1 nq1))& ($ns3 iff $AND3(NOT1 nq3, nq2, nq1))& ($ns4 iff $AND3( nq3,NOT1 nq2,NOT1 nq1))& ($ns5 iff $AND3( nq3,NOT1 nq2, nq1))& ($ns6 iff $AND3( nq3, nq2,NOT1 nq1))& ($ns7 iff $AND3( nq3, nq2, nq1)) & ($nq1 iff $AND2(NOT1 q3, R))& ($nq2 iff $AND2( q1, R))& ($nq3 iff $AND2( q2, R)) implies ($ns1 iff $AND2(s0, R))& ($ns3 iff $AND2(s1, R))& ($ns7 iff $AND2(s3, R))& ($ns6 iff $AND2(s7, R))& ($ns4 iff $AND2(s6, R))& ($ns0 iff $OR2(AND2(s4, R),NOT1 R)) & ($ns2 iff $AND2(s5, R))& ($ns5 iff $AND2(s2, R)); :: 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 iff $AND4(NOT1 q4, NOT1 q3, NOT1 q2, NOT1 q1))& ($s1 iff $AND4(NOT1 q4, NOT1 q3, NOT1 q2, q1))& ($s2 iff $AND4(NOT1 q4, NOT1 q3, q2, NOT1 q1))& ($s3 iff $AND4(NOT1 q4, NOT1 q3, q2, q1))& ($s4 iff $AND4(NOT1 q4, q3, NOT1 q2, NOT1 q1))& ($s5 iff $AND4(NOT1 q4, q3, NOT1 q2, q1))& ($s6 iff $AND4(NOT1 q4, q3, q2, NOT1 q1))& ($s7 iff $AND4(NOT1 q4, q3, q2, q1))& ($s8 iff $AND4( q4, NOT1 q3, NOT1 q2, NOT1 q1))& ($s9 iff $AND4( q4, NOT1 q3, NOT1 q2, q1))& ($s10 iff $AND4( q4, NOT1 q3, q2, NOT1 q1))& ($s11 iff $AND4( q4, NOT1 q3, q2, q1))& ($s12 iff $AND4( q4, q3, NOT1 q2, NOT1 q1))& ($s13 iff $AND4( q4, q3, NOT1 q2, q1))& ($s14 iff $AND4( q4, q3, q2, NOT1 q1))& ($s15 iff $AND4( q4, q3, q2, q1)) & ($ns0 iff $AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1))& ($ns1 iff $AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, nq1))& ($ns2 iff $AND4(NOT1 nq4, NOT1 nq3, nq2, NOT1 nq1))& ($ns3 iff $AND4(NOT1 nq4, NOT1 nq3, nq2, nq1))& ($ns4 iff $AND4(NOT1 nq4, nq3, NOT1 nq2, NOT1 nq1))& ($ns5 iff $AND4(NOT1 nq4, nq3, NOT1 nq2, nq1))& ($ns6 iff $AND4(NOT1 nq4, nq3, nq2, NOT1 nq1))& ($ns7 iff $AND4(NOT1 nq4, nq3, nq2, nq1))& ($ns8 iff $AND4( nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1))& ($ns9 iff $AND4( nq4, NOT1 nq3, NOT1 nq2, nq1))& ($ns10 iff $AND4( nq4, NOT1 nq3, nq2, NOT1 nq1))& ($ns11 iff $AND4( nq4, NOT1 nq3, nq2, nq1))& ($ns12 iff $AND4( nq4, nq3, NOT1 nq2, NOT1 nq1))& ($ns13 iff $AND4( nq4, nq3, NOT1 nq2, nq1))& ($ns14 iff $AND4( nq4, nq3, nq2, NOT1 nq1))& ($ns15 iff $AND4( nq4, nq3, nq2, nq1)) & ($nq1 iff $NOT1 q4)& ($nq2 iff $q1)& ($nq3 iff $q2)& ($nq4 iff $q3) implies ($ns1 iff $s0 )& ($ns3 iff $s1 )& ($ns7 iff $s3 )& ($ns15 iff $s7 )& ($ns14 iff $s15)& ($ns12 iff $s14)& ($ns8 iff $s12)& ($ns0 iff $s8 ) & ($ns5 iff $s2 )& ($ns11 iff $s5 )& ($ns6 iff $s11)& ($ns13 iff $s6 )& ($ns10 iff $s13)& ($ns4 iff $s10)& ($ns9 iff $s4 )& ($ns2 iff $s9 ); :: 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 iff $AND4(NOT1 q4, NOT1 q3, NOT1 q2, NOT1 q1))& ($s1 iff $AND4(NOT1 q4, NOT1 q3, NOT1 q2, q1))& ($s2 iff $AND4(NOT1 q4, NOT1 q3, q2, NOT1 q1))& ($s3 iff $AND4(NOT1 q4, NOT1 q3, q2, q1))& ($s4 iff $AND4(NOT1 q4, q3, NOT1 q2, NOT1 q1))& ($s5 iff $AND4(NOT1 q4, q3, NOT1 q2, q1))& ($s6 iff $AND4(NOT1 q4, q3, q2, NOT1 q1))& ($s7 iff $AND4(NOT1 q4, q3, q2, q1))& ($s8 iff $AND4( q4, NOT1 q3, NOT1 q2, NOT1 q1))& ($s9 iff $AND4( q4, NOT1 q3, NOT1 q2, q1))& ($s10 iff $AND4( q4, NOT1 q3, q2, NOT1 q1))& ($s11 iff $AND4( q4, NOT1 q3, q2, q1))& ($s12 iff $AND4( q4, q3, NOT1 q2, NOT1 q1))& ($s13 iff $AND4( q4, q3, NOT1 q2, q1))& ($s14 iff $AND4( q4, q3, q2, NOT1 q1))& ($s15 iff $AND4( q4, q3, q2, q1)) & ($ns0 iff $AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1))& ($ns1 iff $AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, nq1))& ($ns2 iff $AND4(NOT1 nq4, NOT1 nq3, nq2, NOT1 nq1))& ($ns3 iff $AND4(NOT1 nq4, NOT1 nq3, nq2, nq1))& ($ns4 iff $AND4(NOT1 nq4, nq3, NOT1 nq2, NOT1 nq1))& ($ns5 iff $AND4(NOT1 nq4, nq3, NOT1 nq2, nq1))& ($ns6 iff $AND4(NOT1 nq4, nq3, nq2, NOT1 nq1))& ($ns7 iff $AND4(NOT1 nq4, nq3, nq2, nq1))& ($ns8 iff $AND4( nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1))& ($ns9 iff $AND4( nq4, NOT1 nq3, NOT1 nq2, nq1))& ($ns10 iff $AND4( nq4, NOT1 nq3, nq2, NOT1 nq1))& ($ns11 iff $AND4( nq4, NOT1 nq3, nq2, nq1))& ($ns12 iff $AND4( nq4, nq3, NOT1 nq2, NOT1 nq1))& ($ns13 iff $AND4( nq4, nq3, NOT1 nq2, nq1))& ($ns14 iff $AND4( nq4, nq3, nq2, NOT1 nq1))& ($ns15 iff $AND4( nq4, nq3, nq2, nq1)) & ($nq1 iff $AND2(NOT1 q4,R))& ($nq2 iff $AND2( q1,R))& ($nq3 iff $AND2( q2,R))& ($nq4 iff $AND2( q3,R)) implies ($ns1 iff $AND2(s0 ,R))& ($ns3 iff $AND2(s1 ,R))& ($ns7 iff $AND2(s3 ,R))& ($ns15 iff $AND2(s7 ,R))& ($ns14 iff $AND2(s15,R))& ($ns12 iff $AND2(s14,R))& ($ns8 iff $AND2(s12,R))& ($ns0 iff $OR2(AND2(s8 ,R),NOT1 R)) & ($ns5 iff $AND2(s2 ,R))& ($ns11 iff $AND2(s5 ,R))& ($ns6 iff $AND2(s11,R))& ($ns13 iff $AND2(s6 ,R))& ($ns10 iff $AND2(s13,R))& ($ns4 iff $AND2(s10,R))& ($ns9 iff $AND2(s4 ,R))& ($ns2 iff $AND2(s9 ,R));