gate_3.miz



    begin

    theorem :: GATE_3:1

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

    proof

      let s0,s1,s2,s3,ns0,ns1,ns2,ns3,q1,q2,nq1,nq2 be set;

      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 iff not ( NOT1 q2) is empty) & ( not nq2 is empty iff not q1 is empty);

      thus not ns1 is empty iff not s0 is empty by A1, A6, A9;

      thus not ns3 is empty iff not s1 is empty by A2, A8, A9;

       not ns2 is empty iff not q2 is empty & not q1 is empty by A7, A9;

      hence not ns2 is empty iff not s3 is empty by A4;

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

      hence thesis by A3;

    end;

    theorem :: GATE_3:2

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

    proof

      let s0,s1,s2,s3,ns0,ns1,ns2,ns3,q1,q2,nq1,nq2,R be set;

      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 iff not ( AND2 (( NOT1 q2),R)) is empty) & ( not nq2 is empty iff not ( AND2 (q1,R)) is empty);

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

      hence not ns1 is empty iff not ( AND2 (s0,R)) is empty by A1;

       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;

       not ns2 is empty iff not ( not ( NOT1 q2) is empty & not 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;

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

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

      hence thesis by A3;

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

    proof

      let s0,s1,s2,s3,s4,s5,s6,s7,ns0,ns1,ns2,ns3,ns4,ns5,ns6,ns7,q1,q2,q3,nq1,nq2,nq3 be set;

      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 ( NOT1 q3) is empty) & ( not nq2 is empty iff not q1 is empty) & ( not nq3 is empty iff not q2 is empty);

      thus not ns1 is empty iff not s0 is empty by A1, A10, A17;

      thus not ns3 is empty iff not s1 is empty by A2, A12, A17;

      thus not ns7 is empty iff not s3 is empty by A4, A16, A17;

       not ns6 is empty iff not q3 is empty & not q2 is empty & not q1 is empty by A15, A17;

      hence not ns6 is empty iff not s7 is empty by A8;

       not ns4 is empty iff not q3 is empty & not q2 is empty & not ( NOT1 q1) is empty by A13, A17;

      hence not ns4 is empty iff not s6 is empty by A7;

       not ns0 is empty iff not q3 is empty & not ( NOT1 q2) is empty & not ( NOT1 q1) is empty by A9, A17;

      hence not ns0 is empty iff not s4 is empty by A5;

       not ns2 is empty iff not q3 is empty & not ( NOT1 q2) is empty & not q1 is empty by A11, A17;

      hence not ns2 is empty iff not s5 is empty by A6;

      thus thesis by A3, A14, A17;

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

    proof

      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;

      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 q3),R)) is empty) & ( not nq2 is empty iff not ( AND2 (q1,R)) is empty) & ( not nq3 is empty iff not ( AND2 (q2,R)) is empty);

       not ns1 is empty iff not ( NOT1 q3) is empty & not R is empty & not ( not q2 is empty & not R is empty) & not ( not q1 is empty & not R is empty) by A10, A17;

      hence not ns1 is empty iff not ( AND2 (s0,R)) is empty by A1;

       not ns3 is empty iff not ( NOT1 q3) is empty & not R is empty & not ( not q2 is empty & not R is empty) & not q1 is empty & not R is empty by A12, A17;

      hence not ns3 is empty iff not ( AND2 (s1,R)) is empty by A2;

       not ns7 is empty iff not ( NOT1 q3) is empty & not R is empty & not q2 is empty & not R is empty & not q1 is empty & not R is empty by A16, A17;

      hence not ns7 is empty iff not ( AND2 (s3,R)) is empty by A4;

       not ns6 is empty iff not ( not ( NOT1 q3) is empty & not R is empty) & not q2 is empty & not R is empty & not q1 is empty & not R is empty by A15, A17;

      then not ns6 is empty iff not q3 is empty & not q2 is empty & not q1 is empty & not R is empty;

      hence not ns6 is empty iff not ( AND2 (s7,R)) is empty by A8;

       not ns4 is empty iff not ( not ( NOT1 q3) is empty & not R is empty) & not q2 is empty & not R is empty & not ( not q1 is empty & not R is empty) by A13, A17;

      then not ns4 is empty iff not q3 is empty & not q2 is empty & not ( NOT1 q1) is empty & not R is empty;

      hence not ns4 is empty iff not ( AND2 (s6,R)) is empty by A7;

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

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

      hence not ns0 is empty iff not ( OR2 (( AND2 (s4,R)),( NOT1 R))) is empty by A5;

       not ns2 is empty iff not ( not ( NOT1 q3) is empty & not R is empty) & not ( not q2 is empty & not R is empty) & not q1 is empty & not R is empty by A11, A17;

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

      hence not ns2 is empty iff not ( AND2 (s5,R)) is empty by A6;

       not ns5 is empty iff not ( NOT1 q3) is empty & not R is empty & not q2 is empty & not R is empty & not ( not q1 is empty & not R is empty) by A14, A17;

      hence thesis by A3;

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

    proof

      let 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 be set;

      assume that

       A1: not s0 is empty iff not ( AND4 (( NOT1 q4),( NOT1 q3),( NOT1 q2),( NOT1 q1))) is empty and

       A2: not s1 is empty iff not ( AND4 (( NOT1 q4),( NOT1 q3),( NOT1 q2),q1)) is empty and

       A3: not s2 is empty iff not ( AND4 (( NOT1 q4),( NOT1 q3),q2,( NOT1 q1))) is empty and

       A4: not s3 is empty iff not ( AND4 (( NOT1 q4),( NOT1 q3),q2,q1)) is empty and

       A5: not s4 is empty iff not ( AND4 (( NOT1 q4),q3,( NOT1 q2),( NOT1 q1))) is empty and

       A6: not s5 is empty iff not ( AND4 (( NOT1 q4),q3,( NOT1 q2),q1)) is empty and

       A7: not s6 is empty iff not ( AND4 (( NOT1 q4),q3,q2,( NOT1 q1))) is empty and

       A8: not s7 is empty iff not ( AND4 (( NOT1 q4),q3,q2,q1)) is empty and

       A9: not s8 is empty iff not ( AND4 (q4,( NOT1 q3),( NOT1 q2),( NOT1 q1))) is empty and

       A10: not s9 is empty iff not ( AND4 (q4,( NOT1 q3),( NOT1 q2),q1)) is empty and

       A11: not s10 is empty iff not ( AND4 (q4,( NOT1 q3),q2,( NOT1 q1))) is empty and

       A12: not s11 is empty iff not ( AND4 (q4,( NOT1 q3),q2,q1)) is empty and

       A13: not s12 is empty iff not ( AND4 (q4,q3,( NOT1 q2),( NOT1 q1))) is empty and

       A14: not s13 is empty iff not ( AND4 (q4,q3,( NOT1 q2),q1)) is empty and

       A15: not s14 is empty iff not ( AND4 (q4,q3,q2,( NOT1 q1))) is empty and

       A16: not s15 is empty iff not ( AND4 (q4,q3,q2,q1)) is empty and

       A17: not ns0 is empty iff not ( AND4 (( NOT1 nq4),( NOT1 nq3),( NOT1 nq2),( NOT1 nq1))) is empty and

       A18: not ns1 is empty iff not ( AND4 (( NOT1 nq4),( NOT1 nq3),( NOT1 nq2),nq1)) is empty and

       A19: not ns2 is empty iff not ( AND4 (( NOT1 nq4),( NOT1 nq3),nq2,( NOT1 nq1))) is empty and

       A20: not ns3 is empty iff not ( AND4 (( NOT1 nq4),( NOT1 nq3),nq2,nq1)) is empty and

       A21: not ns4 is empty iff not ( AND4 (( NOT1 nq4),nq3,( NOT1 nq2),( NOT1 nq1))) is empty and

       A22: not ns5 is empty iff not ( AND4 (( NOT1 nq4),nq3,( NOT1 nq2),nq1)) is empty and

       A23: not ns6 is empty iff not ( AND4 (( NOT1 nq4),nq3,nq2,( NOT1 nq1))) is empty and

       A24: not ns7 is empty iff not ( AND4 (( NOT1 nq4),nq3,nq2,nq1)) is empty and

       A25: not ns8 is empty iff not ( AND4 (nq4,( NOT1 nq3),( NOT1 nq2),( NOT1 nq1))) is empty and

       A26: not ns9 is empty iff not ( AND4 (nq4,( NOT1 nq3),( NOT1 nq2),nq1)) is empty and

       A27: not ns10 is empty iff not ( AND4 (nq4,( NOT1 nq3),nq2,( NOT1 nq1))) is empty and

       A28: not ns11 is empty iff not ( AND4 (nq4,( NOT1 nq3),nq2,nq1)) is empty and

       A29: not ns12 is empty iff not ( AND4 (nq4,nq3,( NOT1 nq2),( NOT1 nq1))) is empty and

       A30: not ns13 is empty iff not ( AND4 (nq4,nq3,( NOT1 nq2),nq1)) is empty and

       A31: not ns14 is empty iff not ( AND4 (nq4,nq3,nq2,( NOT1 nq1))) is empty and

       A32: not ns15 is empty iff not ( AND4 (nq4,nq3,nq2,nq1)) is empty and

       A33: ( not nq1 is empty iff not ( NOT1 q4) is empty) & ( not nq2 is empty iff not q1 is empty) & ( not nq3 is empty iff not q2 is empty) & ( not nq4 is empty iff not q3 is empty);

      thus not ns1 is empty iff not s0 is empty by A1, A18, A33, GATE_1: 20;

      thus not ns3 is empty iff not s1 is empty by A2, A20, A33, GATE_1: 20;

      thus not ns7 is empty iff not s3 is empty by A4, A24, A33, GATE_1: 20;

      thus not ns15 is empty iff not s7 is empty by A8, A32, A33, GATE_1: 20;

       not ns14 is empty iff not q4 is empty & not q3 is empty & not q2 is empty & not q1 is empty by A31, A33, GATE_1: 20;

      hence not ns14 is empty iff not s15 is empty by A16, GATE_1: 20;

       not ns12 is empty iff not q4 is empty & not q3 is empty & not q2 is empty & not ( NOT1 q1) is empty by A29, A33, GATE_1: 20;

      hence not ns12 is empty iff not s14 is empty by A15, GATE_1: 20;

       not ns8 is empty iff not q4 is empty & not q3 is empty & not ( NOT1 q2) is empty & not ( NOT1 q1) is empty by A25, A33, GATE_1: 20;

      hence not ns8 is empty iff not s12 is empty by A13, GATE_1: 20;

       not ns0 is empty iff not q4 is empty & not ( NOT1 q3) is empty & not ( NOT1 q2) is empty & not ( NOT1 q1) is empty by A17, A33, GATE_1: 20;

      hence not ns0 is empty iff not s8 is empty by A9, GATE_1: 20;

      thus not ns5 is empty iff not s2 is empty by A3, A22, A33, GATE_1: 20;

      thus not ns11 is empty iff not s5 is empty by A6, A28, A33, GATE_1: 20;

       not ns6 is empty iff not q4 is empty & not ( NOT1 q3) is empty & not q2 is empty & not q1 is empty by A23, A33, GATE_1: 20;

      hence not ns6 is empty iff not s11 is empty by A12, GATE_1: 20;

      thus not ns13 is empty iff not s6 is empty by A7, A30, A33, GATE_1: 20;

       not ns10 is empty iff not q4 is empty & not q3 is empty & not ( NOT1 q2) is empty & not q1 is empty by A27, A33, GATE_1: 20;

      hence not ns10 is empty iff not s13 is empty by A14, GATE_1: 20;

       not ns4 is empty iff not q4 is empty & not ( NOT1 q3) is empty & not q2 is empty & not ( NOT1 q1) is empty by A21, A33, GATE_1: 20;

      hence not ns4 is empty iff not s10 is empty by A11, GATE_1: 20;

      thus not ns9 is empty iff not s4 is empty by A5, A26, A33, GATE_1: 20;

       not ns2 is empty iff not q4 is empty & not ( NOT1 q3) is empty & not ( NOT1 q2) is empty & not q1 is empty by A19, A33, GATE_1: 20;

      hence thesis by A10, GATE_1: 20;

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

    proof

      let 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 be set;

      assume that

       A1: not s0 is empty iff not ( AND4 (( NOT1 q4),( NOT1 q3),( NOT1 q2),( NOT1 q1))) is empty and

       A2: not s1 is empty iff not ( AND4 (( NOT1 q4),( NOT1 q3),( NOT1 q2),q1)) is empty and

       A3: not s2 is empty iff not ( AND4 (( NOT1 q4),( NOT1 q3),q2,( NOT1 q1))) is empty and

       A4: not s3 is empty iff not ( AND4 (( NOT1 q4),( NOT1 q3),q2,q1)) is empty and

       A5: not s4 is empty iff not ( AND4 (( NOT1 q4),q3,( NOT1 q2),( NOT1 q1))) is empty and

       A6: not s5 is empty iff not ( AND4 (( NOT1 q4),q3,( NOT1 q2),q1)) is empty and

       A7: not s6 is empty iff not ( AND4 (( NOT1 q4),q3,q2,( NOT1 q1))) is empty and

       A8: not s7 is empty iff not ( AND4 (( NOT1 q4),q3,q2,q1)) is empty and

       A9: not s8 is empty iff not ( AND4 (q4,( NOT1 q3),( NOT1 q2),( NOT1 q1))) is empty and

       A10: not s9 is empty iff not ( AND4 (q4,( NOT1 q3),( NOT1 q2),q1)) is empty and

       A11: not s10 is empty iff not ( AND4 (q4,( NOT1 q3),q2,( NOT1 q1))) is empty and

       A12: not s11 is empty iff not ( AND4 (q4,( NOT1 q3),q2,q1)) is empty and

       A13: not s12 is empty iff not ( AND4 (q4,q3,( NOT1 q2),( NOT1 q1))) is empty and

       A14: not s13 is empty iff not ( AND4 (q4,q3,( NOT1 q2),q1)) is empty and

       A15: not s14 is empty iff not ( AND4 (q4,q3,q2,( NOT1 q1))) is empty and

       A16: not s15 is empty iff not ( AND4 (q4,q3,q2,q1)) is empty and

       A17: not ns0 is empty iff not ( AND4 (( NOT1 nq4),( NOT1 nq3),( NOT1 nq2),( NOT1 nq1))) is empty and

       A18: not ns1 is empty iff not ( AND4 (( NOT1 nq4),( NOT1 nq3),( NOT1 nq2),nq1)) is empty and

       A19: not ns2 is empty iff not ( AND4 (( NOT1 nq4),( NOT1 nq3),nq2,( NOT1 nq1))) is empty and

       A20: not ns3 is empty iff not ( AND4 (( NOT1 nq4),( NOT1 nq3),nq2,nq1)) is empty and

       A21: not ns4 is empty iff not ( AND4 (( NOT1 nq4),nq3,( NOT1 nq2),( NOT1 nq1))) is empty and

       A22: not ns5 is empty iff not ( AND4 (( NOT1 nq4),nq3,( NOT1 nq2),nq1)) is empty and

       A23: not ns6 is empty iff not ( AND4 (( NOT1 nq4),nq3,nq2,( NOT1 nq1))) is empty and

       A24: not ns7 is empty iff not ( AND4 (( NOT1 nq4),nq3,nq2,nq1)) is empty and

       A25: not ns8 is empty iff not ( AND4 (nq4,( NOT1 nq3),( NOT1 nq2),( NOT1 nq1))) is empty and

       A26: not ns9 is empty iff not ( AND4 (nq4,( NOT1 nq3),( NOT1 nq2),nq1)) is empty and

       A27: not ns10 is empty iff not ( AND4 (nq4,( NOT1 nq3),nq2,( NOT1 nq1))) is empty and

       A28: not ns11 is empty iff not ( AND4 (nq4,( NOT1 nq3),nq2,nq1)) is empty and

       A29: not ns12 is empty iff not ( AND4 (nq4,nq3,( NOT1 nq2),( NOT1 nq1))) is empty and

       A30: not ns13 is empty iff not ( AND4 (nq4,nq3,( NOT1 nq2),nq1)) is empty and

       A31: not ns14 is empty iff not ( AND4 (nq4,nq3,nq2,( NOT1 nq1))) is empty and

       A32: not ns15 is empty iff not ( AND4 (nq4,nq3,nq2,nq1)) is empty and

       A33: ( not nq1 is empty iff not ( AND2 (( NOT1 q4),R)) is empty) & ( not nq2 is empty iff not ( AND2 (q1,R)) is empty) & ( not nq3 is empty iff not ( AND2 (q2,R)) is empty) & ( not nq4 is empty iff not ( AND2 (q3,R)) is empty);

       not ns1 is empty iff not ( NOT1 q4) is empty & not R is empty & not ( not q3 is empty & not R is empty) & not ( not q2 is empty & not R is empty) & not ( not q1 is empty & not R is empty) by A18, A33, GATE_1: 20;

      hence not ns1 is empty iff not ( AND2 (s0,R)) is empty by A1, GATE_1: 20;

       not ns3 is empty iff not ( NOT1 q4) is empty & not R is empty & not ( not q3 is empty & not R is empty) & not ( not q2 is empty & not R is empty) & not q1 is empty & not R is empty by A20, A33, GATE_1: 20;

      hence not ns3 is empty iff not ( AND2 (s1,R)) is empty by A2, GATE_1: 20;

       not ns7 is empty iff not ( NOT1 q4) is empty & not R is empty & not ( not q3 is empty & not R is empty) & not q2 is empty & not R is empty & not q1 is empty & not R is empty by A24, A33, GATE_1: 20;

      hence not ns7 is empty iff not ( AND2 (s3,R)) is empty by A4, GATE_1: 20;

       not ns15 is empty iff not ( NOT1 q4) is empty & not R is empty & not q3 is empty & not R is empty & not q2 is empty & not R is empty & not q1 is empty & not R is empty by A32, A33, GATE_1: 20;

      hence not ns15 is empty iff not ( AND2 (s7,R)) is empty by A8, GATE_1: 20;

       not ns14 is empty iff not ( not ( NOT1 q4) is empty & not R is empty) & not q3 is empty & not R is empty & not q2 is empty & not R is empty & not q1 is empty & not R is empty by A31, A33, GATE_1: 20;

      then not ns14 is empty iff not q4 is empty & not q3 is empty & not q2 is empty & not q1 is empty & not R is empty;

      hence not ns14 is empty iff not ( AND2 (s15,R)) is empty by A16, GATE_1: 20;

       not ns12 is empty iff not ( not ( NOT1 q4) is empty & not R is empty) & not q3 is empty & not R is empty & not q2 is empty & not R is empty & not ( not q1 is empty & not R is empty) by A29, A33, GATE_1: 20;

      then not ns12 is empty iff not q4 is empty & not q3 is empty & not q2 is empty & not ( NOT1 q1) is empty & not R is empty;

      hence not ns12 is empty iff not ( AND2 (s14,R)) is empty by A15, GATE_1: 20;

       not ns8 is empty iff not ( not ( NOT1 q4) is empty & not R is empty) & not q3 is empty & not R is empty & not ( not q2 is empty & not R is empty) & not ( not q1 is empty & not R is empty) by A25, A33, GATE_1: 20;

      then not ns8 is empty iff not q4 is empty & not q3 is empty & not ( NOT1 q2) is empty & not ( NOT1 q1) is empty & not R is empty;

      hence not ns8 is empty iff not ( AND2 (s12,R)) is empty by A13, GATE_1: 20;

       not ns0 is empty iff not ( not ( NOT1 q4) is empty & not R is empty) & not ( not q3 is empty & not R is empty) & not ( not q2 is empty & not R is empty) & not ( not q1 is empty & not R is empty) by A17, A33, GATE_1: 20;

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

      hence not ns0 is empty iff not ( OR2 (( AND2 (s8,R)),( NOT1 R))) is empty by A9, GATE_1: 20;

       not ns5 is empty iff not ( NOT1 q4) is empty & not R is empty & not ( not q3 is empty & not R is empty) & not q2 is empty & not R is empty & not ( not q1 is empty & not R is empty) by A22, A33, GATE_1: 20;

      hence not ns5 is empty iff not ( AND2 (s2,R)) is empty by A3, GATE_1: 20;

       not ns11 is empty iff not ( NOT1 q4) is empty & not R is empty & not q3 is empty & not R is empty & not ( not q2 is empty & not R is empty) & not q1 is empty & not R is empty by A28, A33, GATE_1: 20;

      hence not ns11 is empty iff not ( AND2 (s5,R)) is empty by A6, GATE_1: 20;

       not ns6 is empty iff not ( not ( NOT1 q4) is empty & not R is empty) & not ( not q3 is empty & not R is empty) & not q2 is empty & not R is empty & not q1 is empty & not R is empty by A23, A33, GATE_1: 20;

      then not ns6 is empty iff not q4 is empty & not ( NOT1 q3) is empty & not q2 is empty & not q1 is empty & not R is empty;

      hence not ns6 is empty iff not ( AND2 (s11,R)) is empty by A12, GATE_1: 20;

       not ns13 is empty iff not ( NOT1 q4) is empty & not R is empty & not q3 is empty & not R is empty & not q2 is empty & not R is empty & not ( not q1 is empty & not R is empty) by A30, A33, GATE_1: 20;

      hence not ns13 is empty iff not ( AND2 (s6,R)) is empty by A7, GATE_1: 20;

       not ns10 is empty iff not ( not ( NOT1 q4) is empty & not R is empty) & not q3 is empty & not R is empty & not ( not q2 is empty & not R is empty) & not q1 is empty & not R is empty by A27, A33, GATE_1: 20;

      then not ns10 is empty iff not q4 is empty & not q3 is empty & not ( NOT1 q2) is empty & not q1 is empty & not R is empty;

      hence not ns10 is empty iff not ( AND2 (s13,R)) is empty by A14, GATE_1: 20;

       not ns4 is empty iff not ( not ( NOT1 q4) is empty & not R is empty) & not ( not q3 is empty & not R is empty) & not q2 is empty & not R is empty & not ( not q1 is empty & not R is empty) by A21, A33, GATE_1: 20;

      then not ns4 is empty iff not q4 is empty & not ( NOT1 q3) is empty & not q2 is empty & not ( NOT1 q1) is empty & not R is empty;

      hence not ns4 is empty iff not ( AND2 (s10,R)) is empty by A11, GATE_1: 20;

       not ns9 is empty iff not ( NOT1 q4) is empty & not R is empty & not q3 is empty & not R is empty & not ( not q2 is empty & not R is empty) & not ( not q1 is empty & not R is empty) by A26, A33, GATE_1: 20;

      hence not ns9 is empty iff not ( AND2 (s4,R)) is empty by A5, GATE_1: 20;

       not ns2 is empty iff not ( not ( NOT1 q4) is empty & not R is empty) & not ( not q3 is empty & not R is empty) & not ( not q2 is empty & not R is empty) & not q1 is empty & not R is empty by A19, A33, GATE_1: 20;

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

      hence thesis by A10, GATE_1: 20;

    end;