gate_2.miz



    begin

    reserve a,b,c,d for set;

    theorem :: GATE_2:1

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

      thus (s0 is non empty iff not ( AND3 (( NOT1 q3),( NOT1 q2),( NOT1 q1))) is empty) & (s1 is non empty iff not ( AND3 (( NOT1 q3),( NOT1 q2),q1)) is empty) & (s2 is non empty iff not ( AND3 (( NOT1 q3),q2,( NOT1 q1))) is empty) & (s3 is non empty iff not ( AND3 (( NOT1 q3),q2,q1)) is empty) & (s4 is non empty iff not ( AND3 (q3,( NOT1 q2),( NOT1 q1))) is empty) & (s5 is non empty iff not ( AND3 (q3,( NOT1 q2),q1)) is empty) & (s6 is non empty iff not ( AND3 (q3,q2,( NOT1 q1))) is empty) & (s7 is non empty iff not ( AND3 (q3,q2,q1)) is empty) & (ns0 is non empty iff not ( AND3 (( NOT1 nq3),( NOT1 nq2),( NOT1 nq1))) is empty) & (ns1 is non empty iff not ( AND3 (( NOT1 nq3),( NOT1 nq2),nq1)) is empty) & (ns2 is non empty iff not ( AND3 (( NOT1 nq3),nq2,( NOT1 nq1))) is empty) & (ns3 is non empty iff not ( AND3 (( NOT1 nq3),nq2,nq1)) is empty) & (ns4 is non empty iff not ( AND3 (nq3,( NOT1 nq2),( NOT1 nq1))) is empty) & (ns5 is non empty iff not ( AND3 (nq3,( NOT1 nq2),nq1)) is empty) & (ns6 is non empty iff not ( AND3 (nq3,nq2,( NOT1 nq1))) is empty) & (ns7 is non empty iff not ( AND3 (nq3,nq2,nq1)) is empty) & (nq1 is non empty iff not ( NOT1 q1) is empty) & (nq2 is non empty iff not ( XOR2 (q1,q2)) is empty) & (nq3 is non empty iff not ( OR2 (( AND2 (q3,( NOT1 q1))),( AND2 (q1,( XOR2 (q2,q3)))))) is empty) implies (ns1 is non empty iff s0 is non empty) & (ns2 is non empty iff s1 is non empty) & (ns3 is non empty iff s2 is non empty) & (ns4 is non empty iff s3 is non empty) & (ns5 is non empty iff s4 is non empty) & (ns6 is non empty iff s5 is non empty) & (ns7 is non empty iff s6 is non empty) & (ns0 is non empty iff s7 is non empty)

      proof

        assume that

         A1: s0 is non empty iff not ( AND3 (( NOT1 q3),( NOT1 q2),( NOT1 q1))) is empty and

         A2: s1 is non empty iff not ( AND3 (( NOT1 q3),( NOT1 q2),q1)) is empty and

         A3: s2 is non empty iff not ( AND3 (( NOT1 q3),q2,( NOT1 q1))) is empty and

         A4: s3 is non empty iff not ( AND3 (( NOT1 q3),q2,q1)) is empty and

         A5: s4 is non empty iff not ( AND3 (q3,( NOT1 q2),( NOT1 q1))) is empty and

         A6: s5 is non empty iff not ( AND3 (q3,( NOT1 q2),q1)) is empty and

         A7: s6 is non empty iff not ( AND3 (q3,q2,( NOT1 q1))) is empty and

         A8: s7 is non empty iff not ( AND3 (q3,q2,q1)) is empty and

         A9: ns0 is non empty iff not ( AND3 (( NOT1 nq3),( NOT1 nq2),( NOT1 nq1))) is empty and

         A10: ns1 is non empty iff not ( AND3 (( NOT1 nq3),( NOT1 nq2),nq1)) is empty and

         A11: ns2 is non empty iff not ( AND3 (( NOT1 nq3),nq2,( NOT1 nq1))) is empty and

         A12: ns3 is non empty iff not ( AND3 (( NOT1 nq3),nq2,nq1)) is empty and

         A13: ns4 is non empty iff not ( AND3 (nq3,( NOT1 nq2),( NOT1 nq1))) is empty and

         A14: ns5 is non empty iff not ( AND3 (nq3,( NOT1 nq2),nq1)) is empty and

         A15: ns6 is non empty iff not ( AND3 (nq3,nq2,( NOT1 nq1))) is empty and

         A16: ns7 is non empty iff not ( AND3 (nq3,nq2,nq1)) is empty and

         A17: (nq1 is non empty iff not ( NOT1 q1) is empty) & (nq2 is non empty iff not ( XOR2 (q1,q2)) is empty) and

         A18: nq3 is non empty iff not ( OR2 (( AND2 (q3,( NOT1 q1))),( AND2 (q1,( XOR2 (q2,q3)))))) is empty;

        ns1 is non empty iff ( NOT1 nq3) is non empty & not not ( XOR2 (q1,q2)) is empty & not q1 is non empty by A10, A17;

        then ns1 is non empty iff ( not not q3 is empty or not not ( NOT1 q1) is empty) & ( not not q1 is empty or not not ( XOR2 (q2,q3)) is empty) & not q2 is non empty & not q1 is non empty by A18;

        hence ns1 is non empty iff s0 is non empty by A1;

        ns2 is non empty iff not ( AND2 (q3,( NOT1 q1))) is non empty & not ( AND2 (q1,( XOR2 (q2,q3)))) is non empty & not q2 is non empty & q1 is non empty by A11, A17, A18, GATE_1: 6;

        then ns2 is non empty iff ( not q3 is non empty or q1 is non empty) & not q3 is non empty & not q2 is non empty & q1 is non empty;

        hence ns2 is non empty iff s1 is non empty by A2;

        ns3 is non empty iff ( NOT1 nq3) is non empty & ( XOR2 (q1,q2)) is non empty & not q1 is non empty by A12, A17;

        then ns3 is non empty iff ( not q3 is non empty or not ( NOT1 q1) is non empty) & ( not q1 is non empty or not ( XOR2 (q2,q3)) is non empty) & q2 is non empty & not q1 is non empty by A18;

        hence ns3 is non empty iff s2 is non empty by A3;

        ns4 is non empty iff (( AND2 (q3,( NOT1 q1))) is non empty or ( AND2 (q1,( XOR2 (q2,q3)))) is non empty) & q2 is non empty & q1 is non empty by A13, A17, A18, GATE_1: 6;

        then ns4 is non empty iff not q3 is non empty & q2 is non empty & q1 is non empty;

        hence ns4 is non empty iff s3 is non empty by A4;

        ns5 is non empty iff nq3 is non empty & not ( XOR2 (q1,q2)) is non empty & not q1 is non empty by A14, A17;

        then ns5 is non empty iff (( AND2 (q3,( NOT1 q1))) is non empty or ( AND2 (q1,( XOR2 (q2,q3)))) is non empty) & not q2 is non empty & not q1 is non empty by A18;

        then ns5 is non empty iff q3 is non empty & ( NOT1 q2) is non empty & ( NOT1 q1) is non empty;

        hence ns5 is non empty iff s4 is non empty by A5;

        ns6 is non empty iff (( AND2 (q3,( NOT1 q1))) is non empty or ( AND2 (q1,( XOR2 (q2,q3)))) is non empty) & not q2 is non empty & q1 is non empty by A15, A17, A18, GATE_1: 6;

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

        hence ns6 is non empty iff s5 is non empty by A6;

        ns7 is non empty iff nq3 is non empty & ( XOR2 (q1,q2)) is non empty & not q1 is non empty by A16, A17;

        then ns7 is non empty iff (( AND2 (q3,( NOT1 q1))) is non empty or ( AND2 (q1,( XOR2 (q2,q3)))) is non empty) & q2 is non empty & not q1 is non empty by A18;

        then ns7 is non empty iff q3 is non empty & q2 is non empty & ( NOT1 q1) is non empty;

        hence ns7 is non empty iff s6 is non empty by A7;

        ns0 is non empty iff not ( AND2 (q3,( NOT1 q1))) is non empty & not ( AND2 (q1,( XOR2 (q2,q3)))) is non empty & q2 is non empty & q1 is non empty by A9, A17, A18, GATE_1: 6;

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

        hence thesis by A8;

      end;

    end;

    theorem :: GATE_2:2

    ( AND3 (( AND2 (a,d)),( AND2 (b,d)),( AND2 (c,d)))) is non empty iff ( AND2 (( AND3 (a,b,c)),d)) is non empty

    proof

      a is non empty & b is non empty & c is non empty & d is non empty iff ( AND3 (a,b,c)) is non empty & d is non empty;

      hence thesis;

    end;

    theorem :: GATE_2:3

    ( not ( AND2 (a,b)) is non empty iff ( OR2 (( NOT1 a),( NOT1 b))) is non empty) & (( OR2 (a,b)) is non empty & ( OR2 (c,b)) is non empty iff ( OR2 (( AND2 (a,c)),b)) is non empty) & (( OR2 (a,b)) is non empty & ( OR2 (c,b)) is non empty & ( OR2 (d,b)) is non empty iff ( OR2 (( AND3 (a,c,d)),b)) is non empty) & (( OR2 (a,b)) is non empty & (a is non empty iff c is non empty) implies ( OR2 (c,b)) is non empty)

    proof

      

       A1: ( OR2 (a,b)) is non empty & ( OR2 (c,b)) is non empty iff (a is non empty or b is non empty) & (c is non empty or b is non empty);

      

       A2: ( OR2 (a,b)) is non empty & ( OR2 (c,b)) is non empty & ( OR2 (d,b)) is non empty iff (a is non empty or b is non empty) & (c is non empty or b is non empty) & (d is non empty or b is non empty);

       not ( AND2 (a,b)) is non empty iff not (a is non empty & b is non empty);

      hence thesis by A1, A2;

    end;

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

      thus (s0 is non empty iff ( AND3 (( NOT1 q3),( NOT1 q2),( NOT1 q1))) is non empty) & (s1 is non empty iff ( AND3 (( NOT1 q3),( NOT1 q2),q1)) is non empty) & (s2 is non empty iff ( AND3 (( NOT1 q3),q2,( NOT1 q1))) is non empty) & (s3 is non empty iff ( AND3 (( NOT1 q3),q2,q1)) is non empty) & (s4 is non empty iff ( AND3 (q3,( NOT1 q2),( NOT1 q1))) is non empty) & (s5 is non empty iff ( AND3 (q3,( NOT1 q2),q1)) is non empty) & (s6 is non empty iff ( AND3 (q3,q2,( NOT1 q1))) is non empty) & (s7 is non empty iff ( AND3 (q3,q2,q1)) is non empty) & (ns0 is non empty iff ( AND3 (( NOT1 nq3),( NOT1 nq2),( NOT1 nq1))) is non empty) & (ns1 is non empty iff ( AND3 (( NOT1 nq3),( NOT1 nq2),nq1)) is non empty) & (ns2 is non empty iff ( AND3 (( NOT1 nq3),nq2,( NOT1 nq1))) is non empty) & (ns3 is non empty iff ( AND3 (( NOT1 nq3),nq2,nq1)) is non empty) & (ns4 is non empty iff ( AND3 (nq3,( NOT1 nq2),( NOT1 nq1))) is non empty) & (ns5 is non empty iff ( AND3 (nq3,( NOT1 nq2),nq1)) is non empty) & (ns6 is non empty iff ( AND3 (nq3,nq2,( NOT1 nq1))) is non empty) & (ns7 is non empty iff ( AND3 (nq3,nq2,nq1)) is non empty) & (nq1 is non empty iff ( AND2 (( NOT1 q1),R)) is non empty) & (nq2 is non empty iff ( AND2 (( XOR2 (q1,q2)),R)) is non empty) & (nq3 is non empty iff ( AND2 (( OR2 (( AND2 (q3,( NOT1 q1))),( AND2 (q1,( XOR2 (q2,q3)))))),R)) is non empty) implies (ns1 is non empty iff ( AND2 (s0,R)) is non empty) & (ns2 is non empty iff ( AND2 (s1,R)) is non empty) & (ns3 is non empty iff ( AND2 (s2,R)) is non empty) & (ns4 is non empty iff ( AND2 (s3,R)) is non empty) & (ns5 is non empty iff ( AND2 (s4,R)) is non empty) & (ns6 is non empty iff ( AND2 (s5,R)) is non empty) & (ns7 is non empty iff ( AND2 (s6,R)) is non empty) & (ns0 is non empty iff ( OR2 (s7,( NOT1 R))) is non empty)

      proof

        assume that

         A1: s0 is non empty iff ( AND3 (( NOT1 q3),( NOT1 q2),( NOT1 q1))) is non empty and

         A2: s1 is non empty iff ( AND3 (( NOT1 q3),( NOT1 q2),q1)) is non empty and

         A3: s2 is non empty iff ( AND3 (( NOT1 q3),q2,( NOT1 q1))) is non empty and

         A4: s3 is non empty iff ( AND3 (( NOT1 q3),q2,q1)) is non empty and

         A5: s4 is non empty iff ( AND3 (q3,( NOT1 q2),( NOT1 q1))) is non empty and

         A6: s5 is non empty iff ( AND3 (q3,( NOT1 q2),q1)) is non empty and

         A7: s6 is non empty iff ( AND3 (q3,q2,( NOT1 q1))) is non empty and

         A8: s7 is non empty iff ( AND3 (q3,q2,q1)) is non empty and

         A9: ns0 is non empty iff ( AND3 (( NOT1 nq3),( NOT1 nq2),( NOT1 nq1))) is non empty and

         A10: ns1 is non empty iff ( AND3 (( NOT1 nq3),( NOT1 nq2),nq1)) is non empty and

         A11: ns2 is non empty iff ( AND3 (( NOT1 nq3),nq2,( NOT1 nq1))) is non empty and

         A12: ns3 is non empty iff ( AND3 (( NOT1 nq3),nq2,nq1)) is non empty and

         A13: ns4 is non empty iff ( AND3 (nq3,( NOT1 nq2),( NOT1 nq1))) is non empty and

         A14: ns5 is non empty iff ( AND3 (nq3,( NOT1 nq2),nq1)) is non empty and

         A15: ns6 is non empty iff ( AND3 (nq3,nq2,( NOT1 nq1))) is non empty and

         A16: ns7 is non empty iff ( AND3 (nq3,nq2,nq1)) is non empty and

         A17: nq1 is non empty iff ( AND2 (( NOT1 q1),R)) is non empty and

         A18: nq2 is non empty iff ( AND2 (( XOR2 (q1,q2)),R)) is non empty and

         A19: nq3 is non empty iff ( AND2 (( OR2 (( AND2 (q3,( NOT1 q1))),( AND2 (q1,( XOR2 (q2,q3)))))),R)) is non empty;

        ns1 is non empty iff not nq3 is non empty & ( not ( XOR2 (q1,q2)) is non empty or not R is non empty) & not q1 is non empty & R is non empty by A10, A17, A18;

        then ns1 is non empty iff ( not q3 is non empty or not ( NOT1 q1) is non empty) & ( not q1 is non empty or not ( XOR2 (q2,q3)) is non empty) & not q2 is non empty & not q1 is non empty & R is non empty by A19;

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

        ns2 is non empty iff not nq3 is non empty & ( XOR2 (q1,q2)) is non empty & R is non empty & ( not ( NOT1 q1) is non empty or not R is non empty) by A11, A17, A18;

        then ns2 is non empty iff not nq3 is non empty & ( XOR2 (q1,q2)) is non empty & R is non empty & q1 is non empty;

        then ns2 is non empty iff not ( AND2 (q3,( NOT1 q1))) is non empty & not ( AND2 (q1,( XOR2 (q2,q3)))) is non empty & not q2 is non empty & q1 is non empty & R is non empty by A19;

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

        hence ns2 is non empty iff ( AND2 (s1,R)) is non empty by A2;

        ns3 is non empty iff not nq3 is non empty & ( XOR2 (q1,q2)) is non empty & R is non empty & not q1 is non empty & R is non empty by A12, A17, A18;

        then ns3 is non empty iff ( not q3 is non empty or not ( NOT1 q1) is non empty) & ( not q1 is non empty or not ( XOR2 (q2,q3)) is non empty) & q2 is non empty & not q1 is non empty & R is non empty by A19;

        hence ns3 is non empty iff ( AND2 (s2,R)) is non empty by A3;

        ns4 is non empty iff ( OR2 (( AND2 (q3,( NOT1 q1))),( AND2 (q1,( XOR2 (q2,q3)))))) is non empty & R is non empty & not nq2 is non empty & not ( AND2 (( NOT1 q1),R)) is non empty by A13, A17, A19;

        then ns4 is non empty iff ( OR2 (( AND2 (q3,( NOT1 q1))),( AND2 (q1,( XOR2 (q2,q3)))))) is non empty & R is non empty & not ( XOR2 (q1,q2)) is non empty & q1 is non empty by A18;

        then ns4 is non empty iff (q3 is non empty & ( NOT1 q1) is non empty or q1 is non empty & ( XOR2 (q2,q3)) is non empty) & R is non empty & q2 is non empty & q1 is non empty;

        then ns4 is non empty iff not q3 is non empty & R is non empty & q2 is non empty & q1 is non empty;

        hence ns4 is non empty iff ( AND2 (s3,R)) is non empty by A4;

        ns5 is non empty iff nq3 is non empty & ( not ( XOR2 (q1,q2)) is non empty or not R is non empty) & not q1 is non empty & R is non empty by A14, A17, A18;

        then ns5 is non empty iff ( OR2 (( AND2 (q3,( NOT1 q1))),( AND2 (q1,( XOR2 (q2,q3)))))) is non empty & not q2 is non empty & not q1 is non empty & R is non empty by A19;

        then ns5 is non empty iff q3 is non empty & ( NOT1 q2) is non empty & ( NOT1 q1) is non empty & R is non empty;

        hence ns5 is non empty iff ( AND2 (s4,R)) is non empty by A5;

        ns6 is non empty iff nq3 is non empty & ( XOR2 (q1,q2)) is non empty & R is non empty & ( not ( NOT1 q1) is non empty or not R is non empty) by A15, A17, A18;

        then ns6 is non empty iff nq3 is non empty & ( XOR2 (q1,q2)) is non empty & R is non empty & q1 is non empty;

        then ns6 is non empty iff (q3 is non empty & ( NOT1 q1) is non empty or q1 is non empty & ( XOR2 (q2,q3)) is non empty) & R is non empty & not q2 is non empty & q1 is non empty by A19;

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

        hence ns6 is non empty iff ( AND2 (s5,R)) is non empty by A6;

        ns7 is non empty iff nq3 is non empty & ( XOR2 (q1,q2)) is non empty & not q1 is non empty & R is non empty by A16, A17, A18;

        then ns7 is non empty iff ( OR2 (( AND2 (q3,( NOT1 q1))),( AND2 (q1,( XOR2 (q2,q3)))))) is non empty & q2 is non empty & not q1 is non empty & R is non empty by A19;

        then ns7 is non empty iff q3 is non empty & q2 is non empty & ( NOT1 q1) is non empty & R is non empty;

        hence ns7 is non empty iff ( AND2 (s6,R)) is non empty by A7;

        ns0 is non empty iff q1 is non empty & not ( XOR2 (q1,q2)) is non empty & not ( OR2 (( AND2 (q3,( NOT1 q1))),( AND2 (q1,( XOR2 (q2,q3)))))) is non empty or not R is non empty by A9, A17, A18, A19;

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

        then ns0 is non empty iff q1 is non empty & q2 is non empty & q1 is non empty & q3 is non empty or not R is non empty;

        hence thesis by A8;

      end;

    end;