begin
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 q1 is
empty ) & ( not
NOT1 q1 is
empty implies not
nq1 is
empty ) & ( not
nq2 is
empty implies not
XOR2 q1,
q2 is
empty ) & ( not
XOR2 q1,
q2 is
empty implies not
nq2 is
empty ) & ( not
nq3 is
empty implies not
OR2 (AND2 q3,(NOT1 q1)),
(AND2 q1,(XOR2 q2,q3)) is
empty ) & ( not
OR2 (AND2 q3,(NOT1 q1)),
(AND2 q1,(XOR2 q2,q3)) 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
ns2 is
empty implies not
s1 is
empty ) & ( not
s1 is
empty implies not
ns2 is
empty ) & ( not
ns3 is
empty implies not
s2 is
empty ) & ( not
s2 is
empty implies not
ns3 is
empty ) & ( not
ns4 is
empty implies not
s3 is
empty ) & ( not
s3 is
empty implies not
ns4 is
empty ) & ( not
ns5 is
empty implies not
s4 is
empty ) & ( not
s4 is
empty implies not
ns5 is
empty ) & ( not
ns6 is
empty implies not
s5 is
empty ) & ( not
s5 is
empty implies not
ns6 is
empty ) & ( not
ns7 is
empty implies not
s6 is
empty ) & ( not
s6 is
empty implies not
ns7 is
empty ) & ( not
ns0 is
empty implies not
s7 is
empty ) & ( not
s7 is
empty implies not
ns0 is
empty ) ) )
theorem
for
a,
d,
b,
c being
set holds
( not
AND3 (AND2 a,d),
(AND2 b,d),
(AND2 c,d) is
empty iff not
AND2 (AND3 a,b,c),
d is
empty )
theorem
for
a,
b,
c,
d being
set holds
( (
AND2 a,
b is
empty implies not
OR2 (NOT1 a),
(NOT1 b) is
empty ) & ( not
OR2 (NOT1 a),
(NOT1 b) is
empty implies
AND2 a,
b is
empty ) & ( not
OR2 a,
b is
empty & not
OR2 c,
b is
empty implies not
OR2 (AND2 a,c),
b is
empty ) & ( not
OR2 (AND2 a,c),
b is
empty implies ( not
OR2 a,
b is
empty & not
OR2 c,
b is
empty ) ) & ( not
OR2 a,
b is
empty & not
OR2 c,
b is
empty & not
OR2 d,
b is
empty implies not
OR2 (AND3 a,c,d),
b is
empty ) & ( not
OR2 (AND3 a,c,d),
b is
empty implies ( not
OR2 a,
b is
empty & not
OR2 c,
b is
empty & not
OR2 d,
b is
empty ) ) & not ( not
OR2 a,
b is
empty & ( not
a is
empty implies not
c is
empty ) & ( not
c is
empty implies not
a is
empty ) &
OR2 c,
b 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 q1),
R is
empty ) & ( not
AND2 (NOT1 q1),
R is
empty implies not
nq1 is
empty ) & ( not
nq2 is
empty implies not
AND2 (XOR2 q1,q2),
R is
empty ) & ( not
AND2 (XOR2 q1,q2),
R is
empty implies not
nq2 is
empty ) & ( not
nq3 is
empty implies not
AND2 (OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3))),
R is
empty ) & ( not
AND2 (OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3))),
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
ns2 is
empty implies not
AND2 s1,
R is
empty ) & ( not
AND2 s1,
R is
empty implies not
ns2 is
empty ) & ( not
ns3 is
empty implies not
AND2 s2,
R is
empty ) & ( not
AND2 s2,
R is
empty implies not
ns3 is
empty ) & ( not
ns4 is
empty implies not
AND2 s3,
R is
empty ) & ( not
AND2 s3,
R is
empty implies not
ns4 is
empty ) & ( not
ns5 is
empty implies not
AND2 s4,
R is
empty ) & ( not
AND2 s4,
R is
empty implies not
ns5 is
empty ) & ( not
ns6 is
empty implies not
AND2 s5,
R is
empty ) & ( not
AND2 s5,
R is
empty implies not
ns6 is
empty ) & ( not
ns7 is
empty implies not
AND2 s6,
R is
empty ) & ( not
AND2 s6,
R is
empty implies not
ns7 is
empty ) & ( not
ns0 is
empty implies not
OR2 s7,
(NOT1 R) is
empty ) & ( not
OR2 s7,
(NOT1 R) is
empty implies not
ns0 is
empty ) ) )