:: GATE_2 semantic presentation

begin


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

theorem :: GATE_2:2
for a, d, b, c being set holds
( not AND3 ((AND2 (a,d)),(AND2 (b,d)),(AND2 (c,d))) is empty iff not AND2 ((AND3 (a,b,c)),d) is empty )
proof
let a, d, b, c be set ; ::_thesis: ( not AND3 ((AND2 (a,d)),(AND2 (b,d)),(AND2 (c,d))) is empty iff not AND2 ((AND3 (a,b,c)),d) is empty )
 ( not a is empty & not b is empty & not c is empty & not d is empty iff ( not AND3 (a,b,c) is empty & not d is empty ) ) ;
hence  ( not AND3 ((AND2 (a,d)),(AND2 (b,d)),(AND2 (c,d))) is empty iff not AND2 ((AND3 (a,b,c)),d) is empty ) ; ::_thesis: verum
end;

theorem :: GATE_2:3
for a, b, c, d being set holds
( ( AND2 (a,b) is empty implies not OR2 ((NOT1 a),(NOT1 b)) is empty ) & ( not OR2 ((NOT1 a),(NOT1 b)) is empty implies AND2 (a,b) is empty ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty implies not OR2 ((AND2 (a,c)),b) is empty ) & ( not OR2 ((AND2 (a,c)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty ) ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty implies not OR2 ((AND3 (a,c,d)),b) is empty ) & ( not OR2 ((AND3 (a,c,d)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty ) ) & not ( not OR2 (a,b) is empty & ( not a is empty implies not c is empty ) & ( not c is empty implies not a is empty ) & OR2 (c,b) is empty ) )
proof
let a, b, c, d be set ; ::_thesis: ( ( AND2 (a,b) is empty implies not OR2 ((NOT1 a),(NOT1 b)) is empty ) & ( not OR2 ((NOT1 a),(NOT1 b)) is empty implies AND2 (a,b) is empty ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty implies not OR2 ((AND2 (a,c)),b) is empty ) & ( not OR2 ((AND2 (a,c)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty ) ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty implies not OR2 ((AND3 (a,c,d)),b) is empty ) & ( not OR2 ((AND3 (a,c,d)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty ) ) & not ( not OR2 (a,b) is empty & ( not a is empty implies not c is empty ) & ( not c is empty implies not a is empty ) & OR2 (c,b) is empty ) )
A1: ( not OR2 (a,b) is empty & not OR2 (c,b) is empty iff ( ( not a is empty or not b is empty ) & ( not c is empty or not b is empty ) ) ) ;
A2: ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty iff ( ( not a is empty or not b is empty ) & ( not c is empty or not b is empty ) & ( not d is empty or not b is empty ) ) ) ;
 ( AND2 (a,b) is empty iff ( a is empty or b is empty ) ) ;
hence  ( ( AND2 (a,b) is empty implies not OR2 ((NOT1 a),(NOT1 b)) is empty ) & ( not OR2 ((NOT1 a),(NOT1 b)) is empty implies AND2 (a,b) is empty ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty implies not OR2 ((AND2 (a,c)),b) is empty ) & ( not OR2 ((AND2 (a,c)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty ) ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty implies not OR2 ((AND3 (a,c,d)),b) is empty ) & ( not OR2 ((AND3 (a,c,d)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty ) ) & not ( not OR2 (a,b) is empty & ( not a is empty implies not c is empty ) & ( not c is empty implies not a is empty ) & OR2 (c,b) is empty ) ) by A1, A2; ::_thesis: verum
end;

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