begin
definition
let x0,
x1,
y0,
y1 be
set ;
func MULT210 x1,
y1,
x0,
y0 -> set equals
AND2 x0,
y0;
correctness
coherence
AND2 x0,y0 is set ;
;
func MULT211 x1,
y1,
x0,
y0 -> set equals
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
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
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
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 ) ) )
definition
let x0,
x1,
x2,
y0,
y1 be
set ;
func MULT310 x2,
x1,
y1,
x0,
y0 -> set equals
AND2 x0,
y0;
correctness
coherence
AND2 x0,y0 is set ;
;
func MULT311 x2,
x1,
y1,
x0,
y0 -> set equals
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
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
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
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
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
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
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
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
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 ) ) )
begin
theorem
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 ) ) )
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
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
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
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
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
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
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
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 ) ) )