:: GATE_3 semantic presentation
begin
theorem :: GATE_3:1
for s0, s1, s2, s3, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2 being set holds
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 NOT1 q2 is empty ) & ( not NOT1 q2 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & not ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns0 is empty ) ) )
proof
let s0, s1, s2, s3, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2 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 NOT1 q2 is empty ) & ( not NOT1 q2 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & not ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 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 NOT1 q2 is empty ) & ( not NOT1 q2 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) ) ; ::_thesis: ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns0 is empty ) )
thus ( not ns1 is empty iff not s0 is empty ) by A1, A6, A9; ::_thesis: ( ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns0 is empty ) )
thus ( not ns3 is empty iff not s1 is empty ) by A2, A8, A9; ::_thesis: ( ( not ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns0 is empty ) )
( 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; ::_thesis: ( not ns0 is empty iff not s2 is empty )
( not ns0 is empty iff ( not q2 is empty & not NOT1 q1 is empty ) ) by A5, A9;
hence ( not ns0 is empty iff not s2 is empty ) by A3; ::_thesis: verum
end;
theorem :: GATE_3:2
for s0, s1, s2, s3, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2, R being set holds
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 ) ) )
proof
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
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 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 q3 is empty ) & ( not NOT1 q3 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 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 ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 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 ; ::_thesis: 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 q3 is empty ) & ( not NOT1 q3 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 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 ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 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 implies not NOT1 q3 is empty ) & ( not NOT1 q3 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 is empty implies not nq3 is empty ) ) ; ::_thesis: ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )
thus ( not ns1 is empty iff not s0 is empty ) by A1, A10, A17; ::_thesis: ( ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )
thus ( not ns3 is empty iff not s1 is empty ) by A2, A12, A17; ::_thesis: ( ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )
thus ( not ns7 is empty iff not s3 is empty ) by A4, A16, A17; ::_thesis: ( ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )
( 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; ::_thesis: ( ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )
( 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; ::_thesis: ( ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )
( 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; ::_thesis: ( ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )
( 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; ::_thesis: ( not ns5 is empty iff not s2 is empty )
thus ( not ns5 is empty iff not s2 is empty ) by A3, A14, A17; ::_thesis: verum
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 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 q3),R) is empty ) & ( not AND2 ((NOT1 q3),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 nq3 is empty implies not AND2 (q2,R) is empty ) & ( not AND2 (q2,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 ns3 is empty implies not AND2 (s1,R) is empty ) & ( not AND2 (s1,R) is empty implies not ns3 is empty ) & ( not ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns6 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns6 is empty ) & ( not ns4 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns4 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns2 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 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 ; ::_thesis: 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 q3),R) is empty ) & ( not AND2 ((NOT1 q3),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 nq3 is empty implies not AND2 (q2,R) is empty ) & ( not AND2 (q2,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 ns3 is empty implies not AND2 (s1,R) is empty ) & ( not AND2 (s1,R) is empty implies not ns3 is empty ) & ( not ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns6 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns6 is empty ) & ( not ns4 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns4 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns2 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 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 implies not AND2 ((NOT1 q3),R) is empty ) & ( not AND2 ((NOT1 q3),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 nq3 is empty implies not AND2 (q2,R) is empty ) & ( not AND2 (q2,R) is empty implies not nq3 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 ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns6 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns6 is empty ) & ( not ns4 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns4 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns2 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) )
( not ns1 is empty iff ( not NOT1 q3 is empty & not R is empty & ( q2 is empty or R is empty ) & ( q1 is empty or R is empty ) ) ) by A10, A17;
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 ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns6 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns6 is empty ) & ( not ns4 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns4 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns2 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) )
( not ns3 is empty iff ( not NOT1 q3 is empty & not R is empty & ( q2 is empty or 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; ::_thesis: ( ( not ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns6 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns6 is empty ) & ( not ns4 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns4 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns2 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) )
( 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; ::_thesis: ( ( not ns6 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns6 is empty ) & ( not ns4 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns4 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns2 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) )
( not ns6 is empty iff ( ( NOT1 q3 is empty or 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; ::_thesis: ( ( not ns4 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns4 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns2 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) )
( not ns4 is empty iff ( ( NOT1 q3 is empty or R is empty ) & not q2 is empty & not R is empty & ( q1 is empty or 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; ::_thesis: ( ( not ns0 is empty implies not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s4,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns2 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) )
( not ns0 is empty iff ( ( NOT1 q3 is empty or R is empty ) & ( q2 is empty or R is empty ) & ( q1 is empty or R is empty ) ) ) by A9, A17;
then ( ( ( not q3 is empty & not NOT1 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 (s4,R)),(NOT1 R)) is empty ) by A5; ::_thesis: ( ( not ns2 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns2 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) )
( not ns2 is empty iff ( ( NOT1 q3 is empty or R is empty ) & ( q2 is empty or 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; ::_thesis: ( not ns5 is empty iff not AND2 (s2,R) is empty )
( not ns5 is empty iff ( not NOT1 q3 is empty & not R is empty & not q2 is empty & not R is empty & ( q1 is empty or R is empty ) ) ) by A14, A17;
hence ( not ns5 is empty iff not AND2 (s2,R) is empty ) by A3; ::_thesis: verum
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 being set holds
not ( ( not s0 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),q1) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),q1) is empty implies not s1 is empty ) & ( not s2 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),q2,(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),q2,(NOT1 q1)) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),q2,q1) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),q2,q1) is empty implies not s3 is empty ) & ( not s4 is empty implies not AND4 ((NOT1 q4),q3,(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),q3,(NOT1 q2),(NOT1 q1)) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND4 ((NOT1 q4),q3,(NOT1 q2),q1) is empty ) & ( not AND4 ((NOT1 q4),q3,(NOT1 q2),q1) is empty implies not s5 is empty ) & ( not s6 is empty implies not AND4 ((NOT1 q4),q3,q2,(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),q3,q2,(NOT1 q1)) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND4 ((NOT1 q4),q3,q2,q1) is empty ) & ( not AND4 ((NOT1 q4),q3,q2,q1) is empty implies not s7 is empty ) & ( not s8 is empty implies not AND4 (q4,(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 (q4,(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty implies not s8 is empty ) & ( not s9 is empty implies not AND4 (q4,(NOT1 q3),(NOT1 q2),q1) is empty ) & ( not AND4 (q4,(NOT1 q3),(NOT1 q2),q1) is empty implies not s9 is empty ) & ( not s10 is empty implies not AND4 (q4,(NOT1 q3),q2,(NOT1 q1)) is empty ) & ( not AND4 (q4,(NOT1 q3),q2,(NOT1 q1)) is empty implies not s10 is empty ) & ( not s11 is empty implies not AND4 (q4,(NOT1 q3),q2,q1) is empty ) & ( not AND4 (q4,(NOT1 q3),q2,q1) is empty implies not s11 is empty ) & ( not s12 is empty implies not AND4 (q4,q3,(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 (q4,q3,(NOT1 q2),(NOT1 q1)) is empty implies not s12 is empty ) & ( not s13 is empty implies not AND4 (q4,q3,(NOT1 q2),q1) is empty ) & ( not AND4 (q4,q3,(NOT1 q2),q1) is empty implies not s13 is empty ) & ( not s14 is empty implies not AND4 (q4,q3,q2,(NOT1 q1)) is empty ) & ( not AND4 (q4,q3,q2,(NOT1 q1)) is empty implies not s14 is empty ) & ( not s15 is empty implies not AND4 (q4,q3,q2,q1) is empty ) & ( not AND4 (q4,q3,q2,q1) is empty implies not s15 is empty ) & ( not ns0 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1) is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1)) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,nq1) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,nq1) is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1)) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),nq1) is empty ) & ( not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),nq1) is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND4 ((NOT1 nq4),nq3,nq2,(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),nq3,nq2,(NOT1 nq1)) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND4 ((NOT1 nq4),nq3,nq2,nq1) is empty ) & ( not AND4 ((NOT1 nq4),nq3,nq2,nq1) is empty implies not ns7 is empty ) & ( not ns8 is empty implies not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty implies not ns8 is empty ) & ( not ns9 is empty implies not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),nq1) is empty ) & ( not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),nq1) is empty implies not ns9 is empty ) & ( not ns10 is empty implies not AND4 (nq4,(NOT1 nq3),nq2,(NOT1 nq1)) is empty ) & ( not AND4 (nq4,(NOT1 nq3),nq2,(NOT1 nq1)) is empty implies not ns10 is empty ) & ( not ns11 is empty implies not AND4 (nq4,(NOT1 nq3),nq2,nq1) is empty ) & ( not AND4 (nq4,(NOT1 nq3),nq2,nq1) is empty implies not ns11 is empty ) & ( not ns12 is empty implies not AND4 (nq4,nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 (nq4,nq3,(NOT1 nq2),(NOT1 nq1)) is empty implies not ns12 is empty ) & ( not ns13 is empty implies not AND4 (nq4,nq3,(NOT1 nq2),nq1) is empty ) & ( not AND4 (nq4,nq3,(NOT1 nq2),nq1) is empty implies not ns13 is empty ) & ( not ns14 is empty implies not AND4 (nq4,nq3,nq2,(NOT1 nq1)) is empty ) & ( not AND4 (nq4,nq3,nq2,(NOT1 nq1)) is empty implies not ns14 is empty ) & ( not ns15 is empty implies not AND4 (nq4,nq3,nq2,nq1) is empty ) & ( not AND4 (nq4,nq3,nq2,nq1) is empty implies not ns15 is empty ) & ( not nq1 is empty implies not NOT1 q4 is empty ) & ( not NOT1 q4 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 is empty implies not nq3 is empty ) & ( not nq4 is empty implies not q3 is empty ) & ( not q3 is empty implies not nq4 is empty ) & not ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns15 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns15 is empty ) & ( not ns14 is empty implies not s15 is empty ) & ( not s15 is empty implies not ns14 is empty ) & ( not ns12 is empty implies not s14 is empty ) & ( not s14 is empty implies not ns12 is empty ) & ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 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 ; ::_thesis: not ( ( not s0 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),q1) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),q1) is empty implies not s1 is empty ) & ( not s2 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),q2,(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),q2,(NOT1 q1)) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),q2,q1) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),q2,q1) is empty implies not s3 is empty ) & ( not s4 is empty implies not AND4 ((NOT1 q4),q3,(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),q3,(NOT1 q2),(NOT1 q1)) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND4 ((NOT1 q4),q3,(NOT1 q2),q1) is empty ) & ( not AND4 ((NOT1 q4),q3,(NOT1 q2),q1) is empty implies not s5 is empty ) & ( not s6 is empty implies not AND4 ((NOT1 q4),q3,q2,(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),q3,q2,(NOT1 q1)) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND4 ((NOT1 q4),q3,q2,q1) is empty ) & ( not AND4 ((NOT1 q4),q3,q2,q1) is empty implies not s7 is empty ) & ( not s8 is empty implies not AND4 (q4,(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 (q4,(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty implies not s8 is empty ) & ( not s9 is empty implies not AND4 (q4,(NOT1 q3),(NOT1 q2),q1) is empty ) & ( not AND4 (q4,(NOT1 q3),(NOT1 q2),q1) is empty implies not s9 is empty ) & ( not s10 is empty implies not AND4 (q4,(NOT1 q3),q2,(NOT1 q1)) is empty ) & ( not AND4 (q4,(NOT1 q3),q2,(NOT1 q1)) is empty implies not s10 is empty ) & ( not s11 is empty implies not AND4 (q4,(NOT1 q3),q2,q1) is empty ) & ( not AND4 (q4,(NOT1 q3),q2,q1) is empty implies not s11 is empty ) & ( not s12 is empty implies not AND4 (q4,q3,(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 (q4,q3,(NOT1 q2),(NOT1 q1)) is empty implies not s12 is empty ) & ( not s13 is empty implies not AND4 (q4,q3,(NOT1 q2),q1) is empty ) & ( not AND4 (q4,q3,(NOT1 q2),q1) is empty implies not s13 is empty ) & ( not s14 is empty implies not AND4 (q4,q3,q2,(NOT1 q1)) is empty ) & ( not AND4 (q4,q3,q2,(NOT1 q1)) is empty implies not s14 is empty ) & ( not s15 is empty implies not AND4 (q4,q3,q2,q1) is empty ) & ( not AND4 (q4,q3,q2,q1) is empty implies not s15 is empty ) & ( not ns0 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1) is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1)) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,nq1) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,nq1) is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1)) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),nq1) is empty ) & ( not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),nq1) is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND4 ((NOT1 nq4),nq3,nq2,(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),nq3,nq2,(NOT1 nq1)) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND4 ((NOT1 nq4),nq3,nq2,nq1) is empty ) & ( not AND4 ((NOT1 nq4),nq3,nq2,nq1) is empty implies not ns7 is empty ) & ( not ns8 is empty implies not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty implies not ns8 is empty ) & ( not ns9 is empty implies not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),nq1) is empty ) & ( not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),nq1) is empty implies not ns9 is empty ) & ( not ns10 is empty implies not AND4 (nq4,(NOT1 nq3),nq2,(NOT1 nq1)) is empty ) & ( not AND4 (nq4,(NOT1 nq3),nq2,(NOT1 nq1)) is empty implies not ns10 is empty ) & ( not ns11 is empty implies not AND4 (nq4,(NOT1 nq3),nq2,nq1) is empty ) & ( not AND4 (nq4,(NOT1 nq3),nq2,nq1) is empty implies not ns11 is empty ) & ( not ns12 is empty implies not AND4 (nq4,nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 (nq4,nq3,(NOT1 nq2),(NOT1 nq1)) is empty implies not ns12 is empty ) & ( not ns13 is empty implies not AND4 (nq4,nq3,(NOT1 nq2),nq1) is empty ) & ( not AND4 (nq4,nq3,(NOT1 nq2),nq1) is empty implies not ns13 is empty ) & ( not ns14 is empty implies not AND4 (nq4,nq3,nq2,(NOT1 nq1)) is empty ) & ( not AND4 (nq4,nq3,nq2,(NOT1 nq1)) is empty implies not ns14 is empty ) & ( not ns15 is empty implies not AND4 (nq4,nq3,nq2,nq1) is empty ) & ( not AND4 (nq4,nq3,nq2,nq1) is empty implies not ns15 is empty ) & ( not nq1 is empty implies not NOT1 q4 is empty ) & ( not NOT1 q4 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 is empty implies not nq3 is empty ) & ( not nq4 is empty implies not q3 is empty ) & ( not q3 is empty implies not nq4 is empty ) & not ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns15 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns15 is empty ) & ( not ns14 is empty implies not s15 is empty ) & ( not s15 is empty implies not ns14 is empty ) & ( not ns12 is empty implies not s14 is empty ) & ( not s14 is empty implies not ns12 is empty ) & ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) ) )
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 implies not NOT1 q4 is empty ) & ( not NOT1 q4 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 is empty implies not nq3 is empty ) & ( not nq4 is empty implies not q3 is empty ) & ( not q3 is empty implies not nq4 is empty ) ) ; ::_thesis: ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns15 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns15 is empty ) & ( not ns14 is empty implies not s15 is empty ) & ( not s15 is empty implies not ns14 is empty ) & ( not ns12 is empty implies not s14 is empty ) & ( not s14 is empty implies not ns12 is empty ) & ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
thus ( not ns1 is empty iff not s0 is empty ) by A1, A18, A33, GATE_1:20; ::_thesis: ( ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns15 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns15 is empty ) & ( not ns14 is empty implies not s15 is empty ) & ( not s15 is empty implies not ns14 is empty ) & ( not ns12 is empty implies not s14 is empty ) & ( not s14 is empty implies not ns12 is empty ) & ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
thus ( not ns3 is empty iff not s1 is empty ) by A2, A20, A33, GATE_1:20; ::_thesis: ( ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns15 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns15 is empty ) & ( not ns14 is empty implies not s15 is empty ) & ( not s15 is empty implies not ns14 is empty ) & ( not ns12 is empty implies not s14 is empty ) & ( not s14 is empty implies not ns12 is empty ) & ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
thus ( not ns7 is empty iff not s3 is empty ) by A4, A24, A33, GATE_1:20; ::_thesis: ( ( not ns15 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns15 is empty ) & ( not ns14 is empty implies not s15 is empty ) & ( not s15 is empty implies not ns14 is empty ) & ( not ns12 is empty implies not s14 is empty ) & ( not s14 is empty implies not ns12 is empty ) & ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
thus ( not ns15 is empty iff not s7 is empty ) by A8, A32, A33, GATE_1:20; ::_thesis: ( ( not ns14 is empty implies not s15 is empty ) & ( not s15 is empty implies not ns14 is empty ) & ( not ns12 is empty implies not s14 is empty ) & ( not s14 is empty implies not ns12 is empty ) & ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
( 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; ::_thesis: ( ( not ns12 is empty implies not s14 is empty ) & ( not s14 is empty implies not ns12 is empty ) & ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
( 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; ::_thesis: ( ( not ns8 is empty implies not s12 is empty ) & ( not s12 is empty implies not ns8 is empty ) & ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
( 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; ::_thesis: ( ( not ns0 is empty implies not s8 is empty ) & ( not s8 is empty implies not ns0 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
( 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; ::_thesis: ( ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) & ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
thus ( not ns5 is empty iff not s2 is empty ) by A3, A22, A33, GATE_1:20; ::_thesis: ( ( not ns11 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns11 is empty ) & ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
thus ( not ns11 is empty iff not s5 is empty ) by A6, A28, A33, GATE_1:20; ::_thesis: ( ( not ns6 is empty implies not s11 is empty ) & ( not s11 is empty implies not ns6 is empty ) & ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
( 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; ::_thesis: ( ( not ns13 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns13 is empty ) & ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
thus ( not ns13 is empty iff not s6 is empty ) by A7, A30, A33, GATE_1:20; ::_thesis: ( ( not ns10 is empty implies not s13 is empty ) & ( not s13 is empty implies not ns10 is empty ) & ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
( 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; ::_thesis: ( ( not ns4 is empty implies not s10 is empty ) & ( not s10 is empty implies not ns4 is empty ) & ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
( 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; ::_thesis: ( ( not ns9 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns9 is empty ) & ( not ns2 is empty implies not s9 is empty ) & ( not s9 is empty implies not ns2 is empty ) )
thus ( not ns9 is empty iff not s4 is empty ) by A5, A26, A33, GATE_1:20; ::_thesis: ( not ns2 is empty iff not s9 is empty )
( 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 ( not ns2 is empty iff not s9 is empty ) by A10, GATE_1:20; ::_thesis: verum
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 being set holds
not ( ( not s0 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),q1) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),q1) is empty implies not s1 is empty ) & ( not s2 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),q2,(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),q2,(NOT1 q1)) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),q2,q1) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),q2,q1) is empty implies not s3 is empty ) & ( not s4 is empty implies not AND4 ((NOT1 q4),q3,(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),q3,(NOT1 q2),(NOT1 q1)) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND4 ((NOT1 q4),q3,(NOT1 q2),q1) is empty ) & ( not AND4 ((NOT1 q4),q3,(NOT1 q2),q1) is empty implies not s5 is empty ) & ( not s6 is empty implies not AND4 ((NOT1 q4),q3,q2,(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),q3,q2,(NOT1 q1)) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND4 ((NOT1 q4),q3,q2,q1) is empty ) & ( not AND4 ((NOT1 q4),q3,q2,q1) is empty implies not s7 is empty ) & ( not s8 is empty implies not AND4 (q4,(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 (q4,(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty implies not s8 is empty ) & ( not s9 is empty implies not AND4 (q4,(NOT1 q3),(NOT1 q2),q1) is empty ) & ( not AND4 (q4,(NOT1 q3),(NOT1 q2),q1) is empty implies not s9 is empty ) & ( not s10 is empty implies not AND4 (q4,(NOT1 q3),q2,(NOT1 q1)) is empty ) & ( not AND4 (q4,(NOT1 q3),q2,(NOT1 q1)) is empty implies not s10 is empty ) & ( not s11 is empty implies not AND4 (q4,(NOT1 q3),q2,q1) is empty ) & ( not AND4 (q4,(NOT1 q3),q2,q1) is empty implies not s11 is empty ) & ( not s12 is empty implies not AND4 (q4,q3,(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 (q4,q3,(NOT1 q2),(NOT1 q1)) is empty implies not s12 is empty ) & ( not s13 is empty implies not AND4 (q4,q3,(NOT1 q2),q1) is empty ) & ( not AND4 (q4,q3,(NOT1 q2),q1) is empty implies not s13 is empty ) & ( not s14 is empty implies not AND4 (q4,q3,q2,(NOT1 q1)) is empty ) & ( not AND4 (q4,q3,q2,(NOT1 q1)) is empty implies not s14 is empty ) & ( not s15 is empty implies not AND4 (q4,q3,q2,q1) is empty ) & ( not AND4 (q4,q3,q2,q1) is empty implies not s15 is empty ) & ( not ns0 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1) is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1)) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,nq1) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,nq1) is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1)) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),nq1) is empty ) & ( not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),nq1) is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND4 ((NOT1 nq4),nq3,nq2,(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),nq3,nq2,(NOT1 nq1)) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND4 ((NOT1 nq4),nq3,nq2,nq1) is empty ) & ( not AND4 ((NOT1 nq4),nq3,nq2,nq1) is empty implies not ns7 is empty ) & ( not ns8 is empty implies not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty implies not ns8 is empty ) & ( not ns9 is empty implies not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),nq1) is empty ) & ( not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),nq1) is empty implies not ns9 is empty ) & ( not ns10 is empty implies not AND4 (nq4,(NOT1 nq3),nq2,(NOT1 nq1)) is empty ) & ( not AND4 (nq4,(NOT1 nq3),nq2,(NOT1 nq1)) is empty implies not ns10 is empty ) & ( not ns11 is empty implies not AND4 (nq4,(NOT1 nq3),nq2,nq1) is empty ) & ( not AND4 (nq4,(NOT1 nq3),nq2,nq1) is empty implies not ns11 is empty ) & ( not ns12 is empty implies not AND4 (nq4,nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 (nq4,nq3,(NOT1 nq2),(NOT1 nq1)) is empty implies not ns12 is empty ) & ( not ns13 is empty implies not AND4 (nq4,nq3,(NOT1 nq2),nq1) is empty ) & ( not AND4 (nq4,nq3,(NOT1 nq2),nq1) is empty implies not ns13 is empty ) & ( not ns14 is empty implies not AND4 (nq4,nq3,nq2,(NOT1 nq1)) is empty ) & ( not AND4 (nq4,nq3,nq2,(NOT1 nq1)) is empty implies not ns14 is empty ) & ( not ns15 is empty implies not AND4 (nq4,nq3,nq2,nq1) is empty ) & ( not AND4 (nq4,nq3,nq2,nq1) is empty implies not ns15 is empty ) & ( not nq1 is empty implies not AND2 ((NOT1 q4),R) is empty ) & ( not AND2 ((NOT1 q4),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 nq3 is empty implies not AND2 (q2,R) is empty ) & ( not AND2 (q2,R) is empty implies not nq3 is empty ) & ( not nq4 is empty implies not AND2 (q3,R) is empty ) & ( not AND2 (q3,R) is empty implies not nq4 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 ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns15 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns15 is empty ) & ( not ns14 is empty implies not AND2 (s15,R) is empty ) & ( not AND2 (s15,R) is empty implies not ns14 is empty ) & ( not ns12 is empty implies not AND2 (s14,R) is empty ) & ( not AND2 (s14,R) is empty implies not ns12 is empty ) & ( not ns8 is empty implies not AND2 (s12,R) is empty ) & ( not AND2 (s12,R) is empty implies not ns8 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 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 ; ::_thesis: not ( ( not s0 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),q1) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),(NOT1 q2),q1) is empty implies not s1 is empty ) & ( not s2 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),q2,(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),q2,(NOT1 q1)) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND4 ((NOT1 q4),(NOT1 q3),q2,q1) is empty ) & ( not AND4 ((NOT1 q4),(NOT1 q3),q2,q1) is empty implies not s3 is empty ) & ( not s4 is empty implies not AND4 ((NOT1 q4),q3,(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),q3,(NOT1 q2),(NOT1 q1)) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND4 ((NOT1 q4),q3,(NOT1 q2),q1) is empty ) & ( not AND4 ((NOT1 q4),q3,(NOT1 q2),q1) is empty implies not s5 is empty ) & ( not s6 is empty implies not AND4 ((NOT1 q4),q3,q2,(NOT1 q1)) is empty ) & ( not AND4 ((NOT1 q4),q3,q2,(NOT1 q1)) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND4 ((NOT1 q4),q3,q2,q1) is empty ) & ( not AND4 ((NOT1 q4),q3,q2,q1) is empty implies not s7 is empty ) & ( not s8 is empty implies not AND4 (q4,(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 (q4,(NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty implies not s8 is empty ) & ( not s9 is empty implies not AND4 (q4,(NOT1 q3),(NOT1 q2),q1) is empty ) & ( not AND4 (q4,(NOT1 q3),(NOT1 q2),q1) is empty implies not s9 is empty ) & ( not s10 is empty implies not AND4 (q4,(NOT1 q3),q2,(NOT1 q1)) is empty ) & ( not AND4 (q4,(NOT1 q3),q2,(NOT1 q1)) is empty implies not s10 is empty ) & ( not s11 is empty implies not AND4 (q4,(NOT1 q3),q2,q1) is empty ) & ( not AND4 (q4,(NOT1 q3),q2,q1) is empty implies not s11 is empty ) & ( not s12 is empty implies not AND4 (q4,q3,(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND4 (q4,q3,(NOT1 q2),(NOT1 q1)) is empty implies not s12 is empty ) & ( not s13 is empty implies not AND4 (q4,q3,(NOT1 q2),q1) is empty ) & ( not AND4 (q4,q3,(NOT1 q2),q1) is empty implies not s13 is empty ) & ( not s14 is empty implies not AND4 (q4,q3,q2,(NOT1 q1)) is empty ) & ( not AND4 (q4,q3,q2,(NOT1 q1)) is empty implies not s14 is empty ) & ( not s15 is empty implies not AND4 (q4,q3,q2,q1) is empty ) & ( not AND4 (q4,q3,q2,q1) is empty implies not s15 is empty ) & ( not ns0 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1) is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1)) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,nq1) is empty ) & ( not AND4 ((NOT1 nq4),(NOT1 nq3),nq2,nq1) is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1)) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),nq1) is empty ) & ( not AND4 ((NOT1 nq4),nq3,(NOT1 nq2),nq1) is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND4 ((NOT1 nq4),nq3,nq2,(NOT1 nq1)) is empty ) & ( not AND4 ((NOT1 nq4),nq3,nq2,(NOT1 nq1)) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND4 ((NOT1 nq4),nq3,nq2,nq1) is empty ) & ( not AND4 ((NOT1 nq4),nq3,nq2,nq1) is empty implies not ns7 is empty ) & ( not ns8 is empty implies not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty implies not ns8 is empty ) & ( not ns9 is empty implies not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),nq1) is empty ) & ( not AND4 (nq4,(NOT1 nq3),(NOT1 nq2),nq1) is empty implies not ns9 is empty ) & ( not ns10 is empty implies not AND4 (nq4,(NOT1 nq3),nq2,(NOT1 nq1)) is empty ) & ( not AND4 (nq4,(NOT1 nq3),nq2,(NOT1 nq1)) is empty implies not ns10 is empty ) & ( not ns11 is empty implies not AND4 (nq4,(NOT1 nq3),nq2,nq1) is empty ) & ( not AND4 (nq4,(NOT1 nq3),nq2,nq1) is empty implies not ns11 is empty ) & ( not ns12 is empty implies not AND4 (nq4,nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND4 (nq4,nq3,(NOT1 nq2),(NOT1 nq1)) is empty implies not ns12 is empty ) & ( not ns13 is empty implies not AND4 (nq4,nq3,(NOT1 nq2),nq1) is empty ) & ( not AND4 (nq4,nq3,(NOT1 nq2),nq1) is empty implies not ns13 is empty ) & ( not ns14 is empty implies not AND4 (nq4,nq3,nq2,(NOT1 nq1)) is empty ) & ( not AND4 (nq4,nq3,nq2,(NOT1 nq1)) is empty implies not ns14 is empty ) & ( not ns15 is empty implies not AND4 (nq4,nq3,nq2,nq1) is empty ) & ( not AND4 (nq4,nq3,nq2,nq1) is empty implies not ns15 is empty ) & ( not nq1 is empty implies not AND2 ((NOT1 q4),R) is empty ) & ( not AND2 ((NOT1 q4),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 nq3 is empty implies not AND2 (q2,R) is empty ) & ( not AND2 (q2,R) is empty implies not nq3 is empty ) & ( not nq4 is empty implies not AND2 (q3,R) is empty ) & ( not AND2 (q3,R) is empty implies not nq4 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 ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns15 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns15 is empty ) & ( not ns14 is empty implies not AND2 (s15,R) is empty ) & ( not AND2 (s15,R) is empty implies not ns14 is empty ) & ( not ns12 is empty implies not AND2 (s14,R) is empty ) & ( not AND2 (s14,R) is empty implies not ns12 is empty ) & ( not ns8 is empty implies not AND2 (s12,R) is empty ) & ( not AND2 (s12,R) is empty implies not ns8 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) ) )
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 implies not AND2 ((NOT1 q4),R) is empty ) & ( not AND2 ((NOT1 q4),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 nq3 is empty implies not AND2 (q2,R) is empty ) & ( not AND2 (q2,R) is empty implies not nq3 is empty ) & ( not nq4 is empty implies not AND2 (q3,R) is empty ) & ( not AND2 (q3,R) is empty implies not nq4 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 ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns15 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns15 is empty ) & ( not ns14 is empty implies not AND2 (s15,R) is empty ) & ( not AND2 (s15,R) is empty implies not ns14 is empty ) & ( not ns12 is empty implies not AND2 (s14,R) is empty ) & ( not AND2 (s14,R) is empty implies not ns12 is empty ) & ( not ns8 is empty implies not AND2 (s12,R) is empty ) & ( not AND2 (s12,R) is empty implies not ns8 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns1 is empty iff ( not NOT1 q4 is empty & not R is empty & ( q3 is empty or R is empty ) & ( q2 is empty or R is empty ) & ( q1 is empty or 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; ::_thesis: ( ( not ns3 is empty implies not AND2 (s1,R) is empty ) & ( not AND2 (s1,R) is empty implies not ns3 is empty ) & ( not ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns15 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns15 is empty ) & ( not ns14 is empty implies not AND2 (s15,R) is empty ) & ( not AND2 (s15,R) is empty implies not ns14 is empty ) & ( not ns12 is empty implies not AND2 (s14,R) is empty ) & ( not AND2 (s14,R) is empty implies not ns12 is empty ) & ( not ns8 is empty implies not AND2 (s12,R) is empty ) & ( not AND2 (s12,R) is empty implies not ns8 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns3 is empty iff ( not NOT1 q4 is empty & not R is empty & ( q3 is empty or R is empty ) & ( q2 is empty or 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; ::_thesis: ( ( not ns7 is empty implies not AND2 (s3,R) is empty ) & ( not AND2 (s3,R) is empty implies not ns7 is empty ) & ( not ns15 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns15 is empty ) & ( not ns14 is empty implies not AND2 (s15,R) is empty ) & ( not AND2 (s15,R) is empty implies not ns14 is empty ) & ( not ns12 is empty implies not AND2 (s14,R) is empty ) & ( not AND2 (s14,R) is empty implies not ns12 is empty ) & ( not ns8 is empty implies not AND2 (s12,R) is empty ) & ( not AND2 (s12,R) is empty implies not ns8 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns7 is empty iff ( not NOT1 q4 is empty & not R is empty & ( q3 is empty or 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; ::_thesis: ( ( not ns15 is empty implies not AND2 (s7,R) is empty ) & ( not AND2 (s7,R) is empty implies not ns15 is empty ) & ( not ns14 is empty implies not AND2 (s15,R) is empty ) & ( not AND2 (s15,R) is empty implies not ns14 is empty ) & ( not ns12 is empty implies not AND2 (s14,R) is empty ) & ( not AND2 (s14,R) is empty implies not ns12 is empty ) & ( not ns8 is empty implies not AND2 (s12,R) is empty ) & ( not AND2 (s12,R) is empty implies not ns8 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( 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; ::_thesis: ( ( not ns14 is empty implies not AND2 (s15,R) is empty ) & ( not AND2 (s15,R) is empty implies not ns14 is empty ) & ( not ns12 is empty implies not AND2 (s14,R) is empty ) & ( not AND2 (s14,R) is empty implies not ns12 is empty ) & ( not ns8 is empty implies not AND2 (s12,R) is empty ) & ( not AND2 (s12,R) is empty implies not ns8 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns14 is empty iff ( ( NOT1 q4 is empty or 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; ::_thesis: ( ( not ns12 is empty implies not AND2 (s14,R) is empty ) & ( not AND2 (s14,R) is empty implies not ns12 is empty ) & ( not ns8 is empty implies not AND2 (s12,R) is empty ) & ( not AND2 (s12,R) is empty implies not ns8 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns12 is empty iff ( ( NOT1 q4 is empty or R is empty ) & not q3 is empty & not R is empty & not q2 is empty & not R is empty & ( q1 is empty or 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; ::_thesis: ( ( not ns8 is empty implies not AND2 (s12,R) is empty ) & ( not AND2 (s12,R) is empty implies not ns8 is empty ) & ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns8 is empty iff ( ( NOT1 q4 is empty or R is empty ) & not q3 is empty & not R is empty & ( q2 is empty or R is empty ) & ( q1 is empty or 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; ::_thesis: ( ( not ns0 is empty implies not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty ) & ( not OR2 ((AND2 (s8,R)),(NOT1 R)) is empty implies not ns0 is empty ) & ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns0 is empty iff ( ( NOT1 q4 is empty or R is empty ) & ( q3 is empty or R is empty ) & ( q2 is empty or R is empty ) & ( q1 is empty or R is empty ) ) ) by A17, A33, GATE_1:20;
then ( ( ( not q4 is empty & not NOT1 q3 is empty & not NOT1 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 (s8,R)),(NOT1 R)) is empty ) by A9, GATE_1:20; ::_thesis: ( ( not ns5 is empty implies not AND2 (s2,R) is empty ) & ( not AND2 (s2,R) is empty implies not ns5 is empty ) & ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns5 is empty iff ( not NOT1 q4 is empty & not R is empty & ( q3 is empty or R is empty ) & not q2 is empty & not R is empty & ( q1 is empty or 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; ::_thesis: ( ( not ns11 is empty implies not AND2 (s5,R) is empty ) & ( not AND2 (s5,R) is empty implies not ns11 is empty ) & ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns11 is empty iff ( not NOT1 q4 is empty & not R is empty & not q3 is empty & not R is empty & ( q2 is empty or 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; ::_thesis: ( ( not ns6 is empty implies not AND2 (s11,R) is empty ) & ( not AND2 (s11,R) is empty implies not ns6 is empty ) & ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns6 is empty iff ( ( NOT1 q4 is empty or R is empty ) & ( q3 is empty or 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; ::_thesis: ( ( not ns13 is empty implies not AND2 (s6,R) is empty ) & ( not AND2 (s6,R) is empty implies not ns13 is empty ) & ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( 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 & ( q1 is empty or 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; ::_thesis: ( ( not ns10 is empty implies not AND2 (s13,R) is empty ) & ( not AND2 (s13,R) is empty implies not ns10 is empty ) & ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns10 is empty iff ( ( NOT1 q4 is empty or R is empty ) & not q3 is empty & not R is empty & ( q2 is empty or 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; ::_thesis: ( ( not ns4 is empty implies not AND2 (s10,R) is empty ) & ( not AND2 (s10,R) is empty implies not ns4 is empty ) & ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns4 is empty iff ( ( NOT1 q4 is empty or R is empty ) & ( q3 is empty or R is empty ) & not q2 is empty & not R is empty & ( q1 is empty or 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; ::_thesis: ( ( not ns9 is empty implies not AND2 (s4,R) is empty ) & ( not AND2 (s4,R) is empty implies not ns9 is empty ) & ( not ns2 is empty implies not AND2 (s9,R) is empty ) & ( not AND2 (s9,R) is empty implies not ns2 is empty ) )
( not ns9 is empty iff ( not NOT1 q4 is empty & not R is empty & not q3 is empty & not R is empty & ( q2 is empty or R is empty ) & ( q1 is empty or 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; ::_thesis: ( not ns2 is empty iff not AND2 (s9,R) is empty )
( not ns2 is empty iff ( ( NOT1 q4 is empty or R is empty ) & ( q3 is empty or R is empty ) & ( q2 is empty or 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 ( not ns2 is empty iff not AND2 (s9,R) is empty ) by A10, GATE_1:20; ::_thesis: verum
end;