:: Correctness of the High Speed Array Multiplier Circuits
:: by Hiroshi Yamazaki and Katsumi Wasaki
::
:: Received August 28, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users


::The following 4 definitions are for normal 2-by-2 bit multiplier.
definition
let x0, x1, y0, y1 be set ;
func MULT210 (x1,y1,x0,y0) -> set equals :: GATE_5:def 1
 AND2 (x0,y0);
correctness
coherence
AND2 (x0,y0) is set ;
;
func MULT211 (x1,y1,x0,y0) -> set equals :: GATE_5:def 2
 ADD1 ((AND2 (x1,y0)),(AND2 (x0,y1)),{});
correctness
coherence
ADD1 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is set ;
;
func MULT212 (x1,y1,x0,y0) -> set equals :: GATE_5:def 3
 ADD2 ({},(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});
correctness
coherence
ADD2 ({},(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{}) is set ;
;
func MULT213 (x1,y1,x0,y0) -> set equals :: GATE_5:def 4
 CARR2 ({},(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});
correctness
coherence
CARR2 ({},(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{}) is set ;
;
end;

:: deftheorem defines MULT210 GATE_5:def 1 :
for x0, x1, y0, y1 being set holds MULT210 (x1,y1,x0,y0) = AND2 (x0,y0);

:: deftheorem defines MULT211 GATE_5:def 2 :
for x0, x1, y0, y1 being set holds MULT211 (x1,y1,x0,y0) = ADD1 ((AND2 (x1,y0)),(AND2 (x0,y1)),{});

:: deftheorem defines MULT212 GATE_5:def 3 :
for x0, x1, y0, y1 being set holds MULT212 (x1,y1,x0,y0) = ADD2 ({},(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});

:: deftheorem defines MULT213 GATE_5:def 4 :
for x0, x1, y0, y1 being set holds MULT213 (x1,y1,x0,y0) = CARR2 ({},(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});

::
:: Logical Equivalence of 2-by-2 bit Plain Array Multiplier.
::
::The following theorem shows that
:: outputs of '2-by-2 bit plain Array Multiplier' are equivalent to
:: outputs of '2-by-2 normal Multiplier'
:: We assume that there is no feedback loop in multiplier.
theorem :: GATE_5:1
for x0, x1, y0, y1, z0, z1, z2, z3, q00, q01, c01, q11, c11 being set holds
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 q11 is empty implies not XOR3 ((AND2 (x1,y1)),{},c01) is empty ) & ( not XOR3 ((AND2 (x1,y1)),{},c01) is empty implies not q11 is empty ) & ( not c11 is empty implies not MAJ3 ((AND2 (x1,y1)),{},c01) is empty ) & ( not MAJ3 ((AND2 (x1,y1)),{},c01) is empty implies not c11 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 c11 is empty ) & ( not c11 is empty implies not z3 is empty ) & not ( ( not z0 is empty implies not MULT210 (x1,y1,x0,y0) is empty ) & ( not MULT210 (x1,y1,x0,y0) is empty implies not z0 is empty ) & ( not z1 is empty implies not MULT211 (x1,y1,x0,y0) is empty ) & ( not MULT211 (x1,y1,x0,y0) is empty implies not z1 is empty ) & ( not z2 is empty implies not MULT212 (x1,y1,x0,y0) is empty ) & ( not MULT212 (x1,y1,x0,y0) is empty implies not z2 is empty ) & ( not z3 is empty implies not MULT213 (x1,y1,x0,y0) is empty ) & ( not MULT213 (x1,y1,x0,y0) is empty implies not z3 is empty ) ) )
proof end;

::
:: Logical Equivalence of 3-by-3 bit Plain Array Multiplier.
::
::[sequence 1]
::The following 5 definitions are for normal 3-by-2 bit multiplier.
definition
let x0, x1, x2, y0, y1 be set ;
func MULT310 (x2,x1,y1,x0,y0) -> set equals :: GATE_5:def 5
 AND2 (x0,y0);
correctness
coherence
AND2 (x0,y0) is set ;
;
func MULT311 (x2,x1,y1,x0,y0) -> set equals :: GATE_5:def 6
 ADD1 ((AND2 (x1,y0)),(AND2 (x0,y1)),{});
correctness
coherence
ADD1 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is set ;
;
func MULT312 (x2,x1,y1,x0,y0) -> set equals :: GATE_5:def 7
 ADD2 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});
correctness
coherence
ADD2 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{}) is set ;
;
func MULT313 (x2,x1,y1,x0,y0) -> set equals :: GATE_5:def 8
 ADD3 ({},(AND2 (x2,y1)),(AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});
correctness
coherence
ADD3 ({},(AND2 (x2,y1)),(AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{}) is set ;
;
func MULT314 (x2,x1,y1,x0,y0) -> set equals :: GATE_5:def 9
 CARR3 ({},(AND2 (x2,y1)),(AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});
correctness
coherence
CARR3 ({},(AND2 (x2,y1)),(AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{}) is set ;
;
end;

:: deftheorem defines MULT310 GATE_5:def 5 :
for x0, x1, x2, y0, y1 being set holds MULT310 (x2,x1,y1,x0,y0) = AND2 (x0,y0);

:: deftheorem defines MULT311 GATE_5:def 6 :
for x0, x1, x2, y0, y1 being set holds MULT311 (x2,x1,y1,x0,y0) = ADD1 ((AND2 (x1,y0)),(AND2 (x0,y1)),{});

:: deftheorem defines MULT312 GATE_5:def 7 :
for x0, x1, x2, y0, y1 being set holds MULT312 (x2,x1,y1,x0,y0) = ADD2 ((AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});

:: deftheorem defines MULT313 GATE_5:def 8 :
for x0, x1, x2, y0, y1 being set holds MULT313 (x2,x1,y1,x0,y0) = ADD3 ({},(AND2 (x2,y1)),(AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});

:: deftheorem defines MULT314 GATE_5:def 9 :
for x0, x1, x2, y0, y1 being set holds MULT314 (x2,x1,y1,x0,y0) = CARR3 ({},(AND2 (x2,y1)),(AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});

::[sequence 2]
::The following 4 definitions are for normal 3-by-3 bit multiplier.
definition
let x0, x1, x2, y0, y1, y2 be set ;
func MULT321 (x2,y2,x1,y1,x0,y0) -> set equals :: GATE_5:def 10
 ADD1 ((MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{});
correctness
coherence
ADD1 ((MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{}) is set ;
;
func MULT322 (x2,y2,x1,y1,x0,y0) -> set equals :: GATE_5:def 11
 ADD2 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{});
correctness
coherence
ADD2 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{}) is set ;
;
func MULT323 (x2,y2,x1,y1,x0,y0) -> set equals :: GATE_5:def 12
 ADD3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{});
correctness
coherence
ADD3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{}) is set ;
;
func MULT324 (x2,y2,x1,y1,x0,y0) -> set equals :: GATE_5:def 13
 CARR3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{});
correctness
coherence
CARR3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{}) is set ;
;
end;

:: deftheorem defines MULT321 GATE_5:def 10 :
for x0, x1, x2, y0, y1, y2 being set holds MULT321 (x2,y2,x1,y1,x0,y0) = ADD1 ((MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{});

:: deftheorem defines MULT322 GATE_5:def 11 :
for x0, x1, x2, y0, y1, y2 being set holds MULT322 (x2,y2,x1,y1,x0,y0) = ADD2 ((MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{});

:: deftheorem defines MULT323 GATE_5:def 12 :
for x0, x1, x2, y0, y1, y2 being set holds MULT323 (x2,y2,x1,y1,x0,y0) = ADD3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{});

:: deftheorem defines MULT324 GATE_5:def 13 :
for x0, x1, x2, y0, y1, y2 being set holds MULT324 (x2,y2,x1,y1,x0,y0) = CARR3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{});

::The following theorem shows that
:: outputs of '3-by-3 bit plain Array Multiplier' are equivalent to
:: outputs of '3-by-3 normal (sequencial) Multiplier'
:: We assume that there is no feedback loop in multiplier.
theorem :: GATE_5:2
for 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 being set holds
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 ) ) )
proof end;

::
:: Logical Equivalence of 3-by-3 bit Wallace tree Multiplier.
::
::The following theorem shows that
:: outputs of '3-by-3 bit Wallace tree Multiplier' are equivalent to
:: outputs of '3-by-3 normal (sequencial) Multiplier'
:: We assume that there is no feedback loop in multiplier.
theorem :: GATE_5:3
for 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 being set holds
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 ) ) )
proof end;

notation
let a1, b1, c be set ;
synonym CLAADD1 (a1,b1,c) for XOR3 (a1,b1,c);
synonym CLACARR1 (a1,b1,c) for MAJ3 (a1,b1,c);
end;

::The following two definitions are for CLA 2 bit adder.
definition
let a1, b1, a2, b2, c be set ;
func CLAADD2 (a2,b2,a1,b1,c) -> set equals :: GATE_5:def 14
 XOR3 (a2,b2,(MAJ3 (a1,b1,c)));
correctness
coherence
XOR3 (a2,b2,(MAJ3 (a1,b1,c))) is set ;
;
func CLACARR2 (a2,b2,a1,b1,c) -> set equals :: GATE_5:def 15
 OR2 ((AND2 (a2,b2)),(AND2 ((OR2 (a2,b2)),(MAJ3 (a1,b1,c)))));
correctness
coherence
OR2 ((AND2 (a2,b2)),(AND2 ((OR2 (a2,b2)),(MAJ3 (a1,b1,c))))) is set ;
;
end;

:: deftheorem defines CLAADD2 GATE_5:def 14 :
for a1, b1, a2, b2, c being set holds CLAADD2 (a2,b2,a1,b1,c) = XOR3 (a2,b2,(MAJ3 (a1,b1,c)));

:: deftheorem defines CLACARR2 GATE_5:def 15 :
for a1, b1, a2, b2, c being set holds CLACARR2 (a2,b2,a1,b1,c) = OR2 ((AND2 (a2,b2)),(AND2 ((OR2 (a2,b2)),(MAJ3 (a1,b1,c)))));

::The following two definitions are for CLA 3 bit adder.
definition
let a1, b1, a2, b2, a3, b3, c be set ;
func CLAADD3 (a3,b3,a2,b2,a1,b1,c) -> set equals :: GATE_5:def 16
 XOR3 (a3,b3,(CLACARR2 (a2,b2,a1,b1,c)));
correctness
coherence
XOR3 (a3,b3,(CLACARR2 (a2,b2,a1,b1,c))) is set ;
;
func CLACARR3 (a3,b3,a2,b2,a1,b1,c) -> set equals :: GATE_5:def 17
 OR3 ((AND2 (a3,b3)),(AND2 ((OR2 (a3,b3)),(AND2 (a2,b2)))),(AND3 ((OR2 (a3,b3)),(OR2 (a2,b2)),(MAJ3 (a1,b1,c)))));
correctness
coherence
OR3 ((AND2 (a3,b3)),(AND2 ((OR2 (a3,b3)),(AND2 (a2,b2)))),(AND3 ((OR2 (a3,b3)),(OR2 (a2,b2)),(MAJ3 (a1,b1,c))))) is set ;
;
end;

:: deftheorem defines CLAADD3 GATE_5:def 16 :
for a1, b1, a2, b2, a3, b3, c being set holds CLAADD3 (a3,b3,a2,b2,a1,b1,c) = XOR3 (a3,b3,(CLACARR2 (a2,b2,a1,b1,c)));

:: deftheorem defines CLACARR3 GATE_5:def 17 :
for a1, b1, a2, b2, a3, b3, c being set holds CLACARR3 (a3,b3,a2,b2,a1,b1,c) = OR3 ((AND2 (a3,b3)),(AND2 ((OR2 (a3,b3)),(AND2 (a2,b2)))),(AND3 ((OR2 (a3,b3)),(OR2 (a2,b2)),(MAJ3 (a1,b1,c)))));

::The following two definitions are for CLA 4 bit adder.
definition
let a1, b1, a2, b2, a3, b3, a4, b4, c be set ;
func CLAADD4 (a4,b4,a3,b3,a2,b2,a1,b1,c) -> set equals :: GATE_5:def 18
 XOR3 (a4,b4,(CLACARR3 (a3,b3,a2,b2,a1,b1,c)));
correctness
coherence
XOR3 (a4,b4,(CLACARR3 (a3,b3,a2,b2,a1,b1,c))) is set ;
;
func CLACARR4 (a4,b4,a3,b3,a2,b2,a1,b1,c) -> set equals :: GATE_5:def 19
 OR4 ((AND2 (a4,b4)),(AND2 ((OR2 (a4,b4)),(AND2 (a3,b3)))),(AND3 ((OR2 (a4,b4)),(OR2 (a3,b3)),(AND2 (a2,b2)))),(AND4 ((OR2 (a4,b4)),(OR2 (a3,b3)),(OR2 (a2,b2)),(MAJ3 (a1,b1,c)))));
correctness
coherence
OR4 ((AND2 (a4,b4)),(AND2 ((OR2 (a4,b4)),(AND2 (a3,b3)))),(AND3 ((OR2 (a4,b4)),(OR2 (a3,b3)),(AND2 (a2,b2)))),(AND4 ((OR2 (a4,b4)),(OR2 (a3,b3)),(OR2 (a2,b2)),(MAJ3 (a1,b1,c))))) is set ;
;
end;

:: deftheorem defines CLAADD4 GATE_5:def 18 :
for a1, b1, a2, b2, a3, b3, a4, b4, c being set holds CLAADD4 (a4,b4,a3,b3,a2,b2,a1,b1,c) = XOR3 (a4,b4,(CLACARR3 (a3,b3,a2,b2,a1,b1,c)));

:: deftheorem defines CLACARR4 GATE_5:def 19 :
for a1, b1, a2, b2, a3, b3, a4, b4, c being set holds CLACARR4 (a4,b4,a3,b3,a2,b2,a1,b1,c) = OR4 ((AND2 (a4,b4)),(AND2 ((OR2 (a4,b4)),(AND2 (a3,b3)))),(AND3 ((OR2 (a4,b4)),(OR2 (a3,b3)),(AND2 (a2,b2)))),(AND4 ((OR2 (a4,b4)),(OR2 (a3,b3)),(OR2 (a2,b2)),(MAJ3 (a1,b1,c)))));

::The following theorem shows that
:: outputs of '3-by-3 bit Wallace tree Multiplier' by using Carry Look-up
:: Ahead Adder are equivalent to outputs of '3-by-3 normal (sequencial)
:: Multiplier'.
:: We assume that there is no feedback loop in multiplier.
theorem :: GATE_5:4
for x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, q03, c01, c02, c03 being set holds
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 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 CLAADD1 (q02,c01,{}) is empty ) & ( not CLAADD1 (q02,c01,{}) is empty implies not z2 is empty ) & ( not z3 is empty implies not CLAADD2 (q03,c02,q02,c01,{}) is empty ) & ( not CLAADD2 (q03,c02,q02,c01,{}) is empty implies not z3 is empty ) & ( not z4 is empty implies not CLAADD3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) is empty ) & ( not CLAADD3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) is empty implies not z4 is empty ) & ( not z5 is empty implies not CLACARR3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) is empty ) & ( not CLACARR3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) 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 ) ) )
proof end;