### Correctness of Johnson Counter Circuits

by
Yuguang Yang,
Katsumi Wasaki,
Yasushi Fuwa, and
Yatsuka Nakamura

Received March 13, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: GATE_3
[ MML identifier index ]

```environ

vocabulary GATE_1;
notation GATE_1;
constructors GATE_1, XBOOLE_0;
theorems 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 ::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)
proof
let s0,s1,s2,s3,ns0,ns1,ns2,ns3,q1,q2,nq1,nq2 be set;
assume that A1:(\$s0 iff \$AND2(NOT1 q2,NOT1 q1)) and
A2:(\$s1 iff \$AND2(NOT1 q2,q1))and
A3:(\$s2 iff \$AND2(q2,NOT1 q1))and
A4:(\$s3 iff \$AND2(q2,q1))and
A5: (\$ns0 iff \$AND2(NOT1 nq2,NOT1 nq1))and
A6:(\$ns1 iff \$AND2(NOT1 nq2,nq1))and
A7:(\$ns2 iff \$AND2(nq2,NOT1 nq1))and
A8:(\$ns3 iff \$AND2(nq2,nq1))and
A9:(\$nq1 iff \$NOT1 q2)and
A10:(\$nq2 iff \$q1);
::
:: s0 -> s1
::
\$ns1 iff \$NOT1 nq2 & \$nq1 by A6,GATE_1:6;
then \$ns1 iff \$NOT1 q2 & \$NOT1 q1 by A9,A10,GATE_1:4;
hence \$ns1 iff \$s0 by A1,GATE_1:6;
::
:: s1 -> s3
::
thus \$ns3 iff \$s1 by A2,A8,A9,A10,GATE_1:6;
::
:: s3 -> s2
::
\$ns2 iff \$nq2 & \$NOT1 nq1 by A7,GATE_1:6;
then \$ns2 iff \$q2 & \$q1 by A9,A10,GATE_1:4;
hence \$ns2 iff \$s3 by A4,GATE_1:6;
::
:: s2 -> s0
::
\$ns0 iff \$NOT1 nq2 & \$NOT1 nq1 by A5,GATE_1:6;
then \$ns0 iff \$q2 & \$NOT1 q1 by A9,A10,GATE_1:4;
hence \$ns0 iff \$s2 by A3,GATE_1:6;
end;

:: 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 ::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))
proof
let s0,s1,s2,s3,ns0,ns1,ns2,ns3,q1,q2,nq1,nq2,R be set;
assume that A1:(\$s0 iff \$AND2(NOT1 q2,NOT1 q1)) and
A2:(\$s1 iff \$AND2(NOT1 q2,q1))and
A3:(\$s2 iff \$AND2(q2,NOT1 q1))and
A4:(\$s3 iff \$AND2(q2,q1))and
A5: (\$ns0 iff \$AND2(NOT1 nq2,NOT1 nq1))and
A6:(\$ns1 iff \$AND2(NOT1 nq2,nq1))and
A7:(\$ns2 iff \$AND2(nq2,NOT1 nq1))and
A8:(\$ns3 iff \$AND2(nq2,nq1))and
A9:(\$nq1 iff \$AND2(NOT1 q2,R))and
A10:(\$nq2 iff \$AND2( q1,R));
::
:: s0 -> s1
::
\$ns1 iff \$NOT1 nq2 & \$nq1 by A6,GATE_1:6;
then \$ns1 iff \$NOT1 q2 & \$R & not(\$q1 & \$R) by A9,A10,GATE_1:4,6;
then \$ns1 iff \$NOT1 q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns1 iff \$AND2(s0,R) by A1,GATE_1:6;
::
:: s1 -> s3
::
\$ns3 iff \$NOT1 q2 & \$q1 & \$R by A8,A9,A10,GATE_1:6;
hence \$ns3 iff \$AND2(s1,R) by A2,GATE_1:6;
::
:: s3 -> s2
::
\$ns2 iff \$nq2 & \$NOT1 nq1 by A7,GATE_1:6;
then \$ns2 iff not(\$NOT1 q2 & \$R) & \$q1 & \$R by A9,A10,GATE_1:4,6;
then \$ns2 iff \$q2 & \$q1 & \$R by GATE_1:4;
hence \$ns2 iff \$AND2(s3,R) by A4,GATE_1:6;
::
:: s2 -> s0
::
\$ns0 iff \$NOT1 nq2 & \$NOT1 nq1 by A5,GATE_1:6;
then \$ns0 iff not(\$NOT1 q2 & \$R) & not(\$q1 & \$R) by A9,A10,GATE_1:4,6;
then \$ns0 iff (\$q2 & \$NOT1 q1 & \$R) or not(\$R) by GATE_1:4;
then \$ns0 iff \$AND2(s2,R) or \$NOT1 R by A3,GATE_1:4,6;
hence \$ns0 iff \$OR2(AND2(s2, R),NOT1 R) by GATE_1:7;

end;

:: 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 ::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)
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 iff \$AND3(NOT1 q3,NOT1 q2,NOT1 q1)) and
A2:(\$s1 iff \$AND3(NOT1 q3,NOT1 q2,q1))and
A3:(\$s2 iff \$AND3(NOT1 q3,q2,NOT1 q1))and
A4:(\$s3 iff \$AND3(NOT1 q3,q2,q1))and
A5:(\$s4 iff \$AND3(q3,NOT1 q2,NOT1 q1))and
A6:(\$s5 iff \$AND3(q3,NOT1 q2,q1))and
A7:(\$s6 iff \$AND3(q3,q2,NOT1 q1))and
A8:(\$s7 iff \$AND3(q3,q2,q1))and
A9:(\$ns0 iff \$AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1))and
A10:(\$ns1 iff \$AND3(NOT1 nq3,NOT1 nq2,nq1))and
A11:(\$ns2 iff \$AND3(NOT1 nq3,nq2,NOT1 nq1))and
A12:(\$ns3 iff \$AND3(NOT1 nq3,nq2,nq1))and
A13:(\$ns4 iff \$AND3(nq3,NOT1 nq2,NOT1 nq1))and
A14:(\$ns5 iff \$AND3(nq3,NOT1 nq2,nq1))and
A15:(\$ns6 iff \$AND3(nq3,nq2,NOT1 nq1))and
A16:(\$ns7 iff \$AND3(nq3,nq2,nq1))and
A17:(\$nq1 iff \$NOT1 q3)and
A18:(\$nq2 iff \$q1)and
A19:(\$nq3 iff \$q2);
::
:: s0 -> s1
::
\$ns1 iff \$NOT1 nq3 & \$NOT1 nq2 & \$nq1 by A10,GATE_1:16;
then \$ns1 iff \$NOT1 q3 & \$NOT1 q2 & \$NOT1 q1 by A17,A18,A19,GATE_1:4;
hence \$ns1 iff \$s0 by A1,GATE_1:16;
::
:: s1 -> s3
::
\$ns3 iff \$NOT1 nq3 & \$nq2 & \$nq1 by A12,GATE_1:16;
then \$ns3 iff \$NOT1 q3 & \$NOT1 q2 & \$q1 by A17,A18,A19,GATE_1:4;
hence \$ns3 iff \$s1 by A2,GATE_1:16;
::
:: s3 -> s7
::
thus \$ns7 iff \$s3 by A4,A16,A17,A18,A19,GATE_1:16;
::
:: s7 -> s6
::
\$ns6 iff \$nq3 & \$nq2 & \$NOT1 nq1 by A15,GATE_1:16;
then \$ns6 iff \$q3 & \$q2 & \$q1 by A17,A18,A19,GATE_1:4;
hence \$ns6 iff \$s7 by A8,GATE_1:16;
::
:: s6 -> s4
::
\$ns4 iff \$nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A13,GATE_1:16;
then \$ns4 iff \$q3 & \$q2 & \$NOT1 q1 by A17,A18,A19,GATE_1:4;
hence \$ns4 iff \$s6 by A7,GATE_1:16;
::
:: s4 -> s0
::
\$ns0 iff \$NOT1 nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A9,GATE_1:16;
then \$ns0 iff \$q3 & \$NOT1 q2 & \$NOT1 q1 by A17,A18,A19,GATE_1:4;
hence \$ns0 iff \$s4 by A5,GATE_1:16;
::
:: minor loop
:: s5 -> s2
::
\$ns2 iff \$NOT1 nq3 & \$nq2 & \$NOT1 nq1 by A11,GATE_1:16;
then \$ns2 iff \$q3 & \$NOT1 q2 & \$q1 by A17,A18,A19,GATE_1:4;
hence \$ns2 iff \$s5 by A6,GATE_1:16;
::
:: minor loop
:: s2 -> s5
::
\$ns5 iff \$nq3 & \$NOT1 nq2 & \$nq1 by A14,GATE_1:16;
then \$ns5 iff \$NOT1 q3 & \$q2 & \$NOT1 q1 by A17,A18,A19,GATE_1:4;
hence \$ns5 iff \$s2 by A3,GATE_1:16;

end;

:: 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 ::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))
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 iff \$AND3(NOT1 q3,NOT1 q2,NOT1 q1)) and
A2:(\$s1 iff \$AND3(NOT1 q3,NOT1 q2,q1))and
A3:(\$s2 iff \$AND3(NOT1 q3,q2,NOT1 q1))and
A4:(\$s3 iff \$AND3(NOT1 q3,q2,q1))and
A5:(\$s4 iff \$AND3(q3,NOT1 q2,NOT1 q1))and
A6:(\$s5 iff \$AND3(q3,NOT1 q2,q1))and
A7:(\$s6 iff \$AND3(q3,q2,NOT1 q1))and
A8:(\$s7 iff \$AND3(q3,q2,q1))and
A9:(\$ns0 iff \$AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1))and
A10:(\$ns1 iff \$AND3(NOT1 nq3,NOT1 nq2,nq1))and
A11:(\$ns2 iff \$AND3(NOT1 nq3,nq2,NOT1 nq1))and
A12:(\$ns3 iff \$AND3(NOT1 nq3,nq2,nq1))and
A13:(\$ns4 iff \$AND3(nq3,NOT1 nq2,NOT1 nq1))and
A14:(\$ns5 iff \$AND3(nq3,NOT1 nq2,nq1))and
A15:(\$ns6 iff \$AND3(nq3,nq2,NOT1 nq1))and
A16:(\$ns7 iff \$AND3(nq3,nq2,nq1))and
A17:(\$nq1 iff \$AND2(NOT1 q3,R))and
A18:(\$nq2 iff \$AND2( q1,R))and
A19:(\$nq3 iff \$AND2( q2,R));
::
:: s0 -> s1
::
\$ns1 iff \$NOT1 nq3 & \$NOT1 nq2 & \$nq1 by A10,GATE_1:16;
then \$ns1 iff \$NOT1 q3 & \$R & not(\$q2 & \$R) & not(\$q1 & \$R)
by A17,A18,A19,GATE_1:4,6;
then \$ns1 iff \$NOT1 q3 & \$NOT1 q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns1 iff \$AND2(s0,R) by A1,GATE_1:6,16;
::
:: s1 -> s3
::
\$ns3 iff \$NOT1 nq3 & \$nq2 & \$nq1 by A12,GATE_1:16;
then \$ns3 iff \$NOT1 q3 & \$R & not(\$q2 & \$R) & \$q1 & \$R
by A17,A18,A19,GATE_1:4,6;
then \$ns3 iff \$NOT1 q3 & \$NOT1 q2 & \$q1 & \$R by GATE_1:4;
hence \$ns3 iff \$AND2(s1,R) by A2,GATE_1:6,16;
::
:: s3 -> s7
::
\$ns7 iff \$NOT1 q3 & \$R & \$q2 & \$R & \$q1 & \$R
by A16,A17,A18,A19,GATE_1:6,16;
hence \$ns7 iff \$AND2(s3,R) by A4,GATE_1:6,16;
::
:: s7 -> s6
::
\$ns6 iff \$nq3 & \$nq2 & \$NOT1 nq1 by A15,GATE_1:16;
then \$ns6 iff not(\$NOT1 q3 & \$R) & \$q2 & \$R & \$q1 & \$R
by A17,A18,A19,GATE_1:4,6;
then \$ns6 iff \$q3 & \$q2 & \$q1 & \$R by GATE_1:4;
hence \$ns6 iff \$AND2(s7,R) by A8,GATE_1:6,16;
::
:: s6 -> s4
::
\$ns4 iff \$nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A13,GATE_1:16;
then \$ns4 iff not(\$NOT1 q3 & \$R) & \$q2 & \$R & not(\$q1 & \$R)
by A17,A18,A19,GATE_1:4,6;
then \$ns4 iff \$q3 & \$q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns4 iff \$AND2(s6,R) by A7,GATE_1:6,16;
::
:: s4 -> s0(not reset), or s* -> s0(reset)
::
\$ns0 iff \$NOT1 nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A9,GATE_1:16;
then \$ns0 iff not(\$NOT1 q3 & \$R) & not(\$q2 & \$R) & not(\$q1 & \$R)
by A17,A18,A19,GATE_1:4,6;
then \$ns0 iff (\$q3 & \$NOT1 q2 & \$NOT1 q1 & \$R) or not(\$R) by GATE_1:4;
then \$ns0 iff \$AND2(s4,R) or \$NOT1 R by A5,GATE_1:4,6,16;
hence \$ns0 iff \$OR2(AND2(s4, R),NOT1 R) by GATE_1:7;
::
:: minor loop
:: s5 -> s2
::
\$ns2 iff \$NOT1 nq3 & \$nq2 & \$NOT1 nq1 by A11,GATE_1:16;
then \$ns2 iff not(\$NOT1 q3 & \$R) & not(\$q2 & \$R) & \$q1 & \$R
by A17,A18,A19,GATE_1:4,6;
then \$ns2 iff \$q3 & \$NOT1 q2 & \$q1 & \$R by GATE_1:4;
hence \$ns2 iff \$AND2(s5,R) by A6,GATE_1:6,16;
::
:: minor loop
:: s2 -> s5
::
\$ns5 iff \$nq3 & \$NOT1 nq2 & \$nq1 by A14,GATE_1:16;
then \$ns5 iff \$NOT1 q3 & \$R & \$q2 & \$R & not(\$q1 & \$R)
by A17,A18,A19,GATE_1:4,6;
then \$ns5 iff \$NOT1 q3 & \$q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns5 iff \$AND2(s2,R) by A3,GATE_1:6,16;

end;

:: 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 ::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 )
proof
let 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 be set;
assume that A1:(\$s0 iff \$AND4(NOT1 q4, NOT1 q3, NOT1 q2, NOT1 q1)) and
A2: (\$s1 iff \$AND4(NOT1 q4, NOT1 q3, NOT1 q2, q1)) and
A3: (\$s2 iff \$AND4(NOT1 q4, NOT1 q3, q2, NOT1 q1)) and
A4: (\$s3 iff \$AND4(NOT1 q4, NOT1 q3, q2, q1)) and
A5: (\$s4 iff \$AND4(NOT1 q4, q3, NOT1 q2, NOT1 q1)) and
A6: (\$s5 iff \$AND4(NOT1 q4, q3, NOT1 q2, q1)) and
A7: (\$s6 iff \$AND4(NOT1 q4, q3, q2, NOT1 q1)) and
A8: (\$s7 iff \$AND4(NOT1 q4, q3, q2, q1)) and
A9: (\$s8 iff \$AND4( q4, NOT1 q3, NOT1 q2, NOT1 q1)) and
A10:(\$s9 iff \$AND4( q4, NOT1 q3, NOT1 q2, q1)) and
A11:(\$s10 iff \$AND4( q4, NOT1 q3, q2, NOT1 q1)) and
A12:(\$s11 iff \$AND4( q4, NOT1 q3, q2, q1)) and
A13:(\$s12 iff \$AND4( q4, q3, NOT1 q2, NOT1 q1)) and
A14:(\$s13 iff \$AND4( q4, q3, NOT1 q2, q1)) and
A15:(\$s14 iff \$AND4( q4, q3, q2, NOT1 q1)) and
A16:(\$s15 iff \$AND4( q4, q3, q2, q1)) and
A17:(\$ns0 iff \$AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1)) and
A18:(\$ns1 iff \$AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, nq1)) and
A19:(\$ns2 iff \$AND4(NOT1 nq4, NOT1 nq3, nq2, NOT1 nq1)) and
A20:(\$ns3 iff \$AND4(NOT1 nq4, NOT1 nq3, nq2, nq1)) and
A21:(\$ns4 iff \$AND4(NOT1 nq4, nq3, NOT1 nq2, NOT1 nq1)) and
A22:(\$ns5 iff \$AND4(NOT1 nq4, nq3, NOT1 nq2, nq1)) and
A23:(\$ns6 iff \$AND4(NOT1 nq4, nq3, nq2, NOT1 nq1)) and
A24:(\$ns7 iff \$AND4(NOT1 nq4, nq3, nq2, nq1)) and
A25:(\$ns8 iff \$AND4( nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1)) and
A26:(\$ns9 iff \$AND4( nq4, NOT1 nq3, NOT1 nq2, nq1)) and
A27:(\$ns10 iff \$AND4( nq4, NOT1 nq3, nq2, NOT1 nq1)) and
A28:(\$ns11 iff \$AND4( nq4, NOT1 nq3, nq2, nq1)) and
A29:(\$ns12 iff \$AND4( nq4, nq3, NOT1 nq2, NOT1 nq1)) and
A30:(\$ns13 iff \$AND4( nq4, nq3, NOT1 nq2, nq1)) and
A31:(\$ns14 iff \$AND4( nq4, nq3, nq2, NOT1 nq1)) and
A32:(\$ns15 iff \$AND4( nq4, nq3, nq2, nq1)) and
A33:(\$nq1 iff \$NOT1 q4) and
A34:(\$nq2 iff \$q1) and
A35:(\$nq3 iff \$q2) and
A36:(\$nq4 iff \$q3);
::
:: s0 -> s1
::
\$ns1 iff \$NOT1 nq4 & \$NOT1 nq3 & \$NOT1 nq2 & \$nq1 by A18,GATE_1:22;
then \$ns1 iff \$NOT1 q4 & \$NOT1 q3 & \$NOT1 q2 & \$NOT1 q1
by A33,A34,A35,A36,GATE_1:4;
hence \$ns1 iff \$s0 by A1,GATE_1:22;
::
:: s1 -> s3
::
\$ns3 iff \$NOT1 nq4 & \$NOT1 nq3 & \$nq2 & \$nq1 by A20,GATE_1:22;
then \$ns3 iff \$NOT1 q4 & \$NOT1 q3 & \$NOT1 q2 & \$q1 by A33,A34,A35,A36,GATE_1:
4;
hence \$ns3 iff \$s1 by A2,GATE_1:22;
::
:: s3 -> s7
::
\$ns7 iff \$NOT1 nq4 & \$nq3 & \$nq2 & \$nq1 by A24,GATE_1:22;
then \$ns7 iff \$NOT1 q4 & \$NOT1 q3 & \$q2 & \$q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns7 iff \$s3 by A4,GATE_1:22;
::
:: s7 -> s15
::
thus \$ns15 iff \$s7 by A8,A32,A33,A34,A35,A36,GATE_1:22;
::
:: s15 -> s14
::
\$ns14 iff \$nq4 & \$nq3 & \$nq2 & \$NOT1 nq1 by A31,GATE_1:22;
then \$ns14 iff \$q4 & \$q3 & \$q2 & \$q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns14 iff \$s15 by A16,GATE_1:22;
::
:: s14 -> s12
::
\$ns12 iff \$nq4 & \$nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A29,GATE_1:22;
then \$ns12 iff \$q4 & \$q3 & \$q2 & \$NOT1 q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns12 iff \$s14 by A15,GATE_1:22;
::
:: s12 -> s8
::
\$ns8 iff \$nq4 & \$NOT1 nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A25,GATE_1:22;
then \$ns8 iff \$q4 & \$q3 & \$NOT1 q2 & \$NOT1 q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns8 iff \$s12 by A13,GATE_1:22;
::
:: s8 -> s0
::
\$ns0 iff \$NOT1 nq4 & \$NOT1 nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A17,GATE_1:22;
then \$ns0 iff \$q4 & \$NOT1 q3 & \$NOT1 q2 & \$NOT1 q1 by A33,A34,A35,A36,GATE_1:
4;
hence \$ns0 iff \$s8 by A9,GATE_1:22;
::
:: minor loop
:: s2 -> s5
::
\$ns5 iff \$NOT1 nq4 & \$nq3 & \$NOT1 nq2 & \$nq1 by A22,GATE_1:22;
then \$ns5 iff \$NOT1 q4 & \$NOT1 q3 & \$q2 & \$NOT1 q1 by A33,A34,A35,A36,GATE_1:
4;
hence \$ns5 iff \$s2 by A3,GATE_1:22;
::
:: minor loop
:: s5 -> s11
::
\$ns11 iff \$nq4 & \$NOT1 nq3 & \$nq2 & \$nq1 by A28,GATE_1:22;
then \$ns11 iff \$NOT1 q4 & \$q3 & \$NOT1 q2 & \$q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns11 iff \$s5 by A6,GATE_1:22;
::
:: minor loop
:: s11 -> s6
::
\$ns6 iff \$NOT1 nq4 & \$nq3 & \$nq2 & \$NOT1 nq1 by A23,GATE_1:22;
then \$ns6 iff \$q4 & \$NOT1 q3 & \$q2 & \$q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns6 iff \$s11 by A12,GATE_1:22;
::
:: minor loop
:: s6 -> s13
::
\$ns13 iff \$nq4 & \$nq3 & \$NOT1 nq2 & \$nq1 by A30,GATE_1:22;
then \$ns13 iff \$NOT1 q4 & \$q3 & \$q2 & \$NOT1 q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns13 iff \$s6 by A7,GATE_1:22;
::
:: minor loop
:: s13 -> s10
::
\$ns10 iff \$nq4 & \$NOT1 nq3 & \$nq2 & \$NOT1 nq1 by A27,GATE_1:22;
then \$ns10 iff \$q4 & \$q3 & \$NOT1 q2 & \$q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns10 iff \$s13 by A14,GATE_1:22;
::
:: minor loop
:: s10 -> s4
::
\$ns4 iff \$NOT1 nq4 & \$nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A21,GATE_1:22;
then \$ns4 iff \$q4 & \$NOT1 q3 & \$q2 & \$NOT1 q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns4 iff \$s10 by A11,GATE_1:22;
::
:: minor loop
:: s4 -> s9
::
\$ns9 iff \$nq4 & \$NOT1 nq3 & \$NOT1 nq2 & \$nq1 by A26,GATE_1:22;
then \$ns9 iff \$NOT1 q4 & \$q3 & \$NOT1 q2 & \$NOT1 q1 by A33,A34,A35,A36,GATE_1:
4;
hence \$ns9 iff \$s4 by A5,GATE_1:22;
::
:: minor loop
:: s9 -> s2
::
\$ns2 iff \$NOT1 nq4 & \$NOT1 nq3 & \$nq2 & \$NOT1 nq1 by A19,GATE_1:22;
then \$ns2 iff \$q4 & \$NOT1 q3 & \$NOT1 q2 & \$q1 by A33,A34,A35,A36,GATE_1:4;
hence \$ns2 iff \$s9 by A10,GATE_1:22;

end;

:: 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 ::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))
proof
let 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 be set;
assume that A1:(\$s0 iff \$AND4(NOT1 q4, NOT1 q3, NOT1 q2, NOT1 q1)) and
A2: (\$s1 iff \$AND4(NOT1 q4, NOT1 q3, NOT1 q2, q1)) and
A3: (\$s2 iff \$AND4(NOT1 q4, NOT1 q3, q2, NOT1 q1)) and
A4: (\$s3 iff \$AND4(NOT1 q4, NOT1 q3, q2, q1)) and
A5: (\$s4 iff \$AND4(NOT1 q4, q3, NOT1 q2, NOT1 q1)) and
A6: (\$s5 iff \$AND4(NOT1 q4, q3, NOT1 q2, q1)) and
A7: (\$s6 iff \$AND4(NOT1 q4, q3, q2, NOT1 q1)) and
A8: (\$s7 iff \$AND4(NOT1 q4, q3, q2, q1)) and
A9: (\$s8 iff \$AND4( q4, NOT1 q3, NOT1 q2, NOT1 q1)) and
A10:(\$s9 iff \$AND4( q4, NOT1 q3, NOT1 q2, q1)) and
A11:(\$s10 iff \$AND4( q4, NOT1 q3, q2, NOT1 q1)) and
A12:(\$s11 iff \$AND4( q4, NOT1 q3, q2, q1)) and
A13:(\$s12 iff \$AND4( q4, q3, NOT1 q2, NOT1 q1)) and
A14:(\$s13 iff \$AND4( q4, q3, NOT1 q2, q1)) and
A15:(\$s14 iff \$AND4( q4, q3, q2, NOT1 q1)) and
A16:(\$s15 iff \$AND4( q4, q3, q2, q1)) and
A17:(\$ns0 iff \$AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1)) and
A18:(\$ns1 iff \$AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, nq1)) and
A19:(\$ns2 iff \$AND4(NOT1 nq4, NOT1 nq3, nq2, NOT1 nq1)) and
A20:(\$ns3 iff \$AND4(NOT1 nq4, NOT1 nq3, nq2, nq1)) and
A21:(\$ns4 iff \$AND4(NOT1 nq4, nq3, NOT1 nq2, NOT1 nq1)) and
A22:(\$ns5 iff \$AND4(NOT1 nq4, nq3, NOT1 nq2, nq1)) and
A23:(\$ns6 iff \$AND4(NOT1 nq4, nq3, nq2, NOT1 nq1)) and
A24:(\$ns7 iff \$AND4(NOT1 nq4, nq3, nq2, nq1)) and
A25:(\$ns8 iff \$AND4( nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1)) and
A26:(\$ns9 iff \$AND4( nq4, NOT1 nq3, NOT1 nq2, nq1)) and
A27:(\$ns10 iff \$AND4( nq4, NOT1 nq3, nq2, NOT1 nq1)) and
A28:(\$ns11 iff \$AND4( nq4, NOT1 nq3, nq2, nq1)) and
A29:(\$ns12 iff \$AND4( nq4, nq3, NOT1 nq2, NOT1 nq1)) and
A30:(\$ns13 iff \$AND4( nq4, nq3, NOT1 nq2, nq1)) and
A31:(\$ns14 iff \$AND4( nq4, nq3, nq2, NOT1 nq1)) and
A32:(\$ns15 iff \$AND4( nq4, nq3, nq2, nq1)) and
A33:(\$nq1 iff \$AND2(NOT1 q4,R)) and
A34:(\$nq2 iff \$AND2( q1,R)) and
A35:(\$nq3 iff \$AND2( q2,R)) and
A36:(\$nq4 iff \$AND2( q3,R));
::
:: s0 -> s1
::
\$ns1 iff \$NOT1 nq4 & \$NOT1 nq3 & \$NOT1 nq2 & \$nq1 by A18,GATE_1:22;
then \$ns1 iff \$NOT1 q4 & \$R & not(\$q3 & \$R) & not(\$q2 & \$R) & not(\$q1 & \$R)
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns1 iff \$NOT1 q4 & \$NOT1 q3 & \$NOT1 q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns1 iff \$AND2(s0,R) by A1,GATE_1:6,22;
::
:: s1 -> s3
::
\$ns3 iff \$NOT1 nq4 & \$NOT1 nq3 & \$nq2 & \$nq1 by A20,GATE_1:22;
then \$ns3 iff \$NOT1 q4 & \$R & not(\$q3 & \$R) & not(\$q2 & \$R) & \$q1 & \$R
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns3 iff \$NOT1 q4 & \$NOT1 q3 & \$NOT1 q2 & \$q1 & \$R by GATE_1:4;
hence \$ns3 iff \$AND2(s1,R) by A2,GATE_1:6,22;
::
:: s3 -> s7
::
\$ns7 iff \$NOT1 nq4 & \$nq3 & \$nq2 & \$nq1 by A24,GATE_1:22;
then \$ns7 iff \$NOT1 q4 & \$R & not(\$q3 & \$R) & \$q2 & \$R & \$q1 & \$R
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns7 iff \$NOT1 q4 & \$NOT1 q3 & \$q2 & \$q1 & \$R by GATE_1:4;
hence \$ns7 iff \$AND2(s3,R) by A4,GATE_1:6,22;
::
:: s7 -> s15
::
\$ns15 iff \$NOT1 q4 & \$R & \$q3 & \$R & \$q2 & \$R & \$q1 & \$R
by A32,A33,A34,A35,A36,GATE_1:6,22;
hence \$ns15 iff \$AND2(s7,R) by A8,GATE_1:6,22;
::
:: s15 -> s14
::
\$ns14 iff \$nq4 & \$nq3 & \$nq2 & \$NOT1 nq1 by A31,GATE_1:22;
then \$ns14 iff not(\$NOT1 q4 & \$R) & \$q3 & \$R & \$q2 & \$R & \$q1 & \$R
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns14 iff \$q4 & \$q3 & \$q2 & \$q1 & \$R by GATE_1:4;
hence \$ns14 iff \$AND2(s15,R) by A16,GATE_1:6,22;
::
:: s14 -> s12
::
\$ns12 iff \$nq4 & \$nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A29,GATE_1:22;
then \$ns12 iff not(\$NOT1 q4 & \$R) & \$q3 & \$R & \$q2 & \$R & not(\$q1 & \$R)
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns12 iff \$q4 & \$q3 & \$q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns12 iff \$AND2(s14,R) by A15,GATE_1:6,22;
::
:: s12 -> s8
::
\$ns8 iff \$nq4 & \$NOT1 nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A25,GATE_1:22;
then \$ns8 iff not(\$NOT1 q4 & \$R) & \$q3 & \$R & not(\$q2 & \$R) & not(\$q1 & \$R)
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns8 iff \$q4 & \$q3 & \$NOT1 q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns8 iff \$AND2(s12,R) by A13,GATE_1:6,22;
::
:: s8 -> s0
::

\$ns0 iff \$NOT1 nq4 & \$NOT1 nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A17,GATE_1:22;
then \$ns0 iff not(\$NOT1 q4 & \$R) & not(\$q3 & \$R) & not(\$q2 & \$R) & not(\$q1 & \$
R)
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns0 iff (\$q4 & \$NOT1 q3 & \$NOT1 q2 & \$NOT1 q1 & \$R) or not(\$R)
by GATE_1:4;
then \$ns0 iff \$AND2(s8,R) or \$NOT1 R by A9,GATE_1:4,6,22;
hence \$ns0 iff \$OR2(AND2(s8, R),NOT1 R) by GATE_1:7;
::
:: minor loop
:: s2 -> s5
::
\$ns5 iff \$NOT1 nq4 & \$nq3 & \$NOT1 nq2 & \$nq1 by A22,GATE_1:22;
then \$ns5 iff \$NOT1 q4 & \$R & not(\$q3 & \$R) & \$q2 & \$R & not(\$q1 & \$R)
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns5 iff \$NOT1 q4 & \$NOT1 q3 & \$q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns5 iff \$AND2(s2,R) by A3,GATE_1:6,22;
::
:: minor loop
:: s5 -> s11
::
\$ns11 iff \$nq4 & \$NOT1 nq3 & \$nq2 & \$nq1 by A28,GATE_1:22;
then \$ns11 iff \$NOT1 q4 & \$R & \$q3 & \$R & not(\$q2 & \$R) & \$q1 & \$R
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns11 iff \$NOT1 q4 & \$q3 & \$NOT1 q2 & \$q1 & \$R by GATE_1:4;
hence \$ns11 iff \$AND2(s5,R) by A6,GATE_1:6,22;
::
:: minor loop
:: s11 -> s6
::
\$ns6 iff \$NOT1 nq4 & \$nq3 & \$nq2 & \$NOT1 nq1 by A23,GATE_1:22;
then \$ns6 iff not(\$NOT1 q4 & \$R) & not(\$q3 & \$R) & \$q2 & \$R & \$q1 & \$R
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns6 iff \$q4 & \$NOT1 q3 & \$q2 & \$q1 & \$R by GATE_1:4;
hence \$ns6 iff \$AND2(s11,R) by A12,GATE_1:6,22;
::
:: minor loop
:: s6 -> s13
::
\$ns13 iff \$nq4 & \$nq3 & \$NOT1 nq2 & \$nq1 by A30,GATE_1:22;
then \$ns13 iff \$NOT1 q4 & \$R & \$q3 & \$R & \$q2 & \$R & not(\$q1 & \$R)
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns13 iff \$NOT1 q4 & \$q3 & \$q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns13 iff \$AND2(s6,R) by A7,GATE_1:6,22;
::
:: minor loop
:: s13 -> s10
::
\$ns10 iff \$nq4 & \$NOT1 nq3 & \$nq2 & \$NOT1 nq1 by A27,GATE_1:22;
then \$ns10 iff not(\$NOT1 q4 & \$R) & \$q3 & \$R & not(\$q2 & \$R) & \$q1 & \$R
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns10 iff \$q4 & \$q3 & \$NOT1 q2 & \$q1 & \$R by GATE_1:4;
hence \$ns10 iff \$AND2(s13,R) by A14,GATE_1:6,22;
::
:: minor loop
:: s10 -> s4
::
\$ns4 iff \$NOT1 nq4 & \$nq3 & \$NOT1 nq2 & \$NOT1 nq1 by A21,GATE_1:22;
then \$ns4 iff not(\$NOT1 q4 & \$R) & not(\$q3 & \$R) & \$q2 & \$R & not(\$q1 & \$R)
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns4 iff \$q4 & \$NOT1 q3 & \$q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns4 iff \$AND2(s10,R) by A11,GATE_1:6,22;
::
:: minor loop
:: s4 -> s9
::
\$ns9 iff \$nq4 & \$NOT1 nq3 & \$NOT1 nq2 & \$nq1 by A26,GATE_1:22;
then \$ns9 iff \$NOT1 q4 & \$R & \$q3 & \$R & not(\$q2 & \$R) & not(\$q1 & \$R)
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns9 iff \$NOT1 q4 & \$q3 & \$NOT1 q2 & \$NOT1 q1 & \$R by GATE_1:4;
hence \$ns9 iff \$AND2(s4,R) by A5,GATE_1:6,22;
::
:: minor loop
:: s9 -> s2
::
\$ns2 iff \$NOT1 nq4 & \$NOT1 nq3 & \$nq2 & \$NOT1 nq1 by A19,GATE_1:22;
then \$ns2 iff not(\$NOT1 q4 & \$R) & not(\$q3 & \$R) & not(\$q2 & \$R) & \$q1 & \$R
by A33,A34,A35,A36,GATE_1:4,6;
then \$ns2 iff \$q4 & \$NOT1 q3 & \$NOT1 q2 & \$q1 & \$R by GATE_1:4;
hence \$ns2 iff \$AND2(s9,R) by A10,GATE_1:6,22;

end;
```

Back to top