:: 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 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;
func MULT211 (x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 2
 ADD1 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
func MULT212 (x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 3
 ADD2 ({} : ( ( ) ( empty ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
func MULT213 (x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 4
 CARR2 ({} : ( ( ) ( empty ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
end;

theorem :: GATE_5:1
for x0, x1, y0, y1, z0, z1, z2, z3, q00, q01, c01, q11, c11 being ( ( ) ( ) set ) holds
not ( ( not q00 : ( ( ) ( ) set ) is empty implies not AND2 (x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q00 : ( ( ) ( ) set ) is empty ) & ( not q01 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not q01 : ( ( ) ( ) set ) is empty ) & ( not c01 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not c01 : ( ( ) ( ) set ) is empty ) & ( not q11 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ,c01 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ,c01 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q11 : ( ( ) ( ) set ) is empty ) & ( not c11 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ,c01 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ,c01 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not c11 : ( ( ) ( ) set ) is empty ) & ( not z0 : ( ( ) ( ) set ) is empty implies not q00 : ( ( ) ( ) set ) is empty ) & ( not q00 : ( ( ) ( ) set ) is empty implies not z0 : ( ( ) ( ) set ) is empty ) & ( not z1 : ( ( ) ( ) set ) is empty implies not q01 : ( ( ) ( ) set ) is empty ) & ( not q01 : ( ( ) ( ) set ) is empty implies not z1 : ( ( ) ( ) set ) is empty ) & ( not z2 : ( ( ) ( ) set ) is empty implies not q11 : ( ( ) ( ) set ) is empty ) & ( not q11 : ( ( ) ( ) set ) is empty implies not z2 : ( ( ) ( ) set ) is empty ) & ( not z3 : ( ( ) ( ) set ) is empty implies not c11 : ( ( ) ( ) set ) is empty ) & ( not c11 : ( ( ) ( ) set ) is empty implies not z3 : ( ( ) ( ) set ) is empty ) & not ( ( not z0 : ( ( ) ( ) set ) is empty implies not MULT210 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT210 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z0 : ( ( ) ( ) set ) is empty ) & ( not z1 : ( ( ) ( ) set ) is empty implies not MULT211 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT211 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z1 : ( ( ) ( ) set ) is empty ) & ( not z2 : ( ( ) ( ) set ) is empty implies not MULT212 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT212 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z2 : ( ( ) ( ) set ) is empty ) & ( not z3 : ( ( ) ( ) set ) is empty implies not MULT213 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT213 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z3 : ( ( ) ( ) set ) is empty ) ) ) ;

definition
let x0, x1, x2, y0, y1 be ( ( ) ( ) set ) ;
func MULT310 (x2,x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 5
 AND2 (x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;
func MULT311 (x2,x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 6
 ADD1 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
func MULT312 (x2,x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 7
 ADD2 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
func MULT313 (x2,x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 8
 ADD3 ({} : ( ( ) ( empty ) set ) ,(AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
func MULT314 (x2,x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 9
 CARR3 ({} : ( ( ) ( empty ) set ) ,(AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
end;

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 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
func MULT322 (x2,y2,x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 11
 ADD2 ((MULT313 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(MULT312 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
func MULT323 (x2,y2,x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 12
 ADD3 ((MULT314 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(MULT313 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(MULT312 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
func MULT324 (x2,y2,x1,y1,x0,y0) -> ( ( ) ( ) set ) equals :: GATE_5:def 13
 CARR3 ((MULT314 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(MULT313 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(MULT312 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) ;
end;

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 : ( ( ) ( ) set ) is empty implies not AND2 (x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q00 : ( ( ) ( ) set ) is empty ) & ( not q01 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not q01 : ( ( ) ( ) set ) is empty ) & ( not c01 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not c01 : ( ( ) ( ) set ) is empty ) & ( not q02 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not q02 : ( ( ) ( ) set ) is empty ) & ( not c02 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not c02 : ( ( ) ( ) set ) is empty ) & ( not q11 : ( ( ) ( ) set ) is empty implies not XOR3 (q02 : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 (q02 : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q11 : ( ( ) ( ) set ) is empty ) & ( not c11 : ( ( ) ( ) set ) is empty implies not MAJ3 (q02 : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 (q02 : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not c11 : ( ( ) ( ) set ) is empty ) & ( not q12 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q12 : ( ( ) ( ) set ) is empty ) & ( not c12 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not c12 : ( ( ) ( ) set ) is empty ) & ( not q21 : ( ( ) ( ) set ) is empty implies not XOR3 (q12 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ,c11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 (q12 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ,c11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q21 : ( ( ) ( ) set ) is empty ) & ( not c21 : ( ( ) ( ) set ) is empty implies not MAJ3 (q12 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ,c11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 (q12 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ,c11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not c21 : ( ( ) ( ) set ) is empty ) & ( not q22 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c21 : ( ( ) ( ) set ) ,c12 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c21 : ( ( ) ( ) set ) ,c12 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q22 : ( ( ) ( ) set ) is empty ) & ( not c22 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c21 : ( ( ) ( ) set ) ,c12 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c21 : ( ( ) ( ) set ) ,c12 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not c22 : ( ( ) ( ) set ) is empty ) & ( not z0 : ( ( ) ( ) set ) is empty implies not q00 : ( ( ) ( ) set ) is empty ) & ( not q00 : ( ( ) ( ) set ) is empty implies not z0 : ( ( ) ( ) set ) is empty ) & ( not z1 : ( ( ) ( ) set ) is empty implies not q01 : ( ( ) ( ) set ) is empty ) & ( not q01 : ( ( ) ( ) set ) is empty implies not z1 : ( ( ) ( ) set ) is empty ) & ( not z2 : ( ( ) ( ) set ) is empty implies not q11 : ( ( ) ( ) set ) is empty ) & ( not q11 : ( ( ) ( ) set ) is empty implies not z2 : ( ( ) ( ) set ) is empty ) & ( not z3 : ( ( ) ( ) set ) is empty implies not q21 : ( ( ) ( ) set ) is empty ) & ( not q21 : ( ( ) ( ) set ) is empty implies not z3 : ( ( ) ( ) set ) is empty ) & ( not z4 : ( ( ) ( ) set ) is empty implies not q22 : ( ( ) ( ) set ) is empty ) & ( not q22 : ( ( ) ( ) set ) is empty implies not z4 : ( ( ) ( ) set ) is empty ) & ( not z5 : ( ( ) ( ) set ) is empty implies not c22 : ( ( ) ( ) set ) is empty ) & ( not c22 : ( ( ) ( ) set ) is empty implies not z5 : ( ( ) ( ) set ) is empty ) & not ( ( not z0 : ( ( ) ( ) set ) is empty implies not MULT310 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT310 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z0 : ( ( ) ( ) set ) is empty ) & ( not z1 : ( ( ) ( ) set ) is empty implies not MULT311 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT311 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z1 : ( ( ) ( ) set ) is empty ) & ( not z2 : ( ( ) ( ) set ) is empty implies not MULT321 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT321 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z2 : ( ( ) ( ) set ) is empty ) & ( not z3 : ( ( ) ( ) set ) is empty implies not MULT322 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT322 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z3 : ( ( ) ( ) set ) is empty ) & ( not z4 : ( ( ) ( ) set ) is empty implies not MULT323 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT323 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z4 : ( ( ) ( ) set ) is empty ) & ( not z5 : ( ( ) ( ) set ) is empty implies not MULT324 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT324 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z5 : ( ( ) ( ) set ) is empty ) ) ) ;

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 : ( ( ) ( ) set ) is empty implies not AND2 (x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q00 : ( ( ) ( ) set ) is empty ) & ( not q01 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not q01 : ( ( ) ( ) set ) is empty ) & ( not c01 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not c01 : ( ( ) ( ) set ) is empty ) & ( not q02 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q02 : ( ( ) ( ) set ) is empty ) & ( not c02 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not c02 : ( ( ) ( ) set ) is empty ) & ( not q03 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not q03 : ( ( ) ( ) set ) is empty ) & ( not c03 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not c03 : ( ( ) ( ) set ) is empty ) & ( not q11 : ( ( ) ( ) set ) is empty implies not XOR3 (q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 (q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not q11 : ( ( ) ( ) set ) is empty ) & ( not c11 : ( ( ) ( ) set ) is empty implies not MAJ3 (q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 (q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not c11 : ( ( ) ( ) set ) is empty ) & ( not q12 : ( ( ) ( ) set ) is empty implies not XOR3 (q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,c11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 (q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,c11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q12 : ( ( ) ( ) set ) is empty ) & ( not c12 : ( ( ) ( ) set ) is empty implies not MAJ3 (q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,c11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 (q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,c11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not c12 : ( ( ) ( ) set ) is empty ) & ( not q13 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c03 : ( ( ) ( ) set ) ,c12 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c03 : ( ( ) ( ) set ) ,c12 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q13 : ( ( ) ( ) set ) is empty ) & ( not c13 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c03 : ( ( ) ( ) set ) ,c12 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c03 : ( ( ) ( ) set ) ,c12 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not c13 : ( ( ) ( ) set ) is empty ) & ( not z0 : ( ( ) ( ) set ) is empty implies not q00 : ( ( ) ( ) set ) is empty ) & ( not q00 : ( ( ) ( ) set ) is empty implies not z0 : ( ( ) ( ) set ) is empty ) & ( not z1 : ( ( ) ( ) set ) is empty implies not q01 : ( ( ) ( ) set ) is empty ) & ( not q01 : ( ( ) ( ) set ) is empty implies not z1 : ( ( ) ( ) set ) is empty ) & ( not z2 : ( ( ) ( ) set ) is empty implies not q11 : ( ( ) ( ) set ) is empty ) & ( not q11 : ( ( ) ( ) set ) is empty implies not z2 : ( ( ) ( ) set ) is empty ) & ( not z3 : ( ( ) ( ) set ) is empty implies not q12 : ( ( ) ( ) set ) is empty ) & ( not q12 : ( ( ) ( ) set ) is empty implies not z3 : ( ( ) ( ) set ) is empty ) & ( not z4 : ( ( ) ( ) set ) is empty implies not q13 : ( ( ) ( ) set ) is empty ) & ( not q13 : ( ( ) ( ) set ) is empty implies not z4 : ( ( ) ( ) set ) is empty ) & ( not z5 : ( ( ) ( ) set ) is empty implies not c13 : ( ( ) ( ) set ) is empty ) & ( not c13 : ( ( ) ( ) set ) is empty implies not z5 : ( ( ) ( ) set ) is empty ) & not ( ( not z0 : ( ( ) ( ) set ) is empty implies not MULT310 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT310 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z0 : ( ( ) ( ) set ) is empty ) & ( not z1 : ( ( ) ( ) set ) is empty implies not MULT311 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT311 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z1 : ( ( ) ( ) set ) is empty ) & ( not z2 : ( ( ) ( ) set ) is empty implies not MULT321 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT321 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z2 : ( ( ) ( ) set ) is empty ) & ( not z3 : ( ( ) ( ) set ) is empty implies not MULT322 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT322 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z3 : ( ( ) ( ) set ) is empty ) & ( not z4 : ( ( ) ( ) set ) is empty implies not MULT323 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT323 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z4 : ( ( ) ( ) set ) is empty ) & ( not z5 : ( ( ) ( ) set ) is empty implies not MULT324 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT324 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z5 : ( ( ) ( ) set ) 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 ) ;
func CLAADD2 (a2,b2,a1,b1,c) -> ( ( ) ( ) set ) equals :: GATE_5:def 14
 XOR3 (a2 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ,(MAJ3 (a1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;
func CLACARR2 (a2,b2,a1,b1,c) -> ( ( ) ( ) set ) equals :: GATE_5:def 15
 OR2 ((AND2 (a2 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 ((OR2 (a2 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(MAJ3 (a1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;
end;

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 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) ,(CLACARR2 (a2 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ,a1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;
func CLACARR3 (a3,b3,a2,b2,a1,b1,c) -> ( ( ) ( ) set ) equals :: GATE_5:def 17
 OR3 ((AND2 (a3 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 ((OR2 (a3 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (a2 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND3 ((OR2 (a3 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(OR2 (a2 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(MAJ3 (a1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;
end;

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 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) ,(CLACARR3 (a3 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) ,a2 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ,a1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;
func CLACARR4 (a4,b4,a3,b3,a2,b2,a1,b1,c) -> ( ( ) ( ) set ) equals :: GATE_5:def 19
 OR4 ((AND2 (a4 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 ((OR2 (a4 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (a3 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND3 ((OR2 (a4 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(OR2 (a3 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (a2 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND4 ((OR2 (a4 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(OR2 (a3 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(OR2 (a2 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(MAJ3 (a1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;
end;

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 : ( ( ) ( ) set ) is empty implies not AND2 (x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q00 : ( ( ) ( ) set ) is empty ) & ( not q01 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not q01 : ( ( ) ( ) set ) is empty ) & ( not c01 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x1 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not c01 : ( ( ) ( ) set ) is empty ) & ( not q02 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not q02 : ( ( ) ( ) set ) is empty ) & ( not c02 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x0 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not c02 : ( ( ) ( ) set ) is empty ) & ( not q03 : ( ( ) ( ) set ) is empty implies not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not q03 : ( ( ) ( ) set ) is empty ) & ( not c03 : ( ( ) ( ) set ) is empty implies not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MAJ3 ((AND2 (x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not c03 : ( ( ) ( ) set ) is empty ) & ( not z0 : ( ( ) ( ) set ) is empty implies not q00 : ( ( ) ( ) set ) is empty ) & ( not q00 : ( ( ) ( ) set ) is empty implies not z0 : ( ( ) ( ) set ) is empty ) & ( not z1 : ( ( ) ( ) set ) is empty implies not q01 : ( ( ) ( ) set ) is empty ) & ( not q01 : ( ( ) ( ) set ) is empty implies not z1 : ( ( ) ( ) set ) is empty ) & ( not z2 : ( ( ) ( ) set ) is empty implies not CLAADD1 (q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not CLAADD1 (q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not z2 : ( ( ) ( ) set ) is empty ) & ( not z3 : ( ( ) ( ) set ) is empty implies not CLAADD2 (q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not CLAADD2 (q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not z3 : ( ( ) ( ) set ) is empty ) & ( not z4 : ( ( ) ( ) set ) is empty implies not CLAADD3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c03 : ( ( ) ( ) set ) ,q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not CLAADD3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c03 : ( ( ) ( ) set ) ,q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not z4 : ( ( ) ( ) set ) is empty ) & ( not z5 : ( ( ) ( ) set ) is empty implies not CLACARR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c03 : ( ( ) ( ) set ) ,q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not CLACARR3 ((AND2 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,c03 : ( ( ) ( ) set ) ,q03 : ( ( ) ( ) set ) ,c02 : ( ( ) ( ) set ) ,q02 : ( ( ) ( ) set ) ,c01 : ( ( ) ( ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) is empty implies not z5 : ( ( ) ( ) set ) is empty ) & not ( ( not z0 : ( ( ) ( ) set ) is empty implies not MULT310 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT310 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z0 : ( ( ) ( ) set ) is empty ) & ( not z1 : ( ( ) ( ) set ) is empty implies not MULT311 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT311 (x2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z1 : ( ( ) ( ) set ) is empty ) & ( not z2 : ( ( ) ( ) set ) is empty implies not MULT321 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT321 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z2 : ( ( ) ( ) set ) is empty ) & ( not z3 : ( ( ) ( ) set ) is empty implies not MULT322 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT322 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z3 : ( ( ) ( ) set ) is empty ) & ( not z4 : ( ( ) ( ) set ) is empty implies not MULT323 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT323 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z4 : ( ( ) ( ) set ) is empty ) & ( not z5 : ( ( ) ( ) set ) is empty implies not MULT324 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not MULT324 (x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,y0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not z5 : ( ( ) ( ) set ) is empty ) ) ) ;