let x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, c01, c02, q11, q12, c11, c12, q21, q22, c21, c22 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)),{}) is empty ) & ( not XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),{}) is empty implies not q02 is empty ) & ( not c02 is empty implies not MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),{}) is empty ) & ( not MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),{}) is empty implies not c02 is empty ) & ( not q11 is empty implies not XOR3 (q02,(AND2 (x0,y2)),c01) is empty ) & ( not XOR3 (q02,(AND2 (x0,y2)),c01) is empty implies not q11 is empty ) & ( not c11 is empty implies not MAJ3 (q02,(AND2 (x0,y2)),c01) is empty ) & ( not MAJ3 (q02,(AND2 (x0,y2)),c01) is empty implies not c11 is empty ) & ( not q12 is empty implies not XOR3 ((AND2 (x2,y1)),(AND2 (x1,y2)),c02) is empty ) & ( not XOR3 ((AND2 (x2,y1)),(AND2 (x1,y2)),c02) is empty implies not q12 is empty ) & ( not c12 is empty implies not MAJ3 ((AND2 (x2,y1)),(AND2 (x1,y2)),c02) is empty ) & ( not MAJ3 ((AND2 (x2,y1)),(AND2 (x1,y2)),c02) is empty implies not c12 is empty ) & ( not q21 is empty implies not XOR3 (q12,{},c11) is empty ) & ( not XOR3 (q12,{},c11) is empty implies not q21 is empty ) & ( not c21 is empty implies not MAJ3 (q12,{},c11) is empty ) & ( not MAJ3 (q12,{},c11) is empty implies not c21 is empty ) & ( not q22 is empty implies not XOR3 ((AND2 (x2,y2)),c21,c12) is empty ) & ( not XOR3 ((AND2 (x2,y2)),c21,c12) is empty implies not q22 is empty ) & ( not c22 is empty implies not MAJ3 ((AND2 (x2,y2)),c21,c12) is empty ) & ( not MAJ3 ((AND2 (x2,y2)),c21,c12) is empty implies not c22 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 q21 is empty ) & ( not q21 is empty implies not z3 is empty ) & ( not z4 is empty implies not q22 is empty ) & ( not q22 is empty implies not z4 is empty ) & ( not z5 is empty implies not c22 is empty ) & ( not c22 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 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)),{}) is empty ) & ( not XOR3 ((AND2 (x2,y0)),(AND2 (x1,y1)),{}) is empty implies not q02 is empty ) )
and
A4:
( not c02 is empty iff not MAJ3 ((AND2 (x2,y0)),(AND2 (x1,y1)),{}) is empty )
and
A5:
( not q11 is empty iff not XOR3 (q02,(AND2 (x0,y2)),c01) is empty )
and
A6:
( not c11 is empty iff not MAJ3 (q02,(AND2 (x0,y2)),c01) is empty )
and
A7:
( not q12 is empty iff not XOR3 ((AND2 (x2,y1)),(AND2 (x1,y2)),c02) is empty )
and
A8:
( not c12 is empty iff not MAJ3 ((AND2 (x2,y1)),(AND2 (x1,y2)),c02) is empty )
and
A9:
( not q21 is empty iff not XOR3 (q12,{},c11) is empty )
and
A10:
( not c21 is empty iff not MAJ3 (q12,{},c11) is empty )
and
A11:
( not q22 is empty iff not XOR3 ((AND2 (x2,y2)),c21,c12) is empty )
and
A12:
( not c22 is empty iff not MAJ3 ((AND2 (x2,y2)),c21,c12) is empty )
and
A13:
( not z0 is empty iff not q00 is empty )
and
A14:
( not z1 is empty iff not q01 is empty )
and
A15:
( not z2 is empty iff not q11 is empty )
and
A16:
( not z3 is empty iff not q21 is empty )
and
A17:
( not z4 is empty iff not q22 is empty )
and
A18:
( not z5 is empty iff not c22 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 ) )
set x0y2 = AND2 (x0,y2);
A19:
( ( ( not q02 is empty & not AND2 (x0,y2) is empty ) or ( not AND2 (x0,y2) is empty & not c01 is empty ) or ( not c01 is empty & not q02 is empty ) ) iff not c11 is empty )
by A6;
thus
( not z0 is empty iff not MULT310 (x2,x1,y1,x0,y0) is empty )
by A1, A13; ( ( 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, A14; ( ( 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 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;
then A21:
( ( ( ( ( not AND2 (x2,y0) is empty & AND2 (x1,y1) is empty ) or ( AND2 (x2,y0) is empty & not AND2 (x1,y1) is empty ) ) & MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) 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 MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) ) iff not MULT312 (x2,x1,y1,x0,y0) is empty )
;
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 (x1,y0) is empty or AND2 (x0,y1) 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 (x1,y0) is empty & not AND2 (x0,y1) is empty ) ) iff not MULT312 (x2,x1,y1,x0,y0) is empty )
by A20;
( ( ( ( ( not q02 is empty & AND2 (x0,y2) is empty ) or ( q02 is empty & not AND2 (x0,y2) is empty ) ) & c01 is empty ) or ( not ( not q02 is empty & AND2 (x0,y2) is empty ) & not ( q02 is empty & not AND2 (x0,y2) is empty ) & not c01 is empty ) ) iff not q11 is empty )
by A5;
hence
( not z2 is empty iff not MULT321 (x2,y2,x1,y1,x0,y0) is empty )
by A3, A15, A21; ( ( 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 x1y2 = AND2 (x1,y2);
set x2y1 = AND2 (x2,y1);
A23:
( ( ( ( ( not AND2 (x2,y1) is empty & AND2 (x1,y2) is empty ) or ( AND2 (x2,y1) is empty & not AND2 (x1,y2) is empty ) ) & c02 is empty ) or ( not ( not AND2 (x2,y1) is empty & AND2 (x1,y2) is empty ) & not ( AND2 (x2,y1) is empty & not AND2 (x1,y2) is empty ) & not c02 is empty ) ) iff not q12 is empty )
by A7;
set m324 = MULT324 (x2,y2,x1,y1,x0,y0);
set m323 = MULT323 (x2,y2,x1,y1,x0,y0);
set m314 = MULT314 (x2,x1,y1,x0,y0);
set x2y2 = AND2 (x2,y2);
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 m322 = MULT322 (x2,y2,x1,y1,x0,y0);
set m313 = MULT313 (x2,x1,y1,x0,y0);
A25: 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, A4, A9, A16, A19, A23, A22, A25; ( ( 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 ) )
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 & c21 is empty ) or ( AND2 (x2,y2) is empty & not c21 is empty ) ) & c12 is empty ) or ( not ( not AND2 (x2,y2) is empty & c21 is empty ) & not ( AND2 (x2,y2) is empty & not c21 is empty ) & not c12 is empty ) ) iff not q22 is empty )
by A11;
hence
( not z4 is empty iff not MULT323 (x2,y2,x1,y1,x0,y0) is empty )
by A3, A4, A8, A10, A17, A19, A23, A22, A25, A24, A26; ( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty )
A27: 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
;
( ( ( not AND2 (x2,y2) is empty & not c21 is empty ) or ( not c21 is empty & not c12 is empty ) or ( not c12 is empty & not AND2 (x2,y2) is empty ) ) iff not c22 is empty )
by A12;
hence
( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty )
by A3, A4, A8, A10, A18, A19, A23, A22, A25, A24, A27; verum