:: GATE_5 semantic presentation

begin

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
let x0, x1, y0, y1, z0, z1, z2, z3, q00, q01, c01, q11, c11 be set ; ::_thesis: 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 ) ) )
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 q11 is empty iff not XOR3 ((AND2 (x1,y1)),{},c01) is empty ) and
A5: ( not c11 is empty iff not MAJ3 ((AND2 (x1,y1)),{},c01) is empty ) and
A6: ( not z0 is empty iff not q00 is empty ) and
A7: ( not z1 is empty iff not q01 is empty ) and
A8: ( not z2 is empty iff not q11 is empty ) and
A9: ( not z3 is empty iff not c11 is empty ) ; ::_thesis: ( ( 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 ) )
thus  ( not z0 is empty iff not MULT210 (x1,y1,x0,y0) is empty ) by A1, A6; ::_thesis: ( ( 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 ) )
thus  ( not z1 is empty iff not MULT211 (x1,y1,x0,y0) is empty ) by A2, A7; ::_thesis: ( ( 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 ) )
set m212 = MULT212 (x1,y1,x0,y0);
set x1y1 = AND2 (x1,y1);
set x0y1 = AND2 (x0,y1);
set x1y0 = AND2 (x1,y0);
 MULT212 (x1,y1,x0,y0) = XOR3 ({},(AND2 (x1,y1)),(MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}))) by GATE_1:def_35;
then  ( ( ( not AND2 (x1,y1) is empty & MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) or ( AND2 (x1,y1) is empty & not MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) ) iff not MULT212 (x1,y1,x0,y0) is empty ) ;
hence  ( not z2 is empty iff not MULT212 (x1,y1,x0,y0) is empty ) by A3, A4, A8; ::_thesis: ( not z3 is empty iff not MULT213 (x1,y1,x0,y0) is empty )
set m213 = MULT213 (x1,y1,x0,y0);
 MULT213 (x1,y1,x0,y0) = MAJ3 ({},(AND2 (x1,y1)),(MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}))) by GATE_1:def_36;
then  ( not MULT213 (x1,y1,x0,y0) is empty iff ( not AND2 (x1,y1) is empty & not MAJ3 ((AND2 (x1,y0)),(AND2 (x0,y1)),{}) is empty ) ) ;
hence  ( not z3 is empty iff not MULT213 (x1,y1,x0,y0) is empty ) by A3, A5, A9; ::_thesis: verum
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
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 ; ::_thesis: 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 ) ; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( 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; ::_thesis: verum
end;

begin

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
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 ; ::_thesis: 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 ) ; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( ( 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; ::_thesis: ( 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; ::_thesis: verum
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 ;
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)))));

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

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

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
let x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, q03, c01, c02, c03 be set ; ::_thesis: 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 ) ) )
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 z0 is empty iff not q00 is empty ) and
A9: ( not z1 is empty iff not q01 is empty ) and
A10: ( not z2 is empty iff not CLAADD1 (q02,c01,{}) is empty ) and
A11: ( not z3 is empty iff not CLAADD2 (q03,c02,q02,c01,{}) is empty ) and
A12: ( not z4 is empty iff not CLAADD3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) is empty ) and
A13: ( not z5 is empty iff not CLACARR3 ((AND2 (x2,y2)),c03,q03,c02,q02,c01,{}) is empty ) ; ::_thesis: ( ( 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);
set x1y1 = AND2 (x1,y1);
set x2y0 = AND2 (x2,y0);
thus  ( not z0 is empty iff not MULT310 (x2,x1,y1,x0,y0) is empty ) by A1, A8; ::_thesis: ( ( 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, A9; ::_thesis: ( ( 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 x0y1 = AND2 (x0,y1);
set x1y0 = AND2 (x1,y0);
A14: 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 A15: ( ( ( ( ( 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 ) ;
set x1y2 = AND2 (x1,y2);
set x2y1 = AND2 (x2,y1);
A16: ( ( ( 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;
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);
A17: 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);
A18: 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 ;
 ( ( ( ( ( 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, A10, A14; ::_thesis: ( ( 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 ) )
A19: ( ( ( not AND2 (x2,y0) is empty & not AND2 (x1,y1) is empty ) or ( not AND2 (x1,y1) is empty & not AND2 (x0,y2) is empty ) or ( not AND2 (x0,y2) is empty & not AND2 (x2,y0) is empty ) ) iff not c02 is empty ) by A5;
 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;
then  ( ( ( ( ( not MULT313 (x2,x1,y1,x0,y0) is empty & AND2 (x1,y2) is empty ) or ( MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) ) & ( MULT312 (x2,x1,y1,x0,y0) is empty or AND2 (x0,y2) is empty ) ) or ( not ( not MULT313 (x2,x1,y1,x0,y0) is empty & AND2 (x1,y2) is empty ) & not ( MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) ) iff not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) ;
hence  ( not z3 is empty iff not MULT322 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A4, A11, A19, A16, A15, A18; ::_thesis: ( ( 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 ) )
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 ;
then  ( ( ( ( ( not MULT314 (x2,x1,y1,x0,y0) is empty & AND2 (x2,y2) is empty ) or ( MULT314 (x2,x1,y1,x0,y0) is empty & not AND2 (x2,y2) is empty ) ) & not ( not MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) & not ( not AND2 (x1,y2) is empty & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) & not ( not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty & not MULT313 (x2,x1,y1,x0,y0) is empty ) ) or ( not ( not MULT314 (x2,x1,y1,x0,y0) is empty & AND2 (x2,y2) is empty ) & not ( MULT314 (x2,x1,y1,x0,y0) is empty & not AND2 (x2,y2) is empty ) & ( ( not MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) or ( not AND2 (x1,y2) is empty & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) or ( not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty & not MULT313 (x2,x1,y1,x0,y0) is empty ) ) ) ) iff not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) ;
hence  ( not z4 is empty iff not MULT323 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A4, A7, A12, A19, A16, A15, A18, A17; ::_thesis: ( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty )
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 ;
then  ( ( ( not MULT314 (x2,x1,y1,x0,y0) is empty & not AND2 (x2,y2) is empty ) or ( not AND2 (x2,y2) is empty & ( ( not MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) or ( not AND2 (x1,y2) is empty & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) or ( not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty & not MULT313 (x2,x1,y1,x0,y0) is empty ) ) ) or ( ( ( not MULT313 (x2,x1,y1,x0,y0) is empty & not AND2 (x1,y2) is empty ) or ( not AND2 (x1,y2) is empty & not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty ) or ( not MULT312 (x2,x1,y1,x0,y0) is empty & not AND2 (x0,y2) is empty & not MULT313 (x2,x1,y1,x0,y0) is empty ) ) & not MULT314 (x2,x1,y1,x0,y0) is empty ) ) iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) ;
hence  ( not z5 is empty iff not MULT324 (x2,y2,x1,y1,x0,y0) is empty ) by A3, A4, A7, A13, A19, A16, A15, A18, A17; ::_thesis: verum
end;