let s0, s1, s2, s3, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2, R be set ; :: thesis: 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 ) ) )

assume that

A1: ( not s0 is empty iff not AND2 ((NOT1 q2),(NOT1 q1)) is empty ) and

A2: ( not s1 is empty iff not AND2 ((NOT1 q2),q1) is empty ) and

A3: ( not s2 is empty iff not AND2 (q2,(NOT1 q1)) is empty ) and

A4: ( not s3 is empty iff not AND2 (q2,q1) is empty ) and

A5: ( not ns0 is empty iff not AND2 ((NOT1 nq2),(NOT1 nq1)) is empty ) and

A6: ( not ns1 is empty iff not AND2 ((NOT1 nq2),nq1) is empty ) and

A7: ( not ns2 is empty iff not AND2 (nq2,(NOT1 nq1)) is empty ) and

A8: ( not ns3 is empty iff not AND2 (nq2,nq1) is empty ) and

A9: ( ( 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 ) ) ; :: thesis: ( ( 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 ) )

( not ns1 is empty iff ( not NOT1 q2 is empty & not R is empty & ( q1 is empty or R is empty ) ) ) by A6, A9;

hence ( not ns1 is empty iff not AND2 (s0,R) is empty ) by A1; :: thesis: ( ( 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 ) )

( not ns3 is empty iff ( not NOT1 q2 is empty & not q1 is empty & not R is empty ) ) by A8, A9;

hence ( not ns3 is empty iff not AND2 (s1,R) is empty ) by A2; :: thesis: ( ( 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 ) )

( not ns2 is empty iff ( ( NOT1 q2 is empty or R is empty ) & not q1 is empty & not R is empty ) ) by A7, A9;

then ( not ns2 is empty iff ( not q2 is empty & not q1 is empty & not R is empty ) ) ;

hence ( not ns2 is empty iff not AND2 (s3,R) is empty ) by A4; :: thesis: ( not ns0 is empty iff not OR2 ((AND2 (s2,R)),(NOT1 R)) is empty )

( not ns0 is empty iff ( ( NOT1 q2 is empty or R is empty ) & ( q1 is empty or R is empty ) ) ) by A5, A9;

then ( ( ( not q2 is empty & not NOT1 q1 is empty & not R is empty ) or R is empty ) iff not ns0 is empty ) ;

hence ( not ns0 is empty iff not OR2 ((AND2 (s2,R)),(NOT1 R)) is empty ) by A3; :: thesis: verum

assume that

A1: ( not s0 is empty iff not AND2 ((NOT1 q2),(NOT1 q1)) is empty ) and

A2: ( not s1 is empty iff not AND2 ((NOT1 q2),q1) is empty ) and

A3: ( not s2 is empty iff not AND2 (q2,(NOT1 q1)) is empty ) and

A4: ( not s3 is empty iff not AND2 (q2,q1) is empty ) and

A5: ( not ns0 is empty iff not AND2 ((NOT1 nq2),(NOT1 nq1)) is empty ) and

A6: ( not ns1 is empty iff not AND2 ((NOT1 nq2),nq1) is empty ) and

A7: ( not ns2 is empty iff not AND2 (nq2,(NOT1 nq1)) is empty ) and

A8: ( not ns3 is empty iff not AND2 (nq2,nq1) is empty ) and

A9: ( ( 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 ) ) ; :: thesis: ( ( 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 ) )

( not ns1 is empty iff ( not NOT1 q2 is empty & not R is empty & ( q1 is empty or R is empty ) ) ) by A6, A9;

hence ( not ns1 is empty iff not AND2 (s0,R) is empty ) by A1; :: thesis: ( ( 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 ) )

( not ns3 is empty iff ( not NOT1 q2 is empty & not q1 is empty & not R is empty ) ) by A8, A9;

hence ( not ns3 is empty iff not AND2 (s1,R) is empty ) by A2; :: thesis: ( ( 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 ) )

( not ns2 is empty iff ( ( NOT1 q2 is empty or R is empty ) & not q1 is empty & not R is empty ) ) by A7, A9;

then ( not ns2 is empty iff ( not q2 is empty & not q1 is empty & not R is empty ) ) ;

hence ( not ns2 is empty iff not AND2 (s3,R) is empty ) by A4; :: thesis: ( not ns0 is empty iff not OR2 ((AND2 (s2,R)),(NOT1 R)) is empty )

( not ns0 is empty iff ( ( NOT1 q2 is empty or R is empty ) & ( q1 is empty or R is empty ) ) ) by A5, A9;

then ( ( ( not q2 is empty & not NOT1 q1 is empty & not R is empty ) or R is empty ) iff not ns0 is empty ) ;

hence ( not ns0 is empty iff not OR2 ((AND2 (s2,R)),(NOT1 R)) is empty ) by A3; :: thesis: verum