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 ; 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 ) ) )
assume that
A1:
( not s0 is empty iff not AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) is empty )
and
A2:
( not s1 is empty iff not AND3 (NOT1 q3),(NOT1 q2),q1 is empty )
and
A3:
( not s2 is empty iff not AND3 (NOT1 q3),q2,(NOT1 q1) is empty )
and
A4:
( not s3 is empty iff not AND3 (NOT1 q3),q2,q1 is empty )
and
A5:
( not s4 is empty iff not AND3 q3,(NOT1 q2),(NOT1 q1) is empty )
and
A6:
( not s5 is empty iff not AND3 q3,(NOT1 q2),q1 is empty )
and
A7:
( not s6 is empty iff not AND3 q3,q2,(NOT1 q1) is empty )
and
A8:
( not s7 is empty iff not AND3 q3,q2,q1 is empty )
and
A9:
( not ns0 is empty iff not AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty )
and
A10:
( not ns1 is empty iff not AND3 (NOT1 nq3),(NOT1 nq2),nq1 is empty )
and
A11:
( not ns2 is empty iff not AND3 (NOT1 nq3),nq2,(NOT1 nq1) is empty )
and
A12:
( not ns3 is empty iff not AND3 (NOT1 nq3),nq2,nq1 is empty )
and
A13:
( not ns4 is empty iff not AND3 nq3,(NOT1 nq2),(NOT1 nq1) is empty )
and
A14:
( not ns5 is empty iff not AND3 nq3,(NOT1 nq2),nq1 is empty )
and
A15:
( not ns6 is empty iff not AND3 nq3,nq2,(NOT1 nq1) is empty )
and
A16:
( not ns7 is empty iff not AND3 nq3,nq2,nq1 is empty )
and
A17:
( not nq1 is empty iff not AND2 (NOT1 q1),R is empty )
and
A18:
( not nq2 is empty iff not AND2 (XOR2 q1,q2),R is empty )
and
A19:
( not nq3 is empty iff not AND2 (OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3))),R is empty )
; ( ( 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 ) )
( not ns1 is empty iff ( nq3 is empty & ( XOR2 q1,q2 is empty or R is empty ) & q1 is empty & not R is empty ) )
by A10, A17, A18;
then
( not ns1 is empty iff ( ( q3 is empty or NOT1 q1 is empty ) & ( q1 is empty or XOR2 q2,q3 is empty ) & q2 is empty & q1 is empty & not R is empty ) )
by A19;
hence
( not ns1 is empty iff not AND2 s0,R is empty )
by A1; ( ( 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 ) )
( not ns2 is empty iff ( nq3 is empty & not XOR2 q1,q2 is empty & not R is empty & ( NOT1 q1 is empty or R is empty ) ) )
by A11, A17, A18;
then
( not ns2 is empty iff ( nq3 is empty & not XOR2 q1,q2 is empty & not R is empty & not q1 is empty ) )
;
then
( not ns2 is empty iff ( AND2 q3,(NOT1 q1) is empty & AND2 q1,(XOR2 q2,q3) is empty & q2 is empty & not q1 is empty & not R is empty ) )
by A19;
then
( not ns2 is empty iff ( ( q3 is empty or not q1 is empty ) & q3 is empty & q2 is empty & not q1 is empty & not R is empty ) )
;
hence
( not ns2 is empty iff not AND2 s1,R is empty )
by A2; ( ( 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 ) )
( not ns3 is empty iff ( nq3 is empty & not XOR2 q1,q2 is empty & not R is empty & q1 is empty & not R is empty ) )
by A12, A17, A18;
then
( not ns3 is empty iff ( ( q3 is empty or NOT1 q1 is empty ) & ( q1 is empty or XOR2 q2,q3 is empty ) & not q2 is empty & q1 is empty & not R is empty ) )
by A19;
hence
( not ns3 is empty iff not AND2 s2,R is empty )
by A3; ( ( 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 ) )
( not ns4 is empty iff ( not OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3)) is empty & not R is empty & nq2 is empty & AND2 (NOT1 q1),R is empty ) )
by A13, A17, A19;
then
( not ns4 is empty iff ( not OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3)) is empty & not R is empty & XOR2 q1,q2 is empty & not q1 is empty ) )
by A18;
then
( not ns4 is empty iff ( ( ( not q3 is empty & not NOT1 q1 is empty ) or ( not q1 is empty & not XOR2 q2,q3 is empty ) ) & not R is empty & not q2 is empty & not q1 is empty ) )
;
then
( not ns4 is empty iff ( q3 is empty & not R is empty & not q2 is empty & not q1 is empty ) )
;
hence
( not ns4 is empty iff not AND2 s3,R is empty )
by A4; ( ( 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 ) )
( not ns5 is empty iff ( not nq3 is empty & ( XOR2 q1,q2 is empty or R is empty ) & q1 is empty & not R is empty ) )
by A14, A17, A18;
then
( not ns5 is empty iff ( not OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3)) is empty & q2 is empty & q1 is empty & not R is empty ) )
by A19;
then
( not ns5 is empty iff ( not q3 is empty & not NOT1 q2 is empty & not NOT1 q1 is empty & not R is empty ) )
;
hence
( not ns5 is empty iff not AND2 s4,R is empty )
by A5; ( ( 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 ) )
( not ns6 is empty iff ( not nq3 is empty & not XOR2 q1,q2 is empty & not R is empty & ( NOT1 q1 is empty or R is empty ) ) )
by A15, A17, A18;
then
( not ns6 is empty iff ( not nq3 is empty & not XOR2 q1,q2 is empty & not R is empty & not q1 is empty ) )
;
then
( not ns6 is empty iff ( ( ( not q3 is empty & not NOT1 q1 is empty ) or ( not q1 is empty & not XOR2 q2,q3 is empty ) ) & not R is empty & q2 is empty & not q1 is empty ) )
by A19;
then
( not ns6 is empty iff ( not q3 is empty & not R is empty & q2 is empty & not q1 is empty ) )
;
hence
( not ns6 is empty iff not AND2 s5,R is empty )
by A6; ( ( 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 ) )
( not ns7 is empty iff ( not nq3 is empty & not XOR2 q1,q2 is empty & q1 is empty & not R is empty ) )
by A16, A17, A18;
then
( not ns7 is empty iff ( not OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3)) is empty & not q2 is empty & q1 is empty & not R is empty ) )
by A19;
then
( not ns7 is empty iff ( not q3 is empty & not q2 is empty & not NOT1 q1 is empty & not R is empty ) )
;
hence
( not ns7 is empty iff not AND2 s6,R is empty )
by A7; ( not ns0 is empty iff not OR2 s7,(NOT1 R) is empty )
( ( ( not q1 is empty & XOR2 q1,q2 is empty & OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3)) is empty ) or R is empty ) iff not ns0 is empty )
by A9, A17, A18, A19;
then
( ( ( not q1 is empty & not q2 is empty & AND2 q3,(NOT1 q1) is empty & XOR2 q2,q3 is empty ) or R is empty ) iff not ns0 is empty )
;
then
( ( ( not q1 is empty & not q2 is empty & not q1 is empty & not q3 is empty ) or R is empty ) iff not ns0 is empty )
;
hence
( not ns0 is empty iff not OR2 s7,(NOT1 R) is empty )
by A8; verum