GATE_2

:: Correctness of Binary 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;
 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;