let x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, q03, c01, c02, c03, q11, q12, q13, c11, c12, c13 be set ; not ( ( not q00 is empty implies not AND2 (x0,y0) is empty ) & ( not AND2 (x0,y0) is empty implies not q00 is empty ) & ( not q01 is empty implies not XOR3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) & ( not XOR3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty implies not q01 is empty ) & ( not c01 is empty implies not MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) & ( not MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty implies not c01 is empty ) & ( not q02 is empty implies not XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty ) & ( not XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty implies not q02 is empty ) & ( not c02 is empty implies not MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty ) & ( not MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty implies not c02 is empty ) & ( not q03 is empty implies not XOR3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty ) & ( not XOR3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty implies not q03 is empty ) & ( not c03 is empty implies not MAJ3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty ) & ( not MAJ3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty implies not c03 is empty ) & ( not q11 is empty implies not XOR3 (q02,c01,{}) is empty ) & ( not XOR3 (q02,c01,{}) is empty implies not q11 is empty ) & ( not c11 is empty implies not MAJ3 (q02,c01,{}) is empty ) & ( not MAJ3 (q02,c01,{}) is empty implies not c11 is empty ) & ( not q12 is empty implies not XOR3 (q03,c02,c11) is empty ) & ( not XOR3 (q03,c02,c11) is empty implies not q12 is empty ) & ( not c12 is empty implies not MAJ3 (q03,c02,c11) is empty ) & ( not MAJ3 (q03,c02,c11) is empty implies not c12 is empty ) & ( not q13 is empty implies not XOR3 ((AND2 (x2,y2)),c03,c12) is empty ) & ( not XOR3 ((AND2 (x2,y2)),c03,c12) is empty implies not q13 is empty ) & ( not c13 is empty implies not MAJ3 ((AND2 (x2,y2)),c03,c12) is empty ) & ( not MAJ3 ((AND2 (x2,y2)),c03,c12) is empty implies not c13 is empty ) & ( not z0 is empty implies not q00 is empty ) & ( not q00 is empty implies not z0 is empty ) & ( not z1 is empty implies not q01 is empty ) & ( not q01 is empty implies not z1 is empty ) & ( not z2 is empty implies not q11 is empty ) & ( not q11 is empty implies not z2 is empty ) & ( not z3 is empty implies not q12 is empty ) & ( not q12 is empty implies not z3 is empty ) & ( not z4 is empty implies not q13 is empty ) & ( not q13 is empty implies not z4 is empty ) & ( not z5 is empty implies not c13 is empty ) & ( not c13 is empty implies not z5 is empty ) & not ( ( not z0 is empty implies not MULT310 (x2,x1,y1,x0,y0) is empty ) & ( not MULT310 (x2,x1,y1,x0,y0) is empty implies not z0 is empty ) & ( not z1 is empty implies not MULT311 (x2,x1,y1,x0,y0) is empty ) & ( not MULT311 (x2,x1,y1,x0,y0) is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT321 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT321 (x2,y2,x1,y1,x0,y0) is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) ) )
assume that
A1:
( not q00 is empty iff not AND2 (x0,y0) is empty )
and
A2:
( not q01 is empty iff not XOR3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty )
and
A3:
( not c01 is empty iff not MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty )
and
A4:
( not q02 is empty iff not XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty )
and
A5:
( not c02 is empty iff not MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x0,y2))) is empty )
and
A6:
( not q03 is empty iff not XOR3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty )
and
A7:
( not c03 is empty iff not MAJ3 ((AND2 (x2,y1)),(AND2 (x1,y2)),{}) is empty )
and
A8:
( not q11 is empty iff not XOR3 (q02,c01,{}) is empty )
and
A9:
( not c11 is empty iff not MAJ3 (q02,c01,{}) is empty )
and
A10:
( not q12 is empty iff not XOR3 (q03,c02,c11) is empty )
and
A11:
( not c12 is empty iff not MAJ3 (q03,c02,c11) is empty )
and
A12:
( not q13 is empty iff not XOR3 ((AND2 (x2,y2)),c03,c12) is empty )
and
A13:
( not c13 is empty iff not MAJ3 ((AND2 (x2,y2)),c03,c12) is empty )
and
A14:
( not z0 is empty iff not q00 is empty )
and
A15:
( not z1 is empty iff not q01 is empty )
and
A16:
( not z2 is empty iff not q11 is empty )
and
A17:
( not z3 is empty iff not q12 is empty )
and
A18:
( not z4 is empty iff not q13 is empty )
and
A19:
( not z5 is empty iff not c13 is empty )
; ( ( not z0 is empty implies not MULT310 (x2,x1,y1,x0,y0) is empty ) & ( not MULT310 (x2,x1,y1,x0,y0) is empty implies not z0 is empty ) & ( not z1 is empty implies not MULT311 (x2,x1,y1,x0,y0) is empty ) & ( not MULT311 (x2,x1,y1,x0,y0) is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT321 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT321 (x2,y2,x1,y1,x0,y0) is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
thus
( not z0 is empty iff not MULT310 (x2,x1,y1,x0,y0) is empty )
by A1, A14; ( ( not z1 is empty implies not MULT311 (x2,x1,y1,x0,y0) is empty ) & ( not MULT311 (x2,x1,y1,x0,y0) is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT321 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT321 (x2,y2,x1,y1,x0,y0) is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
thus
( not z1 is empty iff not MULT311 (x2,x1,y1,x0,y0) is empty )
by A2, A15; ( ( not z2 is empty implies not MULT321 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT321 (x2,y2,x1,y1,x0,y0) is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
set m312 = MULT312 (x2,x1,y1,x0,y0);
set x0y2 = AND2 (x0,y2);
set x1y1 = AND2 (x1,y1);
set x0y1 = AND2 (x0,y1);
set x2y0 = AND2 (x2,y0);
set x1y0 = AND2 (x1,y0);
A20:
MULT312 (x2,x1,y1,x0,y0) = XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{})))
by GATE_1:def 35;
set m323 = MULT323 (x2,y2,x1,y1,x0,y0);
set m314 = MULT314 (x2,x1,y1,x0,y0);
set x2y2 = AND2 (x2,y2);
set m322 = MULT322 (x2,y2,x1,y1,x0,y0);
set m313 = MULT313 (x2,x1,y1,x0,y0);
set x1y2 = AND2 (x1,y2);
set x2y1 = AND2 (x2,y1);
A21:
( ( ( not AND2 (x2,y1) is empty & AND2 (x1,y2) is empty ) or ( AND2 (x2,y1) is empty & not AND2 (x1,y2) is empty ) ) iff not q03 is empty )
by A6;
A22:
( ( ( ( ( not AND2 (x2,y0) is empty & AND2 (x1,y1) is empty ) or ( AND2 (x2,y0) is empty & not AND2 (x1,y1) is empty ) ) & AND2 (x0,y2) is empty ) or ( not ( not AND2 (x2,y0) is empty & AND2 (x1,y1) is empty ) & not ( AND2 (x2,y0) is empty & not AND2 (x1,y1) is empty ) & not AND2 (x0,y2) is empty ) ) iff not q02 is empty )
by A4;
hence
( not z2 is empty iff not MULT321 (x2,y2,x1,y1,x0,y0) is empty )
by A3, A8, A16, A20; ( ( not z3 is empty implies not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT322 (x2,y2,x1,y1,x0,y0) is empty implies not z3 is empty ) & ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
A23: MULT313 (x2,x1,y1,x0,y0) =
XOR3 ({},(AND2 (x2,y1)),(CARR2 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{})))
by GATE_1:def 37
.=
XOR3 ({},(AND2 (x2,y1)),(MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{})))))
by GATE_1:def 36
;
MULT322 (x2,y2,x1,y1,x0,y0) = XOR3 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MAJ3 ((MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{})))
by GATE_1:def 35;
hence
( not z3 is empty iff not MULT322 (x2,y2,x1,y1,x0,y0) is empty )
by A3, A5, A9, A10, A17, A22, A21, A20, A23; ( ( not z4 is empty implies not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT323 (x2,y2,x1,y1,x0,y0) is empty implies not z4 is empty ) & ( not z5 is empty implies not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) & ( not MULT324 (x2,y2,x1,y1,x0,y0) is empty implies not z5 is empty ) )
A24: MULT314 (x2,x1,y1,x0,y0) =
MAJ3 ({},(AND2 (x2,y1)),(CARR2 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{})))
by GATE_1:def 38
.=
MAJ3 ({},(AND2 (x2,y1)),(MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),(MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{})))))
by GATE_1:def 36
;
set m324 = MULT324 (x2,y2,x1,y1,x0,y0);
A25: MULT324 (x2,y2,x1,y1,x0,y0) =
MAJ3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(CARR2 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{})))
by GATE_1:def 38
.=
MAJ3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MAJ3 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MAJ3 ((MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{})))))
by GATE_1:def 36
;
A26: MULT323 (x2,y2,x1,y1,x0,y0) =
XOR3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(CARR2 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{})))
by GATE_1:def 37
.=
XOR3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MAJ3 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MAJ3 ((MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{})))))
by GATE_1:def 36
;
( ( ( ( ( not AND2 (x2,y2) is empty & c03 is empty ) or ( AND2 (x2,y2) is empty & not c03 is empty ) ) & c12 is empty ) or ( not ( not AND2 (x2,y2) is empty & c03 is empty ) & not ( AND2 (x2,y2) is empty & not c03 is empty ) & not c12 is empty ) ) iff not q13 is empty )
by A12;
hence
( not z4 is empty iff not MULT323 (x2,y2,x1,y1,x0,y0) is empty )
by A3, A5, A7, A9, A11, A18, A22, A21, A20, A23, A24, A26; ( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty )
( ( ( not AND2 (x2,y2) is empty & not c03 is empty ) or ( not c03 is empty & not c12 is empty ) or ( not c12 is empty & not AND2 (x2,y2) is empty ) ) iff not c13 is empty )
by A13;
hence
( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty )
by A3, A5, A7, A9, A11, A19, A22, A21, A20, A23, A24, A25; verum