let c1, x1, y1, x2, y2, x3, y3, x4, y4, c4, q1, p1, sd1, q2, p2, sd2, q3, p3, sd3, q4, p4, sd4, cb1, cb2, l2, t2, l3, m3, t3, l4, m4, n4, t4, l5, m5, n5, o5, s1, s2, s3, s4 be set ; :: thesis: not ( ( not q1 is empty implies not NOR2 (x1,y1) is empty ) & ( not NOR2 (x1,y1) is empty implies not q1 is empty ) & ( not p1 is empty implies not NAND2 (x1,y1) is empty ) & ( not NAND2 (x1,y1) is empty implies not p1 is empty ) & ( not sd1 is empty implies not MODADD2 (x1,y1) is empty ) & ( not MODADD2 (x1,y1) is empty implies not sd1 is empty ) & ( not q2 is empty implies not NOR2 (x2,y2) is empty ) & ( not NOR2 (x2,y2) is empty implies not q2 is empty ) & ( not p2 is empty implies not NAND2 (x2,y2) is empty ) & ( not NAND2 (x2,y2) is empty implies not p2 is empty ) & ( not sd2 is empty implies not MODADD2 (x2,y2) is empty ) & ( not MODADD2 (x2,y2) is empty implies not sd2 is empty ) & ( not q3 is empty implies not NOR2 (x3,y3) is empty ) & ( not NOR2 (x3,y3) is empty implies not q3 is empty ) & ( not p3 is empty implies not NAND2 (x3,y3) is empty ) & ( not NAND2 (x3,y3) is empty implies not p3 is empty ) & ( not sd3 is empty implies not MODADD2 (x3,y3) is empty ) & ( not MODADD2 (x3,y3) is empty implies not sd3 is empty ) & ( not q4 is empty implies not NOR2 (x4,y4) is empty ) & ( not NOR2 (x4,y4) is empty implies not q4 is empty ) & ( not p4 is empty implies not NAND2 (x4,y4) is empty ) & ( not NAND2 (x4,y4) is empty implies not p4 is empty ) & ( not sd4 is empty implies not MODADD2 (x4,y4) is empty ) & ( not MODADD2 (x4,y4) is empty implies not sd4 is empty ) & ( not cb1 is empty implies not NOT1 c1 is empty ) & ( not NOT1 c1 is empty implies not cb1 is empty ) & ( not cb2 is empty implies not NOT1 cb1 is empty ) & ( not NOT1 cb1 is empty implies not cb2 is empty ) & ( not s1 is empty implies not XOR2 (cb2,sd1) is empty ) & ( not XOR2 (cb2,sd1) is empty implies not s1 is empty ) & ( not l2 is empty implies not AND2 (cb1,p1) is empty ) & ( not AND2 (cb1,p1) is empty implies not l2 is empty ) & ( not t2 is empty implies not NOR2 (l2,q1) is empty ) & ( not NOR2 (l2,q1) is empty implies not t2 is empty ) & ( not s2 is empty implies not XOR2 (t2,sd2) is empty ) & ( not XOR2 (t2,sd2) is empty implies not s2 is empty ) & ( not l3 is empty implies not AND2 (q1,p2) is empty ) & ( not AND2 (q1,p2) is empty implies not l3 is empty ) & ( not m3 is empty implies not AND3 (p2,p1,cb1) is empty ) & ( not AND3 (p2,p1,cb1) is empty implies not m3 is empty ) & ( not t3 is empty implies not NOR3 (l3,m3,q2) is empty ) & ( not NOR3 (l3,m3,q2) is empty implies not t3 is empty ) & ( not s3 is empty implies not XOR2 (t3,sd3) is empty ) & ( not XOR2 (t3,sd3) is empty implies not s3 is empty ) & ( not l4 is empty implies not AND2 (q2,p3) is empty ) & ( not AND2 (q2,p3) is empty implies not l4 is empty ) & ( not m4 is empty implies not AND3 (q1,p3,p2) is empty ) & ( not AND3 (q1,p3,p2) is empty implies not m4 is empty ) & ( not n4 is empty implies not AND4 (p3,p2,p1,cb1) is empty ) & ( not AND4 (p3,p2,p1,cb1) is empty implies not n4 is empty ) & ( not t4 is empty implies not NOR4 (l4,m4,n4,q3) is empty ) & ( not NOR4 (l4,m4,n4,q3) is empty implies not t4 is empty ) & ( not s4 is empty implies not XOR2 (t4,sd4) is empty ) & ( not XOR2 (t4,sd4) is empty implies not s4 is empty ) & ( not l5 is empty implies not AND2 (q3,p4) is empty ) & ( not AND2 (q3,p4) is empty implies not l5 is empty ) & ( not m5 is empty implies not AND3 (q2,p4,p3) is empty ) & ( not AND3 (q2,p4,p3) is empty implies not m5 is empty ) & ( not n5 is empty implies not AND4 (q1,p4,p3,p2) is empty ) & ( not AND4 (q1,p4,p3,p2) is empty implies not n5 is empty ) & ( not o5 is empty implies not AND5 (p4,p3,p2,p1,cb1) is empty ) & ( not AND5 (p4,p3,p2,p1,cb1) is empty implies not o5 is empty ) & ( not c4 is empty implies not NOR5 (q4,l5,m5,n5,o5) is empty ) & ( not NOR5 (q4,l5,m5,n5,o5) is empty implies not c4 is empty ) & not ( ( not s1 is empty implies not ADD1 (x1,y1,c1) is empty ) & ( not ADD1 (x1,y1,c1) is empty implies not s1 is empty ) & ( not s2 is empty implies not ADD2 (x2,y2,x1,y1,c1) is empty ) & ( not ADD2 (x2,y2,x1,y1,c1) is empty implies not s2 is empty ) & ( not s3 is empty implies not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty implies not s3 is empty ) & ( not s4 is empty implies not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) ) )
assume that
A1: ( not q1 is empty iff not NOR2 (x1,y1) is empty ) and
A2: ( not p1 is empty iff not NAND2 (x1,y1) is empty ) and
A3: ( not sd1 is empty iff not MODADD2 (x1,y1) is empty ) and
A4: ( not q2 is empty iff not NOR2 (x2,y2) is empty ) and
A5: ( not p2 is empty iff not NAND2 (x2,y2) is empty ) and
A6: ( not sd2 is empty iff not MODADD2 (x2,y2) is empty ) and
A7: ( not q3 is empty iff not NOR2 (x3,y3) is empty ) and
A8: ( not p3 is empty iff not NAND2 (x3,y3) is empty ) and
A9: ( not sd3 is empty iff not MODADD2 (x3,y3) is empty ) and
A10: ( not q4 is empty iff not NOR2 (x4,y4) is empty ) and
A11: ( not p4 is empty iff not NAND2 (x4,y4) is empty ) and
A12: ( not sd4 is empty iff not MODADD2 (x4,y4) is empty ) and
A13: ( not cb1 is empty iff not NOT1 c1 is empty ) and
A14: ( ( not cb2 is empty implies not NOT1 cb1 is empty ) & ( not NOT1 cb1 is empty implies not cb2 is empty ) & ( not s1 is empty implies not XOR2 (cb2,sd1) is empty ) & ( not XOR2 (cb2,sd1) is empty implies not s1 is empty ) ) and
A15: ( not l2 is empty iff not AND2 (cb1,p1) is empty ) and
A16: ( ( not t2 is empty implies not NOR2 (l2,q1) is empty ) & ( not NOR2 (l2,q1) is empty implies not t2 is empty ) & ( not s2 is empty implies not XOR2 (t2,sd2) is empty ) & ( not XOR2 (t2,sd2) is empty implies not s2 is empty ) ) and
A17: ( not l3 is empty iff not AND2 (q1,p2) is empty ) and
A18: ( not m3 is empty iff not AND3 (p2,p1,cb1) is empty ) and
A19: ( ( not t3 is empty implies not NOR3 (l3,m3,q2) is empty ) & ( not NOR3 (l3,m3,q2) is empty implies not t3 is empty ) & ( not s3 is empty implies not XOR2 (t3,sd3) is empty ) & ( not XOR2 (t3,sd3) is empty implies not s3 is empty ) ) and
A20: ( not l4 is empty iff not AND2 (q2,p3) is empty ) and
A21: ( ( not m4 is empty implies not AND3 (q1,p3,p2) is empty ) & ( not AND3 (q1,p3,p2) is empty implies not m4 is empty ) & ( not n4 is empty implies not AND4 (p3,p2,p1,cb1) is empty ) & ( not AND4 (p3,p2,p1,cb1) is empty implies not n4 is empty ) & ( not t4 is empty implies not NOR4 (l4,m4,n4,q3) is empty ) & ( not NOR4 (l4,m4,n4,q3) is empty implies not t4 is empty ) & ( not s4 is empty implies not XOR2 (t4,sd4) is empty ) & ( not XOR2 (t4,sd4) is empty implies not s4 is empty ) ) and
A22: ( not l5 is empty iff not AND2 (q3,p4) is empty ) and
A23: ( ( not m5 is empty implies not AND3 (q2,p4,p3) is empty ) & ( not AND3 (q2,p4,p3) is empty implies not m5 is empty ) & ( not n5 is empty implies not AND4 (q1,p4,p3,p2) is empty ) & ( not AND4 (q1,p4,p3,p2) is empty implies not n5 is empty ) & ( not o5 is empty implies not AND5 (p4,p3,p2,p1,cb1) is empty ) & ( not AND5 (p4,p3,p2,p1,cb1) is empty implies not o5 is empty ) ) and
A24: ( not c4 is empty iff not NOR5 (q4,l5,m5,n5,o5) is empty ) ; :: thesis: ( ( not s1 is empty implies not ADD1 (x1,y1,c1) is empty ) & ( not ADD1 (x1,y1,c1) is empty implies not s1 is empty ) & ( not s2 is empty implies not ADD2 (x2,y2,x1,y1,c1) is empty ) & ( not ADD2 (x2,y2,x1,y1,c1) is empty implies not s2 is empty ) & ( not s3 is empty implies not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty implies not s3 is empty ) & ( not s4 is empty implies not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) )
A25: ( not p1 is empty & not x1 is empty iff y1 is empty ) by A2;
A26: ( not sd1 is empty iff ( ( not x1 is empty or not y1 is empty ) & ( x1 is empty or y1 is empty ) ) ) by A3, Def34;
hereby :: thesis: ( ( not ADD1 (x1,y1,c1) is empty implies not s1 is empty ) & ( not s2 is empty implies not ADD2 (x2,y2,x1,y1,c1) is empty ) & ( not ADD2 (x2,y2,x1,y1,c1) is empty implies not s2 is empty ) & ( not s3 is empty implies not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty implies not s3 is empty ) & ( not s4 is empty implies not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) )
assume A27: not s1 is empty ; :: thesis: not ADD1 (x1,y1,c1) is empty
per cases ( ( not c1 is empty & sd1 is empty ) or ( c1 is empty & not sd1 is empty ) ) by A13, A14, A27;
suppose ( not c1 is empty & sd1 is empty ) ; :: thesis: not ADD1 (x1,y1,c1) is empty
hence not ADD1 (x1,y1,c1) is empty by A26; :: thesis: verum
end;
suppose ( c1 is empty & not sd1 is empty ) ; :: thesis: not ADD1 (x1,y1,c1) is empty
hence not ADD1 (x1,y1,c1) is empty by A26; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( ( not s2 is empty implies not ADD2 (x2,y2,x1,y1,c1) is empty ) & ( not ADD2 (x2,y2,x1,y1,c1) is empty implies not s2 is empty ) & ( not s3 is empty implies not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty implies not s3 is empty ) & ( not s4 is empty implies not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) )
assume A28: not ADD1 (x1,y1,c1) is empty ; :: thesis: not s1 is empty
per cases ( ( not c1 is empty & sd1 is empty ) or ( c1 is empty & not sd1 is empty ) ) by A26, A28;
suppose ( c1 is empty & not sd1 is empty ) ; :: thesis: not s1 is empty
hence not s1 is empty by A13, A14; :: thesis: verum
end;
end;
end;
A29: ( not q1 is empty iff ( x1 is empty & y1 is empty ) ) by A1;
A30: ( not sd2 is empty iff ( ( not x2 is empty or not y2 is empty ) & ( x2 is empty or y2 is empty ) ) ) by A6, Def34;
hereby :: thesis: ( ( not ADD2 (x2,y2,x1,y1,c1) is empty implies not s2 is empty ) & ( not s3 is empty implies not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty implies not s3 is empty ) & ( not s4 is empty implies not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) )
assume A31: not s2 is empty ; :: thesis: not ADD2 (x2,y2,x1,y1,c1) is empty
per cases ( ( ( not c1 is empty or p1 is empty ) & q1 is empty & sd2 is empty ) or ( ( ( c1 is empty & not p1 is empty ) or not q1 is empty ) & not sd2 is empty ) ) by A13, A15, A16, A31;
suppose ( ( not c1 is empty or p1 is empty ) & q1 is empty & sd2 is empty ) ; :: thesis: not ADD2 (x2,y2,x1,y1,c1) is empty
hence not ADD2 (x2,y2,x1,y1,c1) is empty by A29, A25, A30; :: thesis: verum
end;
suppose ( ( ( c1 is empty & not p1 is empty ) or not q1 is empty ) & not sd2 is empty ) ; :: thesis: not ADD2 (x2,y2,x1,y1,c1) is empty
hence not ADD2 (x2,y2,x1,y1,c1) is empty by A29, A25, A30; :: thesis: verum
end;
end;
end;
A32: ( not cb1 is empty iff c1 is empty ) by A13;
hereby :: thesis: ( ( not s3 is empty implies not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty implies not s3 is empty ) & ( not s4 is empty implies not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) )
assume A33: not ADD2 (x2,y2,x1,y1,c1) is empty ; :: thesis: not s2 is empty
per cases ( ( l2 is empty & q1 is empty & sd2 is empty ) or ( ( not l2 is empty or not q1 is empty ) & not sd2 is empty ) ) by A15, A29, A25, A30, A32, A33;
suppose ( l2 is empty & q1 is empty & sd2 is empty ) ; :: thesis: not s2 is empty
hence not s2 is empty by A16; :: thesis: verum
end;
suppose ( ( not l2 is empty or not q1 is empty ) & not sd2 is empty ) ; :: thesis: not s2 is empty
hence not s2 is empty by A16; :: thesis: verum
end;
end;
end;
A34: ( not q2 is empty iff ( x2 is empty & y2 is empty ) ) by A4;
A35: ( not p2 is empty & not x2 is empty iff y2 is empty ) by A5;
A36: ( not sd3 is empty iff ( ( not x3 is empty or not y3 is empty ) & ( x3 is empty or y3 is empty ) ) ) by A9, Def34;
hereby :: thesis: ( ( not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty implies not s3 is empty ) & ( not s4 is empty implies not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) )
assume A37: not s3 is empty ; :: thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
per cases ( ( l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty ) or ( l3 is empty & m3 is empty & q2 is empty & not x3 is empty & not y3 is empty ) or ( not l3 is empty & not sd3 is empty ) or ( not m3 is empty & not sd3 is empty ) or ( not q2 is empty & not sd3 is empty ) ) by A9, A19, A37, Def13, Def34;
suppose ( l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty ) ; :: thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
hence not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A17, A18, A29, A25, A34, A35, A32; :: thesis: verum
end;
suppose ( l3 is empty & m3 is empty & q2 is empty & not x3 is empty & not y3 is empty ) ; :: thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
hence not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A17, A18, A29, A25, A34, A35, A32; :: thesis: verum
end;
suppose A38: ( not l3 is empty & not sd3 is empty ) ; :: thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
then A39: ( x2 is empty or y2 is empty ) by A5, A17;
( x1 is empty & y1 is empty ) by A1, A17, A38;
hence not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A36, A38, A39; :: thesis: verum
end;
suppose A40: ( not m3 is empty & not sd3 is empty ) ; :: thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
then c1 is empty by A13, A18;
hence not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A18, A25, A35, A36, A40; :: thesis: verum
end;
suppose ( not q2 is empty & not sd3 is empty ) ; :: thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
hence not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A34, A36; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( ( not s4 is empty implies not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) )
assume A41: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty ; :: thesis: not s3 is empty
per cases ( ( l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty ) or ( l3 is empty & m3 is empty & q2 is empty & not x3 is empty & not y3 is empty ) or ( not l3 is empty & not sd3 is empty ) or ( not m3 is empty & not sd3 is empty ) or ( not q2 is empty & not sd3 is empty ) ) by A17, A18, A29, A25, A34, A35, A36, A32, A41;
suppose ( l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty ) ; :: thesis: not s3 is empty
hence not s3 is empty by A9, A19, Def13, Def34; :: thesis: verum
end;
suppose ( l3 is empty & m3 is empty & q2 is empty & not x3 is empty & not y3 is empty ) ; :: thesis: not s3 is empty
hence not s3 is empty by A9, A19, Def13, Def34; :: thesis: verum
end;
end;
end;
A42: ( not p3 is empty & not x3 is empty iff y3 is empty ) by A8;
A43: ( not sd4 is empty iff ( ( not x4 is empty or not y4 is empty ) & ( x4 is empty or y4 is empty ) ) ) by A12, Def34;
A44: ( not q3 is empty iff ( x3 is empty & y3 is empty ) ) by A7;
hereby :: thesis: ( ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) )
assume A45: not s4 is empty ; :: thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
per cases ( ( l4 is empty & ( q1 is empty or p3 is empty or p2 is empty ) & ( p3 is empty or p2 is empty or p1 is empty or not c1 is empty ) & q3 is empty & sd4 is empty ) or ( not l4 is empty & not sd4 is empty ) or ( not q1 is empty & not p3 is empty & not p2 is empty & not sd4 is empty ) or ( not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty & not sd4 is empty ) or ( not q3 is empty & not sd4 is empty ) ) by A13, A21, A45, Def14, Def17;
suppose ( l4 is empty & ( q1 is empty or p3 is empty or p2 is empty ) & ( p3 is empty or p2 is empty or p1 is empty or not c1 is empty ) & q3 is empty & sd4 is empty ) ; :: thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A20, A29, A25, A34, A35, A44, A42, A43; :: thesis: verum
end;
suppose ( not l4 is empty & not sd4 is empty ) ; :: thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A20, A34, A42, A43; :: thesis: verum
end;
suppose ( not q1 is empty & not p3 is empty & not p2 is empty & not sd4 is empty ) ; :: thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A29, A35, A42, A43; :: thesis: verum
end;
suppose ( not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty & not sd4 is empty ) ; :: thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A25, A35, A42, A43; :: thesis: verum
end;
suppose ( not q3 is empty & not sd4 is empty ) ; :: thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A44, A43; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( not c4 is empty iff not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty )
assume A46: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ; :: thesis: not s4 is empty
thus not s4 is empty :: thesis: verum
proof
assume A47: s4 is empty ; :: thesis: contradiction
per cases ( ( l4 is empty & ( q1 is empty or p3 is empty or p2 is empty ) & ( p3 is empty or p2 is empty or p1 is empty or not c1 is empty ) & q3 is empty & not sd4 is empty ) or ( not l4 is empty & sd4 is empty ) or ( not q1 is empty & not p3 is empty & not p2 is empty & sd4 is empty ) or ( not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty & sd4 is empty ) or ( not q3 is empty & sd4 is empty ) ) by A13, A21, A47, Def14, Def17;
suppose ( l4 is empty & ( q1 is empty or p3 is empty or p2 is empty ) & ( p3 is empty or p2 is empty or p1 is empty or not c1 is empty ) & q3 is empty & not sd4 is empty ) ; :: thesis: contradiction
hence contradiction by A20, A29, A25, A34, A35, A44, A42, A43, A46; :: thesis: verum
end;
suppose ( not q1 is empty & not p3 is empty & not p2 is empty & sd4 is empty ) ; :: thesis: contradiction
hence contradiction by A29, A35, A42, A43, A46; :: thesis: verum
end;
suppose ( not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty & sd4 is empty ) ; :: thesis: contradiction
hence contradiction by A25, A35, A42, A43, A46; :: thesis: verum
end;
end;
end;
end;
A48: ( not p4 is empty & not x4 is empty iff y4 is empty ) by A11;
A49: ( not q4 is empty iff ( x4 is empty & y4 is empty ) ) by A10;
now
assume that
A50: q4 is empty and
A51: l5 is empty and
A52: ( m5 is empty & n5 is empty & o5 is empty ) ; :: thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
per cases ( p4 is empty or p3 is empty or ( p2 is empty & q2 is empty ) or ( p1 is empty & q2 is empty ) or ( not c1 is empty & q1 is empty & q2 is empty ) ) by A13, A23, A52, Def14, Def18;
suppose p4 is empty ; :: thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A48; :: thesis: verum
end;
suppose p3 is empty ; :: thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A42, A49, A50; :: thesis: verum
end;
suppose ( p2 is empty & q2 is empty ) ; :: thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A22, A35, A44, A49, A48, A50, A51; :: thesis: verum
end;
suppose ( p1 is empty & q2 is empty ) ; :: thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A22, A25, A34, A44, A49, A48, A50, A51; :: thesis: verum
end;
suppose ( not c1 is empty & q1 is empty & q2 is empty ) ; :: thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A22, A29, A34, A44, A49, A48, A50, A51; :: thesis: verum
end;
end;
end;
hence ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) by A24, Def21; :: thesis: ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty )
assume A53: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ; :: thesis: not c4 is empty
assume A54: c4 is empty ; :: thesis: contradiction
per cases ( not q4 is empty or ( not q3 is empty & not p4 is empty ) or ( not q2 is empty & not p4 is empty & not p3 is empty ) or ( not q1 is empty & not p4 is empty & not p3 is empty & not p2 is empty ) or ( not p4 is empty & not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty ) ) by A13, A22, A23, A24, A54, Def14, Def18, Def21;
suppose not q4 is empty ; :: thesis: contradiction
hence contradiction by A49, A53; :: thesis: verum
end;
suppose ( not q3 is empty & not p4 is empty ) ; :: thesis: contradiction
hence contradiction by A44, A48, A53; :: thesis: verum
end;
suppose ( not q2 is empty & not p4 is empty & not p3 is empty ) ; :: thesis: contradiction
hence contradiction by A34, A42, A48, A53; :: thesis: verum
end;
suppose ( not q1 is empty & not p4 is empty & not p3 is empty & not p2 is empty ) ; :: thesis: contradiction
hence contradiction by A29, A35, A42, A48, A53; :: thesis: verum
end;
suppose ( not p4 is empty & not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty ) ; :: thesis: contradiction
hence contradiction by A25, A35, A42, A48, A53; :: thesis: verum
end;
end;