:: Correctness of Johnson Counter Circuits
:: by Yuguang Yang , Wasaki Katsumi , Yasushi Fuwa and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999 Association of Mizar Users

theorem :: GATE_3:1

for s0, s1, s2, s3, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2 being set holds
not ( ( not s0 is empty implies not AND2 (NOT1 q2),(NOT1 q1) is empty ) & ( not AND2 (NOT1 q2),(NOT1 q1) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND2 (NOT1 q2),q1 is empty ) & ( not AND2 (NOT1 q2),q1 is empty implies not s1 is empty ) & ( not s2 is empty implies not AND2 q2,(NOT1 q1) is empty ) & ( not AND2 q2,(NOT1 q1) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND2 q2,q1 is empty ) & ( not AND2 q2,q1 is empty implies not s3 is empty ) & ( not ns0 is empty implies not AND2 (NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND2 (NOT1 nq2),(NOT1 nq1) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND2 (NOT1 nq2),nq1 is empty ) & ( not AND2 (NOT1 nq2),nq1 is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND2 nq2,(NOT1 nq1) is empty ) & ( not AND2 nq2,(NOT1 nq1) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND2 nq2,nq1 is empty ) & ( not AND2 nq2,nq1 is empty implies not ns3 is empty ) & ( not nq1 is empty implies not NOT1 q2 is empty ) & ( not NOT1 q2 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & not ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns0 is empty ) ) )

proof end;

theorem :: GATE_3:2

for s0, s1, s2, s3, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2, R being set holds
not ( ( not s0 is empty implies not AND2 (NOT1 q2),(NOT1 q1) is empty ) & ( not AND2 (NOT1 q2),(NOT1 q1) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND2 (NOT1 q2),q1 is empty ) & ( not AND2 (NOT1 q2),q1 is empty implies not s1 is empty ) & ( not s2 is empty implies not AND2 q2,(NOT1 q1) is empty ) & ( not AND2 q2,(NOT1 q1) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND2 q2,q1 is empty ) & ( not AND2 q2,q1 is empty implies not s3 is empty ) & ( not ns0 is empty implies not AND2 (NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND2 (NOT1 nq2),(NOT1 nq1) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND2 (NOT1 nq2),nq1 is empty ) & ( not AND2 (NOT1 nq2),nq1 is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND2 nq2,(NOT1 nq1) is empty ) & ( not AND2 nq2,(NOT1 nq1) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND2 nq2,nq1 is empty ) & ( not AND2 nq2,nq1 is empty implies not ns3 is empty ) & ( not nq1 is empty implies not AND2 (NOT1 q2),R is empty ) & ( not AND2 (NOT1 q2),R is empty implies not nq1 is empty ) & ( not nq2 is empty implies not AND2 q1,R is empty ) & ( not AND2 q1,R is empty implies not nq2 is empty ) & not ( ( not ns1 is empty implies not AND2 s0,R is empty ) & ( not AND2 s0,R is empty implies not ns1 is empty ) & ( not ns3 is empty implies not AND2 s1,R is empty ) & ( not AND2 s1,R is empty implies not ns3 is empty ) & ( not ns2 is empty implies not AND2 s3,R is empty ) & ( not AND2 s3,R is empty implies not ns2 is empty ) & ( not ns0 is empty implies not OR2 (AND2 s2,R),(NOT1 R) is empty ) & ( not OR2 (AND2 s2,R),(NOT1 R) is empty implies not ns0 is empty ) ) )

proof end;

theorem :: GATE_3:3

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
not ( ( not s0 is empty implies not AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) is empty ) & ( not AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND3 (NOT1 q3),(NOT1 q2),q1 is empty ) & ( not AND3 (NOT1 q3),(NOT1 q2),q1 is empty implies not s1 is empty ) & ( not s2 is empty implies not AND3 (NOT1 q3),q2,(NOT1 q1) is empty ) & ( not AND3 (NOT1 q3),q2,(NOT1 q1) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND3 (NOT1 q3),q2,q1 is empty ) & ( not AND3 (NOT1 q3),q2,q1 is empty implies not s3 is empty ) & ( not s4 is empty implies not AND3 q3,(NOT1 q2),(NOT1 q1) is empty ) & ( not AND3 q3,(NOT1 q2),(NOT1 q1) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND3 q3,(NOT1 q2),q1 is empty ) & ( not AND3 q3,(NOT1 q2),q1 is empty implies not s5 is empty ) & ( not s6 is empty implies not AND3 q3,q2,(NOT1 q1) is empty ) & ( not AND3 q3,q2,(NOT1 q1) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND3 q3,q2,q1 is empty ) & ( not AND3 q3,q2,q1 is empty implies not s7 is empty ) & ( not ns0 is empty implies not AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND3 (NOT1 nq3),(NOT1 nq2),nq1 is empty ) & ( not AND3 (NOT1 nq3),(NOT1 nq2),nq1 is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND3 (NOT1 nq3),nq2,(NOT1 nq1) is empty ) & ( not AND3 (NOT1 nq3),nq2,(NOT1 nq1) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND3 (NOT1 nq3),nq2,nq1 is empty ) & ( not AND3 (NOT1 nq3),nq2,nq1 is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND3 nq3,(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND3 nq3,(NOT1 nq2),(NOT1 nq1) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND3 nq3,(NOT1 nq2),nq1 is empty ) & ( not AND3 nq3,(NOT1 nq2),nq1 is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND3 nq3,nq2,(NOT1 nq1) is empty ) & ( not AND3 nq3,nq2,(NOT1 nq1) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND3 nq3,nq2,nq1 is empty ) & ( not AND3 nq3,nq2,nq1 is empty implies not ns7 is empty ) & ( not nq1 is empty implies not NOT1 q3 is empty ) & ( not NOT1 q3 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 is empty implies not nq3 is empty ) & not ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) ) )

proof end;

theorem :: GATE_3:4

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
not ( ( not s0 is empty implies not AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) is empty ) & ( not AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND3 (NOT1 q3),(NOT1 q2),q1 is empty ) & ( not AND3 (NOT1 q3),(NOT1 q2),q1 is empty implies not s1 is empty ) & ( not s2 is empty implies not AND3 (NOT1 q3),q2,(NOT1 q1) is empty ) & ( not AND3 (NOT1 q3),q2,(NOT1 q1) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND3 (NOT1 q3),q2,q1 is empty ) & ( not AND3 (NOT1 q3),q2,q1 is empty implies not s3 is empty ) & ( not s4 is empty implies not AND3 q3,(NOT1 q2),(NOT1 q1) is empty ) & ( not AND3 q3,(NOT1 q2),(NOT1 q1) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND3 q3,(NOT1 q2),q1 is empty ) & ( not AND3 q3,(NOT1 q2),q1 is empty implies not s5 is empty ) & ( not s6 is empty implies not AND3 q3,q2,(NOT1 q1) is empty ) & ( not AND3 q3,q2,(NOT1 q1) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND3 q3,q2,q1 is empty ) & ( not AND3 q3,q2,q1 is empty implies not s7 is empty ) & ( not ns0 is empty implies not AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND3 (NOT1 nq3),(NOT1 nq2),nq1 is empty ) & ( not AND3 (NOT1 nq3),(NOT1 nq2),nq1 is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND3 (NOT1 nq3),nq2,(NOT1 nq1) is empty ) & ( not AND3 (NOT1 nq3),nq2,(NOT1 nq1) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND3 (NOT1 nq3),nq2,nq1 is empty ) & ( not AND3 (NOT1 nq3),nq2,nq1 is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND3 nq3,(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND3 nq3,(NOT1 nq2),(NOT1 nq1) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND3 nq3,(NOT1 nq2),nq1 is empty ) & ( not AND3 nq3,(NOT1 nq2),nq1 is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND3 nq3,nq2,(NOT1 nq1) is empty ) & ( not AND3 nq3,nq2,(NOT1 nq1) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND3 nq3,nq2,nq1 is empty ) & ( not AND3 nq3,nq2,nq1 is empty implies not ns7 is empty ) & ( not nq1 is empty implies not AND2 (NOT1 q3),R is empty ) & ( not AND2 (NOT1 q3),R is empty implies not nq1 is empty ) & ( not nq2 is empty implies not AND2 q1,R is empty ) & ( not AND2 q1,R is empty implies not nq2 is empty ) & ( not nq3 is empty implies not AND2 q2,R is empty ) & ( not AND2 q2,R is empty implies not nq3 is empty ) & not ( ( not ns1 is empty implies not AND2 s0,R is empty ) & ( not AND2 s0,R is empty implies not ns1 is empty ) & ( not ns3 is empty implies not AND2 s1,R is empty ) & ( not AND2 s1,R is empty implies not ns3 is empty ) & ( not ns7 is empty implies not AND2 s3,R is empty ) & ( not AND2 s3,R is empty implies not ns7 is empty ) & ( not ns6 is empty implies not AND2 s7,R is empty ) & ( not AND2 s7,R is empty implies not ns6 is empty ) & ( not ns4 is empty implies not AND2 s6,R is empty ) & ( not AND2 s6,R is empty implies not ns4 is empty ) & ( not ns0 is empty implies not OR2 (AND2 s4,R),(NOT1 R) is empty ) & ( not OR2 (AND2 s4,R),(NOT1 R) is empty implies not ns0 is empty ) & ( not ns2 is empty implies not AND2 s5,R is empty ) & ( not AND2 s5,R is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 s2,R is empty ) & ( not AND2 s2,R is empty implies not ns5 is empty ) ) )

proof end;

theorem :: GATE_3:5

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
not ( ( not s0 is empty implies not AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1) is empty ) & ( not AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),q1 is empty ) & ( not AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),q1 is empty implies not s1 is empty ) & ( not s2 is empty implies not AND4 (NOT1 q4),(NOT1 q3),q2,(NOT1 q1) is empty ) & ( not AND4 (NOT1 q4),(NOT1 q3),q2,(NOT1 q1) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND4 (NOT1 q4),(NOT1 q3),q2,q1 is empty ) & ( not AND4 (NOT1 q4),(NOT1 q3),q2,q1 is empty implies not s3 is empty ) & ( not s4 is empty implies not AND4 (NOT1 q4),q3,(NOT1 q2),(NOT1 q1) is empty ) & ( not AND4 (NOT1 q4),q3,(NOT1 q2),(NOT1 q1) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND4 (NOT1 q4),q3,(NOT1 q2),q1 is empty ) & ( not AND4 (NOT1 q4),q3,(NOT1 q2),q1 is empty implies not s5 is empty ) & ( not s6 is empty implies not AND4 (NOT1 q4),q3,q2,(NOT1 q1) is empty ) & ( not AND4 (NOT1 q4),q3,q2,(NOT1 q1) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND4 (NOT1 q4),q3,q2,q1 is empty ) & ( not AND4 (NOT1 q4),q3,q2,q1 is empty implies not s7 is empty ) & ( not s8 is empty implies not AND4 q4,(NOT1 q3),(NOT1 q2),(NOT1 q1) is empty ) & ( not AND4 q4,(NOT1 q3),(NOT1 q2),(NOT1 q1) is empty implies not s8 is empty ) & ( not s9 is empty implies not AND4 q4,(NOT1 q3),(NOT1 q2),q1 is empty ) & ( not AND4 q4,(NOT1 q3),(NOT1 q2),q1 is empty implies not s9 is empty ) & ( not s10 is empty implies not AND4 q4,(NOT1 q3),q2,(NOT1 q1) is empty ) & ( not AND4 q4,(NOT1 q3),q2,(NOT1 q1) is empty implies not s10 is empty ) & ( not s11 is empty implies not AND4 q4,(NOT1 q3),q2,q1 is empty ) & ( not AND4 q4,(NOT1 q3),q2,q1 is empty implies not s11 is empty ) & ( not s12 is empty implies not AND4 q4,q3,(NOT1 q2),(NOT1 q1) is empty ) & ( not AND4 q4,q3,(NOT1 q2),(NOT1 q1) is empty implies not s12 is empty ) & ( not s13 is empty implies not AND4 q4,q3,(NOT1 q2),q1 is empty ) & ( not AND4 q4,q3,(NOT1 q2),q1 is empty implies not s13 is empty ) & ( not s14 is empty implies not AND4 q4,q3,q2,(NOT1 q1) is empty ) & ( not AND4 q4,q3,q2,(NOT1 q1) is empty implies not s14 is empty ) & ( not s15 is empty implies not AND4 q4,q3,q2,q1 is empty ) & ( not AND4 q4,q3,q2,q1 is empty implies not s15 is empty ) & ( not ns0 is empty implies not AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1 is empty ) & ( not AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1 is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND4 (NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1) is empty ) & ( not AND4 (NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND4 (NOT1 nq4),(NOT1 nq3),nq2,nq1 is empty ) & ( not AND4 (NOT1 nq4),(NOT1 nq3),nq2,nq1 is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND4 (NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND4 (NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND4 (NOT1 nq4),nq3,(NOT1 nq2),nq1 is empty ) & ( not AND4 (NOT1 nq4),nq3,(NOT1 nq2),nq1 is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND4 (NOT1 nq4),nq3,nq2,(NOT1 nq1) is empty ) & ( not AND4 (NOT1 nq4),nq3,nq2,(NOT1 nq1) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND4 (NOT1 nq4),nq3,nq2,nq1 is empty ) & ( not AND4 (NOT1 nq4),nq3,nq2,nq1 is empty implies not ns7 is empty ) & ( not ns8 is empty implies not AND4 nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND4 nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty implies not ns8 is empty ) & ( not ns9 is empty implies not AND4 nq4,(NOT1 nq3),(NOT1 nq2),nq1 is empty ) & ( not AND4 nq4,(NOT1 nq3),(NOT1 nq2),nq1 is empty implies not ns9 is empty ) & ( not ns10 is empty implies not AND4 nq4,(NOT1 nq3),nq2,(NOT1 nq1) is empty ) & ( not AND4 nq4,(NOT1 nq3),nq2,(NOT1 nq1) is empty implies not ns10 is empty ) & ( not ns11 is empty implies not AND4 nq4,(NOT1 nq3),nq2,nq1 is empty ) & ( not AND4 nq4,(NOT1 nq3),nq2,nq1 is empty implies not ns11 is empty ) & ( not ns12 is empty implies not AND4 nq4,nq3,(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND4 nq4,nq3,(NOT1 nq2),(NOT1 nq1) is empty implies not ns12 is empty ) & ( not ns13 is empty implies not AND4 nq4,nq3,(NOT1 nq2),nq1 is empty ) & ( not AND4 nq4,nq3,(NOT1 nq2),nq1 is empty implies not ns13 is empty ) & ( not ns14 is empty implies not AND4 nq4,nq3,nq2,(NOT1 nq1) is empty ) & ( not AND4 nq4,nq3,nq2,(NOT1 nq1) is empty implies not ns14 is empty ) & ( not ns15 is empty implies not AND4 nq4,nq3,nq2,nq1 is empty ) & ( not AND4 nq4,nq3,nq2,nq1 is empty implies not ns15 is empty ) & ( not nq1 is empty implies not NOT1 q4 is empty ) & ( not NOT1 q4 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 is empty implies not nq3 is empty ) & ( not nq4 is empty implies not q3 is empty ) & ( not q3 is empty implies not nq4 is empty ) & not ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns15 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns15 is empty ) & ( not ns14 is empty implies not s15 is empty ) & ( not s15 is empty implies not ns14 is empty ) & ( not ns12 is empty implies not s14 is empty ) & ( not s14 is empty implies not ns12 is empty ) & ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) ) )

proof end;

theorem :: GATE_3:6

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

proof end;