GATE_3

:: Correctness of Johnson Counter Circuits
::  by Yuguang Yang , Wasaki Katsumi , Yasushi Fuwa and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999-2026 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;
 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 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)
proof
  let s0,s1,s2,s3,ns0,ns1,ns2,ns3,q1,q2,nq1,nq2 be set;
  assume that
A1: s0 is not empty iff AND2(NOT1 q2,NOT1 q1) is not empty and
A2: s1 is not empty iff AND2(NOT1 q2,q1) is not empty and
A3: s2 is not empty iff AND2(q2,NOT1 q1) is not empty and
A4: s3 is not empty iff AND2(q2,q1) is not empty and
A5: ns0 is not empty iff AND2(NOT1 nq2,NOT1 nq1) is not empty and
A6: ns1 is not empty iff AND2(NOT1 nq2,nq1) is not empty and
A7: ns2 is not empty iff AND2(nq2,NOT1 nq1) is not empty and
A8: ns3 is not empty iff AND2(nq2,nq1) is not empty and
A9: ( nq1 is not empty iff NOT1 q2 is not empty)&( nq2 is not empty iff
  q1 is not empty);
  thus ns1 is not empty iff s0 is not empty by A1,A6,A9;
  thus ns3 is not empty iff s1 is not empty by A2,A8,A9;
  ns2 is not empty iff q2 is not empty & q1 is not empty by A7,A9;
  hence ns2 is not empty iff s3 is not empty by A4;
  ns0 is not empty iff q2 is not empty & NOT1 q1 is not empty by A5,A9;
  hence thesis by A3;
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 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)
proof
  let s0,s1,s2,s3,ns0,ns1,ns2,ns3,q1,q2,nq1,nq2,R be set;
  assume that
A1: s0 is not empty iff AND2(NOT1 q2,NOT1 q1) is not empty and
A2: s1 is not empty iff AND2(NOT1 q2,q1) is not empty and
A3: s2 is not empty iff AND2(q2,NOT1 q1) is not empty and
A4: s3 is not empty iff AND2(q2,q1) is not empty and
A5: ns0 is not empty iff AND2(NOT1 nq2,NOT1 nq1) is not empty and
A6: ns1 is not empty iff AND2(NOT1 nq2,nq1) is not empty and
A7: ns2 is not empty iff AND2(nq2,NOT1 nq1) is not empty and
A8: ns3 is not empty iff AND2(nq2,nq1) is not empty and
A9: ( nq1 is not empty iff AND2(NOT1 q2,R) is not empty)&( nq2 is not
  empty iff AND2( q1,R) is not empty);
  ns1 is not empty iff NOT1 q2 is not empty & R is not empty & not(q1 is
  not empty & R is not empty) by A6,A9;
  hence ns1 is not empty iff AND2(s0,R) is not empty by A1;
  ns3 is not empty iff NOT1 q2 is not empty & q1 is not empty & R is not
  empty by A8,A9;
  hence ns3 is not empty iff AND2(s1,R) is not empty by A2;
  ns2 is not empty iff not(NOT1 q2 is not empty & R is not empty) & q1 is
  not empty & R is not empty by A7,A9;
  then
  ns2 is not empty iff q2 is not empty & q1 is not empty & R is not empty;
  hence ns2 is not empty iff AND2(s3,R) is not empty by A4;
  ns0 is not empty iff not(NOT1 q2 is not empty & R is not empty) & not(
  q1 is not empty & R is not empty) by A5,A9;
  then ns0 is not empty iff q2 is not empty & NOT1 q1 is not empty & R is not
  empty or not R is not empty;
  hence thesis by A3;
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 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)
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 not empty iff AND3(NOT1 q3,NOT1 q2,NOT1 q1) is not empty and
A2: s1 is not empty iff AND3(NOT1 q3,NOT1 q2,q1) is not empty and
A3: s2 is not empty iff AND3(NOT1 q3,q2,NOT1 q1) is not empty and
A4: s3 is not empty iff AND3(NOT1 q3,q2,q1) is not empty and
A5: s4 is not empty iff AND3(q3,NOT1 q2,NOT1 q1) is not empty and
A6: s5 is not empty iff AND3(q3,NOT1 q2,q1) is not empty and
A7: s6 is not empty iff AND3(q3,q2,NOT1 q1) is not empty and
A8: s7 is not empty iff AND3(q3,q2,q1) is not empty and
A9: ns0 is not empty iff AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1) is not empty and
A10: ns1 is not empty iff AND3(NOT1 nq3,NOT1 nq2,nq1) is not empty and
A11: ns2 is not empty iff AND3(NOT1 nq3,nq2,NOT1 nq1) is not empty and
A12: ns3 is not empty iff AND3(NOT1 nq3,nq2,nq1) is not empty and
A13: ns4 is not empty iff AND3(nq3,NOT1 nq2,NOT1 nq1) is not empty and
A14: ns5 is not empty iff AND3(nq3,NOT1 nq2,nq1) is not empty and
A15: ns6 is not empty iff AND3(nq3,nq2,NOT1 nq1) is not empty and
A16: ns7 is not empty iff AND3(nq3,nq2,nq1) is not empty and
A17: ( 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);
  thus ns1 is not empty iff s0 is not empty by A1,A10,A17;
  thus ns3 is not empty iff s1 is not empty by A2,A12,A17;
  thus ns7 is not empty iff s3 is not empty by A4,A16,A17;
  ns6 is not empty iff q3 is not empty & q2 is not empty & q1 is not
  empty by A15,A17;
  hence ns6 is not empty iff s7 is not empty by A8;
  ns4 is not empty iff q3 is not empty & q2 is not empty & NOT1 q1 is not
  empty by A13,A17;
  hence ns4 is not empty iff s6 is not empty by A7;
  ns0 is not empty iff q3 is not empty & NOT1 q2 is not empty & NOT1 q1
  is not empty by A9,A17;
  hence ns0 is not empty iff s4 is not empty by A5;
  ns2 is not empty iff q3 is not empty & NOT1 q2 is not empty & q1 is not
  empty by A11,A17;
  hence ns2 is not empty iff s5 is not empty by A6;
  thus thesis by A3,A14,A17;
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 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)
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 not empty iff AND3(NOT1 q3,NOT1 q2,NOT1 q1) is not empty and
A2: s1 is not empty iff AND3(NOT1 q3,NOT1 q2,q1) is not empty and
A3: s2 is not empty iff AND3(NOT1 q3,q2,NOT1 q1) is not empty and
A4: s3 is not empty iff AND3(NOT1 q3,q2,q1) is not empty and
A5: s4 is not empty iff AND3(q3,NOT1 q2,NOT1 q1) is not empty and
A6: s5 is not empty iff AND3(q3,NOT1 q2,q1) is not empty and
A7: s6 is not empty iff AND3(q3,q2,NOT1 q1) is not empty and
A8: s7 is not empty iff AND3(q3,q2,q1) is not empty and
A9: ns0 is not empty iff AND3(NOT1 nq3,NOT1 nq2,NOT1 nq1) is not empty and
A10: ns1 is not empty iff AND3(NOT1 nq3,NOT1 nq2,nq1) is not empty and
A11: ns2 is not empty iff AND3(NOT1 nq3,nq2,NOT1 nq1) is not empty and
A12: ns3 is not empty iff AND3(NOT1 nq3,nq2,nq1) is not empty and
A13: ns4 is not empty iff AND3(nq3,NOT1 nq2,NOT1 nq1) is not empty and
A14: ns5 is not empty iff AND3(nq3,NOT1 nq2,nq1) is not empty and
A15: ns6 is not empty iff AND3(nq3,nq2,NOT1 nq1) is not empty and
A16: ns7 is not empty iff AND3(nq3,nq2,nq1) is not empty and
A17: ( 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);
  ns1 is not empty iff NOT1 q3 is not empty & R is not empty & not(q2 is
not empty & R is not empty) & not(q1 is not empty & R is not empty) by A10,A17;
  hence ns1 is not empty iff AND2(s0,R) is not empty by A1;
  ns3 is not empty iff NOT1 q3 is not empty & R is not empty & not(q2 is
  not empty & R is not empty) & q1 is not empty & R is not empty by A12,A17;
  hence ns3 is not empty iff AND2(s1,R) is not empty by A2;
  ns7 is not empty iff NOT1 q3 is not empty & R is not empty & q2 is not
  empty & R is not empty & q1 is not empty & R is not empty by A16,A17;
  hence ns7 is not empty iff AND2(s3,R) is not empty by A4;
  ns6 is not empty iff not(NOT1 q3 is not empty & R is not empty) & q2 is
  not empty & R is not empty & q1 is not empty & R is not empty by A15,A17;
  then ns6 is not empty iff q3 is not empty & q2 is not empty & q1 is not
  empty & R is not empty;
  hence ns6 is not empty iff AND2(s7,R) is not empty by A8;
  ns4 is not empty iff not(NOT1 q3 is not empty & R is not empty) & q2 is
not empty & R is not empty & not(q1 is not empty & R is not empty) by A13,A17;
  then
  ns4 is not empty iff q3 is not empty & q2 is not empty & NOT1 q1 is not
  empty & R is not empty;
  hence ns4 is not empty iff AND2(s6,R) is not empty by A7;
  ns0 is not empty iff not(NOT1 q3 is not empty & R is not empty) & not(
q2 is not empty & R is not empty) & not(q1 is not empty & R is not empty) by A9
,A17;
  then ns0 is not empty iff q3 is not empty & NOT1 q2 is not empty & NOT1 q1
  is not empty & R is not empty or not(R) is not empty;
  hence ns0 is not empty iff OR2(AND2(s4, R),NOT1 R) is not empty by A5;
  ns2 is not empty iff not(NOT1 q3 is not empty & R is not empty) & not(
q2 is not empty & R is not empty) & q1 is not empty & R is not empty by A11,A17
  ;
  then
  ns2 is not empty iff q3 is not empty & NOT1 q2 is not empty & q1 is not
  empty & R is not empty;
  hence ns2 is not empty iff AND2(s5,R) is not empty by A6;
  ns5 is not empty iff NOT1 q3 is not empty & R is not empty & q2 is not
  empty & R is not empty & not(q1 is not empty & R is not empty) by A14,A17;
  hence thesis by A3;
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 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)
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 is not empty iff AND4(NOT1 q4, NOT1 q3, NOT1 q2, NOT1 q1) is not
  empty and
A2: s1 is not empty iff AND4(NOT1 q4, NOT1 q3, NOT1 q2, q1) is not empty and
A3: s2 is not empty iff AND4(NOT1 q4, NOT1 q3, q2, NOT1 q1) is not empty and
A4: s3 is not empty iff AND4(NOT1 q4, NOT1 q3, q2, q1) is not empty and
A5: s4 is not empty iff AND4(NOT1 q4, q3, NOT1 q2, NOT1 q1) is not empty and
A6: s5 is not empty iff AND4(NOT1 q4, q3, NOT1 q2, q1) is not empty and
A7: s6 is not empty iff AND4(NOT1 q4, q3, q2, NOT1 q1) is not empty and
A8: s7 is not empty iff AND4(NOT1 q4, q3, q2, q1) is not empty and
A9: s8 is not empty iff AND4( q4, NOT1 q3, NOT1 q2, NOT1 q1) is not empty and
A10: s9 is not empty iff AND4( q4, NOT1 q3, NOT1 q2, q1) is not empty and
A11: s10 is not empty iff AND4( q4, NOT1 q3, q2, NOT1 q1) is not empty and
A12: s11 is not empty iff AND4( q4, NOT1 q3, q2, q1) is not empty and
A13: s12 is not empty iff AND4( q4, q3, NOT1 q2, NOT1 q1) is not empty and
A14: s13 is not empty iff AND4( q4, q3, NOT1 q2, q1) is not empty and
A15: s14 is not empty iff AND4( q4, q3, q2, NOT1 q1) is not empty and
A16: s15 is not empty iff AND4( q4, q3, q2, q1) is not empty and
A17: ns0 is not empty iff AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1)
  is not empty and
A18: ns1 is not empty iff AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, nq1) is not
  empty and
A19: ns2 is not empty iff AND4(NOT1 nq4, NOT1 nq3, nq2, NOT1 nq1) is not
  empty and
A20: ns3 is not empty iff AND4(NOT1 nq4, NOT1 nq3, nq2, nq1) is not empty and
A21: ns4 is not empty iff AND4(NOT1 nq4, nq3, NOT1 nq2, NOT1 nq1) is not
  empty and
A22: ns5 is not empty iff AND4(NOT1 nq4, nq3, NOT1 nq2, nq1) is not empty and
A23: ns6 is not empty iff AND4(NOT1 nq4, nq3, nq2, NOT1 nq1) is not empty and
A24: ns7 is not empty iff AND4(NOT1 nq4, nq3, nq2, nq1) is not empty and
A25: ns8 is not empty iff AND4( nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1) is
  not empty and
A26: ns9 is not empty iff AND4( nq4, NOT1 nq3, NOT1 nq2, nq1) is not empty and
A27: ns10 is not empty iff AND4( nq4, NOT1 nq3, nq2, NOT1 nq1) is not empty and
A28: ns11 is not empty iff AND4( nq4, NOT1 nq3, nq2, nq1) is not empty and
A29: ns12 is not empty iff AND4( nq4, nq3, NOT1 nq2, NOT1 nq1) is not empty and
A30: ns13 is not empty iff AND4( nq4, nq3, NOT1 nq2, nq1) is not empty and
A31: ns14 is not empty iff AND4( nq4, nq3, nq2, NOT1 nq1) is not empty and
A32: ns15 is not empty iff AND4( nq4, nq3, nq2, nq1) is not empty and
A33: ( 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);
  thus ns1 is not empty iff s0 is not empty by A1,A18,A33,GATE_1:20;
  thus ns3 is not empty iff s1 is not empty by A2,A20,A33,GATE_1:20;
  thus ns7 is not empty iff s3 is not empty by A4,A24,A33,GATE_1:20;
  thus ns15 is not empty iff s7 is not empty by A8,A32,A33,GATE_1:20;
  ns14 is not empty iff q4 is not empty & q3 is not empty & q2 is not
  empty & q1 is not empty by A31,A33,GATE_1:20;
  hence ns14 is not empty iff s15 is not empty by A16,GATE_1:20;
  ns12 is not empty iff q4 is not empty & q3 is not empty & q2 is not
  empty & NOT1 q1 is not empty by A29,A33,GATE_1:20;
  hence ns12 is not empty iff s14 is not empty by A15,GATE_1:20;
  ns8 is not empty iff q4 is not empty & q3 is not empty & NOT1 q2 is not
  empty & NOT1 q1 is not empty by A25,A33,GATE_1:20;
  hence ns8 is not empty iff s12 is not empty by A13,GATE_1:20;
  ns0 is not empty iff q4 is not empty & NOT1 q3 is not empty & NOT1 q2
  is not empty & NOT1 q1 is not empty by A17,A33,GATE_1:20;
  hence ns0 is not empty iff s8 is not empty by A9,GATE_1:20;
  thus ns5 is not empty iff s2 is not empty by A3,A22,A33,GATE_1:20;
  thus ns11 is not empty iff s5 is not empty by A6,A28,A33,GATE_1:20;
  ns6 is not empty iff q4 is not empty & NOT1 q3 is not empty & q2 is not
  empty & q1 is not empty by A23,A33,GATE_1:20;
  hence ns6 is not empty iff s11 is not empty by A12,GATE_1:20;
  thus ns13 is not empty iff s6 is not empty by A7,A30,A33,GATE_1:20;
  ns10 is not empty iff q4 is not empty & q3 is not empty & NOT1 q2 is
  not empty & q1 is not empty by A27,A33,GATE_1:20;
  hence ns10 is not empty iff s13 is not empty by A14,GATE_1:20;
  ns4 is not empty iff q4 is not empty & NOT1 q3 is not empty & q2 is not
  empty & NOT1 q1 is not empty by A21,A33,GATE_1:20;
  hence ns4 is not empty iff s10 is not empty by A11,GATE_1:20;
  thus ns9 is not empty iff s4 is not empty by A5,A26,A33,GATE_1:20;
  ns2 is not empty iff q4 is not empty & NOT1 q3 is not empty & NOT1 q2
  is not empty & q1 is not empty by A19,A33,GATE_1:20;
  hence thesis by A10,GATE_1:20;
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 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)
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 is not empty iff AND4(NOT1 q4, NOT1 q3, NOT1 q2, NOT1 q1) is not
  empty and
A2: s1 is not empty iff AND4(NOT1 q4, NOT1 q3, NOT1 q2, q1) is not empty and
A3: s2 is not empty iff AND4(NOT1 q4, NOT1 q3, q2, NOT1 q1) is not empty and
A4: s3 is not empty iff AND4(NOT1 q4, NOT1 q3, q2, q1) is not empty and
A5: s4 is not empty iff AND4(NOT1 q4, q3, NOT1 q2, NOT1 q1) is not empty and
A6: s5 is not empty iff AND4(NOT1 q4, q3, NOT1 q2, q1) is not empty and
A7: s6 is not empty iff AND4(NOT1 q4, q3, q2, NOT1 q1) is not empty and
A8: s7 is not empty iff AND4(NOT1 q4, q3, q2, q1) is not empty and
A9: s8 is not empty iff AND4( q4, NOT1 q3, NOT1 q2, NOT1 q1) is not empty and
A10: s9 is not empty iff AND4( q4, NOT1 q3, NOT1 q2, q1) is not empty and
A11: s10 is not empty iff AND4( q4, NOT1 q3, q2, NOT1 q1) is not empty and
A12: s11 is not empty iff AND4( q4, NOT1 q3, q2, q1) is not empty and
A13: s12 is not empty iff AND4( q4, q3, NOT1 q2, NOT1 q1) is not empty and
A14: s13 is not empty iff AND4( q4, q3, NOT1 q2, q1) is not empty and
A15: s14 is not empty iff AND4( q4, q3, q2, NOT1 q1) is not empty and
A16: s15 is not empty iff AND4( q4, q3, q2, q1) is not empty and
A17: ns0 is not empty iff AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1)
  is not empty and
A18: ns1 is not empty iff AND4(NOT1 nq4, NOT1 nq3, NOT1 nq2, nq1) is not
  empty and
A19: ns2 is not empty iff AND4(NOT1 nq4, NOT1 nq3, nq2, NOT1 nq1) is not
  empty and
A20: ns3 is not empty iff AND4(NOT1 nq4, NOT1 nq3, nq2, nq1) is not empty and
A21: ns4 is not empty iff AND4(NOT1 nq4, nq3, NOT1 nq2, NOT1 nq1) is not
  empty and
A22: ns5 is not empty iff AND4(NOT1 nq4, nq3, NOT1 nq2, nq1) is not empty and
A23: ns6 is not empty iff AND4(NOT1 nq4, nq3, nq2, NOT1 nq1) is not empty and
A24: ns7 is not empty iff AND4(NOT1 nq4, nq3, nq2, nq1) is not empty and
A25: ns8 is not empty iff AND4( nq4, NOT1 nq3, NOT1 nq2, NOT1 nq1) is
  not empty and
A26: ns9 is not empty iff AND4( nq4, NOT1 nq3, NOT1 nq2, nq1) is not empty and
A27: ns10 is not empty iff AND4( nq4, NOT1 nq3, nq2, NOT1 nq1) is not empty and
A28: ns11 is not empty iff AND4( nq4, NOT1 nq3, nq2, nq1) is not empty and
A29: ns12 is not empty iff AND4( nq4, nq3, NOT1 nq2, NOT1 nq1) is not empty and
A30: ns13 is not empty iff AND4( nq4, nq3, NOT1 nq2, nq1) is not empty and
A31: ns14 is not empty iff AND4( nq4, nq3, nq2, NOT1 nq1) is not empty and
A32: ns15 is not empty iff AND4( nq4, nq3, nq2, nq1) is not empty and
A33: ( 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);
  ns1 is not empty iff NOT1 q4 is not empty & R is not empty & not(q3 is
not empty & R is not empty) & not(q2 is not empty & R is not empty) & not(q1 is
  not empty & R is not empty) by A18,A33,GATE_1:20;
  hence ns1 is not empty iff AND2(s0,R) is not empty by A1,GATE_1:20;
  ns3 is not empty iff NOT1 q4 is not empty & R is not empty & not(q3 is
not empty & R is not empty) & not(q2 is not empty & R is not empty) & q1 is not
  empty & R is not empty by A20,A33,GATE_1:20;
  hence ns3 is not empty iff AND2(s1,R) is not empty by A2,GATE_1:20;
  ns7 is not empty iff NOT1 q4 is not empty & R is not empty & not(q3 is
  not empty & R is not empty) & q2 is not empty & R is not empty & q1 is not
  empty & R is not empty by A24,A33,GATE_1:20;
  hence ns7 is not empty iff AND2(s3,R) is not empty by A4,GATE_1:20;
  ns15 is not empty iff NOT1 q4 is not empty & R is not empty & q3 is not
empty & R is not empty & q2 is not empty & R is not empty & q1 is not empty & R
  is not empty by A32,A33,GATE_1:20;
  hence ns15 is not empty iff AND2(s7,R) is not empty by A8,GATE_1:20;
  ns14 is not empty iff not(NOT1 q4 is not empty & R is not empty) & q3
  is not empty & R is not empty & q2 is not empty & R is not empty & q1 is not
  empty & R is not empty by A31,A33,GATE_1:20;
  then ns14 is not empty iff q4 is not empty & q3 is not empty & q2 is not
  empty & q1 is not empty & R is not empty;
  hence ns14 is not empty iff AND2(s15,R) is not empty by A16,GATE_1:20;
  ns12 is not empty iff not(NOT1 q4 is not empty & R is not empty) & q3
  is not empty & R is not empty & q2 is not empty & R is not empty & not(q1 is
  not empty & R is not empty) by A29,A33,GATE_1:20;
  then ns12 is not empty iff q4 is not empty & q3 is not empty & q2 is not
  empty & NOT1 q1 is not empty & R is not empty;
  hence ns12 is not empty iff AND2(s14,R) is not empty by A15,GATE_1:20;
  ns8 is not empty iff not(NOT1 q4 is not empty & R is not empty) & q3 is
not empty & R is not empty & not(q2 is not empty & R is not empty) & not(q1 is
  not empty & R is not empty) by A25,A33,GATE_1:20;
  then
  ns8 is not empty iff q4 is not empty & q3 is not empty & NOT1 q2 is not
  empty & NOT1 q1 is not empty & R is not empty;
  hence ns8 is not empty iff AND2(s12,R) is not empty by A13,GATE_1:20;
  ns0 is not empty iff not(NOT1 q4 is not empty & R is not empty) & not(
q3 is not empty & R is not empty) & not(q2 is not empty & R is not empty) & not
  (q1 is not empty & R is not empty) by A17,A33,GATE_1:20;
  then ns0 is not empty iff q4 is not empty & NOT1 q3 is not empty & NOT1 q2
  is not empty & NOT1 q1 is not empty & R is not empty or not(R) is not empty;
  hence ns0 is not empty iff OR2(AND2(s8, R),NOT1 R) is not empty by A9,
GATE_1:20;
  ns5 is not empty iff NOT1 q4 is not empty & R is not empty & not(q3 is
not empty & R is not empty) & q2 is not empty & R is not empty & not(q1 is not
  empty & R is not empty) by A22,A33,GATE_1:20;
  hence ns5 is not empty iff AND2(s2,R) is not empty by A3,GATE_1:20;
  ns11 is not empty iff NOT1 q4 is not empty & R is not empty & q3 is not
  empty & R is not empty & not(q2 is not empty & R is not empty) & q1 is not
  empty & R is not empty by A28,A33,GATE_1:20;
  hence ns11 is not empty iff AND2(s5,R) is not empty by A6,GATE_1:20;
  ns6 is not empty iff not(NOT1 q4 is not empty & R is not empty) & not(
  q3 is not empty & R is not empty) & q2 is not empty & R is not empty & q1 is
  not empty & R is not empty by A23,A33,GATE_1:20;
  then
  ns6 is not empty iff q4 is not empty & NOT1 q3 is not empty & q2 is not
  empty & q1 is not empty & R is not empty;
  hence ns6 is not empty iff AND2(s11,R) is not empty by A12,GATE_1:20;
  ns13 is not empty iff NOT1 q4 is not empty & R is not empty & q3 is not
empty & R is not empty & q2 is not empty & R is not empty & not(q1 is not empty
  & R is not empty) by A30,A33,GATE_1:20;
  hence ns13 is not empty iff AND2(s6,R) is not empty by A7,GATE_1:20;
  ns10 is not empty iff not(NOT1 q4 is not empty & R is not empty) & q3
  is not empty & R is not empty & not(q2 is not empty & R is not empty) & q1 is
  not empty & R is not empty by A27,A33,GATE_1:20;
  then ns10 is not empty iff q4 is not empty & q3 is not empty & NOT1 q2 is
  not empty & q1 is not empty & R is not empty;
  hence ns10 is not empty iff AND2(s13,R) is not empty by A14,GATE_1:20;
  ns4 is not empty iff not(NOT1 q4 is not empty & R is not empty) & not(
  q3 is not empty & R is not empty) & q2 is not empty & R is not empty & not(q1
  is not empty & R is not empty) by A21,A33,GATE_1:20;
  then
  ns4 is not empty iff q4 is not empty & NOT1 q3 is not empty & q2 is not
  empty & NOT1 q1 is not empty & R is not empty;
  hence ns4 is not empty iff AND2(s10,R) is not empty by A11,GATE_1:20;
  ns9 is not empty iff NOT1 q4 is not empty & R is not empty & q3 is not
empty & R is not empty & not(q2 is not empty & R is not empty) & not(q1 is not
  empty & R is not empty) by A26,A33,GATE_1:20;
  hence ns9 is not empty iff AND2(s4,R) is not empty by A5,GATE_1:20;
  ns2 is not empty iff not(NOT1 q4 is not empty & R is not empty) & not(
q3 is not empty & R is not empty) & not(q2 is not empty & R is not empty) & q1
  is not empty & R is not empty by A19,A33,GATE_1:20;
  then ns2 is not empty iff q4 is not empty & NOT1 q3 is not empty & NOT1 q2
  is not empty & q1 is not empty & R is not empty;
  hence thesis by A10,GATE_1:20;
end;