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

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),{} ;

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;

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),{} ;

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),{} ;

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;

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;

definition

let a1, b1, a2, b2, c be set ;
canceled;
canceled;
func CLAADD2 a2,b2,a1,b1,c -> set equals :: GATE_5:def 16
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 17
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 GATE_5:def 14 :

canceled;

:: deftheorem GATE_5:def 15 :

canceled;

:: deftheorem defines CLAADD2 GATE_5:def 16 :

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

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

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 18
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 19
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 18 :

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

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

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 20
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 21
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 20 :

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

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

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;