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 ) ; :: thesis: ( ( not p2 is empty & NAND2 (x2,y2) is empty ) or ( not NAND2 (x2,y2) is empty & p2 is empty ) or ( not sd2 is empty & MODADD2 (x2,y2) is empty ) or ( not MODADD2 (x2,y2) is empty & sd2 is empty ) or ( not q3 is empty & NOR2 (x3,y3) is empty ) or ( not NOR2 (x3,y3) is empty & q3 is empty ) or ( not p3 is empty & NAND2 (x3,y3) is empty ) or ( not NAND2 (x3,y3) is empty & p3 is empty ) or ( not sd3 is empty & MODADD2 (x3,y3) is empty ) or ( not MODADD2 (x3,y3) is empty & sd3 is empty ) or ( not q4 is empty & NOR2 (x4,y4) is empty ) or ( not NOR2 (x4,y4) is empty & q4 is empty ) or ( not p4 is empty & NAND2 (x4,y4) is empty ) or ( not NAND2 (x4,y4) is empty & p4 is empty ) or ( not sd4 is empty & MODADD2 (x4,y4) is empty ) or ( not MODADD2 (x4,y4) is empty & sd4 is empty ) or ( not cb1 is empty & NOT1 c1 is empty ) or ( not NOT1 c1 is empty & cb1 is empty ) or ( not cb2 is empty & NOT1 cb1 is empty ) or ( not NOT1 cb1 is empty & cb2 is empty ) or ( not s1 is empty & XOR2 (cb2,sd1) is empty ) or ( not XOR2 (cb2,sd1) is empty & s1 is empty ) or ( not l2 is empty & AND2 (cb1,p1) is empty ) or ( not AND2 (cb1,p1) is empty & l2 is empty ) or ( not t2 is empty & NOR2 (l2,q1) is empty ) or ( not NOR2 (l2,q1) is empty & t2 is empty ) or ( not s2 is empty & XOR2 (t2,sd2) is empty ) or ( not XOR2 (t2,sd2) is empty & s2 is empty ) or ( not l3 is empty & AND2 (q1,p2) is empty ) or ( not AND2 (q1,p2) is empty & l3 is empty ) or ( not m3 is empty & AND3 (p2,p1,cb1) is empty ) or ( not AND3 (p2,p1,cb1) is empty & m3 is empty ) or ( not t3 is empty & NOR3 (l3,m3,q2) is empty ) or ( not NOR3 (l3,m3,q2) is empty & t3 is empty ) or ( not s3 is empty & XOR2 (t3,sd3) is empty ) or ( not XOR2 (t3,sd3) is empty & s3 is empty ) or ( not l4 is empty & AND2 (q2,p3) is empty ) or ( not AND2 (q2,p3) is empty & l4 is empty ) or ( not m4 is empty & AND3 (q1,p3,p2) is empty ) or ( not AND3 (q1,p3,p2) is empty & m4 is empty ) or ( not n4 is empty & AND4 (p3,p2,p1,cb1) is empty ) or ( not AND4 (p3,p2,p1,cb1) is empty & n4 is empty ) or ( not t4 is empty & NOR4 (l4,m4,n4,q3) is empty ) or ( not NOR4 (l4,m4,n4,q3) is empty & t4 is empty ) or ( not s4 is empty & XOR2 (t4,sd4) is empty ) or ( not XOR2 (t4,sd4) is empty & s4 is empty ) or ( not l5 is empty & AND2 (q3,p4) is empty ) or ( not AND2 (q3,p4) is empty & l5 is empty ) or ( not m5 is empty & AND3 (q2,p4,p3) is empty ) or ( not AND3 (q2,p4,p3) is empty & m5 is empty ) or ( not n5 is empty & AND4 (q1,p4,p3,p2) is empty ) or ( not AND4 (q1,p4,p3,p2) is empty & n5 is empty ) or ( not o5 is empty & AND5 (p4,p3,p2,p1,cb1) is empty ) or ( not AND5 (p4,p3,p2,p1,cb1) is empty & o5 is empty ) or ( not c4 is empty & NOR5 (q4,l5,m5,n5,o5) is empty ) or ( not NOR5 (q4,l5,m5,n5,o5) is empty & c4 is empty ) or ( ( 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 ) ) )

thus not ( ( 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 ) ) ) :: thesis: verum

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 ) ; :: thesis: ( ( not p2 is empty & NAND2 (x2,y2) is empty ) or ( not NAND2 (x2,y2) is empty & p2 is empty ) or ( not sd2 is empty & MODADD2 (x2,y2) is empty ) or ( not MODADD2 (x2,y2) is empty & sd2 is empty ) or ( not q3 is empty & NOR2 (x3,y3) is empty ) or ( not NOR2 (x3,y3) is empty & q3 is empty ) or ( not p3 is empty & NAND2 (x3,y3) is empty ) or ( not NAND2 (x3,y3) is empty & p3 is empty ) or ( not sd3 is empty & MODADD2 (x3,y3) is empty ) or ( not MODADD2 (x3,y3) is empty & sd3 is empty ) or ( not q4 is empty & NOR2 (x4,y4) is empty ) or ( not NOR2 (x4,y4) is empty & q4 is empty ) or ( not p4 is empty & NAND2 (x4,y4) is empty ) or ( not NAND2 (x4,y4) is empty & p4 is empty ) or ( not sd4 is empty & MODADD2 (x4,y4) is empty ) or ( not MODADD2 (x4,y4) is empty & sd4 is empty ) or ( not cb1 is empty & NOT1 c1 is empty ) or ( not NOT1 c1 is empty & cb1 is empty ) or ( not cb2 is empty & NOT1 cb1 is empty ) or ( not NOT1 cb1 is empty & cb2 is empty ) or ( not s1 is empty & XOR2 (cb2,sd1) is empty ) or ( not XOR2 (cb2,sd1) is empty & s1 is empty ) or ( not l2 is empty & AND2 (cb1,p1) is empty ) or ( not AND2 (cb1,p1) is empty & l2 is empty ) or ( not t2 is empty & NOR2 (l2,q1) is empty ) or ( not NOR2 (l2,q1) is empty & t2 is empty ) or ( not s2 is empty & XOR2 (t2,sd2) is empty ) or ( not XOR2 (t2,sd2) is empty & s2 is empty ) or ( not l3 is empty & AND2 (q1,p2) is empty ) or ( not AND2 (q1,p2) is empty & l3 is empty ) or ( not m3 is empty & AND3 (p2,p1,cb1) is empty ) or ( not AND3 (p2,p1,cb1) is empty & m3 is empty ) or ( not t3 is empty & NOR3 (l3,m3,q2) is empty ) or ( not NOR3 (l3,m3,q2) is empty & t3 is empty ) or ( not s3 is empty & XOR2 (t3,sd3) is empty ) or ( not XOR2 (t3,sd3) is empty & s3 is empty ) or ( not l4 is empty & AND2 (q2,p3) is empty ) or ( not AND2 (q2,p3) is empty & l4 is empty ) or ( not m4 is empty & AND3 (q1,p3,p2) is empty ) or ( not AND3 (q1,p3,p2) is empty & m4 is empty ) or ( not n4 is empty & AND4 (p3,p2,p1,cb1) is empty ) or ( not AND4 (p3,p2,p1,cb1) is empty & n4 is empty ) or ( not t4 is empty & NOR4 (l4,m4,n4,q3) is empty ) or ( not NOR4 (l4,m4,n4,q3) is empty & t4 is empty ) or ( not s4 is empty & XOR2 (t4,sd4) is empty ) or ( not XOR2 (t4,sd4) is empty & s4 is empty ) or ( not l5 is empty & AND2 (q3,p4) is empty ) or ( not AND2 (q3,p4) is empty & l5 is empty ) or ( not m5 is empty & AND3 (q2,p4,p3) is empty ) or ( not AND3 (q2,p4,p3) is empty & m5 is empty ) or ( not n5 is empty & AND4 (q1,p4,p3,p2) is empty ) or ( not AND4 (q1,p4,p3,p2) is empty & n5 is empty ) or ( not o5 is empty & AND5 (p4,p3,p2,p1,cb1) is empty ) or ( not AND5 (p4,p3,p2,p1,cb1) is empty & o5 is empty ) or ( not c4 is empty & NOR5 (q4,l5,m5,n5,o5) is empty ) or ( not NOR5 (q4,l5,m5,n5,o5) is empty & c4 is empty ) or ( ( 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 ) ) )

thus not ( ( 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 ) ) ) :: thesis: verum

proof

assume that

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;

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;

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;

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;

A49: ( not q4 is empty iff ( x4 is empty & y4 is empty ) ) by A10;

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

end;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

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 ) )

A29:
( not q1 is empty iff ( x1 is empty & y1 is empty ) )
by A1;assume A28:
not ADD1 (x1,y1,c1) is empty
; :: thesis: not s1 is empty

end;per cases
( ( not c1 is empty & sd1 is empty ) or ( c1 is empty & not sd1 is empty ) )
by A26, A28;

end;

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 ) )

A32:
( not cb1 is empty iff c1 is empty )
by A13;assume A31:
not s2 is empty
; :: thesis: not ADD2 (x2,y2,x1,y1,c1) is empty

end;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;

end;

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

end;

end;

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 ) )

A34:
( not q2 is empty iff ( x2 is empty & y2 is empty ) )
by A4;assume A33:
not ADD2 (x2,y2,x1,y1,c1) is empty
; :: thesis: not s2 is empty

end;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;

end;

suppose
( ( not l2 is empty or not q1 is empty ) & not sd2 is empty )
; :: thesis: not s2 is empty

end;

end;

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

end;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;

end;

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;( 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

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;hence not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A18, A25, A35, A36, A40; :: thesis: verum

suppose
( not q2 is empty & not sd3 is empty )
; :: thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty

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 ) )

A42:
( not p3 is empty & not x3 is empty iff y3 is empty )
by A8;assume A41:
not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
; :: thesis: not s3 is empty

end;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;

end;

suppose
( l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty )
; :: thesis: not s3 is empty

end;

end;

suppose
( l3 is empty & m3 is empty & q2 is empty & not x3 is empty & not y3 is empty )
; :: thesis: not s3 is empty

end;

end;

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

end;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;

end;

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

end;

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

end;

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

end;

end;

suppose
( not q3 is empty & not sd4 is empty )
; :: thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty

end;

end;

hereby :: thesis: ( not c4 is empty iff not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty )

A48:
( not p4 is empty & not x4 is empty iff y4 is empty )
by A11;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

end;thus not s4 is empty :: thesis: verum

proof

assume A47:
s4 is empty
; :: thesis: contradiction

end;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;

end;

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

end;

end;

suppose
( not q1 is empty & not p3 is empty & not p2 is empty & sd4 is empty )
; :: thesis: contradiction

end;

end;

suppose
( not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty & sd4 is empty )
; :: thesis: contradiction

end;

end;

A49: ( not q4 is empty iff ( x4 is empty & y4 is empty ) ) by A10;

now :: thesis: ( q4 is empty & l5 is empty & m5 is empty & n5 is empty & o5 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty )

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 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

end;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;

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;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;

end;

suppose
( not q1 is empty & not p4 is empty & not p3 is empty & not p2 is empty )
; :: thesis: contradiction

end;

end;

suppose
( not p4 is empty & not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty )
; :: thesis: contradiction

end;

end;