begin
theorem
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 ) ) )
theorem
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 ) ) )
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
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 ) ) )
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
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 ) ) )
theorem
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 ) ) )
theorem
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 ) ) )