gate_5.miz



    begin

    definition

      let x0,x1,y0,y1 be set;

      :: GATE_5:def1

      func MULT210 (x1,y1,x0,y0) -> set equals ( AND2 (x0,y0));

      correctness ;

      :: GATE_5:def2

      func MULT211 (x1,y1,x0,y0) -> set equals ( ADD1 (( AND2 (x1,y0)),( AND2 (x0,y1)), {} ));

      correctness ;

      :: GATE_5:def3

      func MULT212 (x1,y1,x0,y0) -> set equals ( ADD2 ( {} ,( AND2 (x1,y1)),( AND2 (x1,y0)),( AND2 (x0,y1)), {} ));

      correctness ;

      :: GATE_5:def4

      func MULT213 (x1,y1,x0,y0) -> set equals ( CARR2 ( {} ,( AND2 (x1,y1)),( AND2 (x1,y0)),( AND2 (x0,y1)), {} ));

      correctness ;

    end

    theorem :: GATE_5:1

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

    proof

      let x0,x1,y0,y1,z0,z1,z2,z3,q00,q01,c01,q11,c11 be set;

      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;

      thus not z0 is empty iff not ( MULT210 (x1,y1,x0,y0)) is empty by A1, A6;

      thus not z1 is empty iff not ( MULT211 (x1,y1,x0,y0)) is empty by A2, A7;

      set m212 = ( MULT212 (x1,y1,x0,y0));

      set x1y1 = ( AND2 (x1,y1));

      set x0y1 = ( AND2 (x0,y1));

      set x1y0 = ( AND2 (x1,y0));

      m212 = ( XOR3 ( {} ,x1y1,( MAJ3 (x1y0,x0y1, {} )))) by GATE_1:def 35;

      then not m212 is empty iff not x1y1 is empty & not not ( MAJ3 (x1y0,x0y1, {} )) is empty or not not x1y1 is empty & not ( MAJ3 (x1y0,x0y1, {} )) is empty;

      hence not z2 is empty iff not ( MULT212 (x1,y1,x0,y0)) is empty by A3, A4, A8;

      set m213 = ( MULT213 (x1,y1,x0,y0));

      m213 = ( MAJ3 ( {} ,x1y1,( MAJ3 (x1y0,x0y1, {} )))) by GATE_1:def 36;

      then not m213 is empty iff not x1y1 is empty & not ( MAJ3 (x1y0,x0y1, {} )) is empty;

      hence thesis by A3, A5, A9;

    end;

    definition

      let x0,x1,x2,y0,y1 be set;

      :: GATE_5:def5

      func MULT310 (x2,x1,y1,x0,y0) -> set equals ( AND2 (x0,y0));

      correctness ;

      :: GATE_5:def6

      func MULT311 (x2,x1,y1,x0,y0) -> set equals ( ADD1 (( AND2 (x1,y0)),( AND2 (x0,y1)), {} ));

      correctness ;

      :: GATE_5:def7

      func MULT312 (x2,x1,y1,x0,y0) -> set equals ( ADD2 (( AND2 (x2,y0)),( AND2 (x1,y1)),( AND2 (x1,y0)),( AND2 (x0,y1)), {} ));

      correctness ;

      :: GATE_5:def8

      func MULT313 (x2,x1,y1,x0,y0) -> set equals ( ADD3 ( {} ,( AND2 (x2,y1)),( AND2 (x2,y0)),( AND2 (x1,y1)),( AND2 (x1,y0)),( AND2 (x0,y1)), {} ));

      correctness ;

      :: GATE_5:def9

      func MULT314 (x2,x1,y1,x0,y0) -> set equals ( CARR3 ( {} ,( AND2 (x2,y1)),( AND2 (x2,y0)),( AND2 (x1,y1)),( AND2 (x1,y0)),( AND2 (x0,y1)), {} ));

      correctness ;

    end

    definition

      let x0,x1,x2,y0,y1,y2 be set;

      :: GATE_5:def10

      func MULT321 (x2,y2,x1,y1,x0,y0) -> set equals ( ADD1 (( MULT312 (x2,x1,y1,x0,y0)),( AND2 (x0,y2)), {} ));

      correctness ;

      :: GATE_5:def11

      func MULT322 (x2,y2,x1,y1,x0,y0) -> set equals ( ADD2 (( MULT313 (x2,x1,y1,x0,y0)),( AND2 (x1,y2)),( MULT312 (x2,x1,y1,x0,y0)),( AND2 (x0,y2)), {} ));

      correctness ;

      :: GATE_5:def12

      func MULT323 (x2,y2,x1,y1,x0,y0) -> set equals ( ADD3 (( MULT314 (x2,x1,y1,x0,y0)),( AND2 (x2,y2)),( MULT313 (x2,x1,y1,x0,y0)),( AND2 (x1,y2)),( MULT312 (x2,x1,y1,x0,y0)),( AND2 (x0,y2)), {} ));

      correctness ;

      :: GATE_5:def13

      func MULT324 (x2,y2,x1,y1,x0,y0) -> set equals ( CARR3 (( MULT314 (x2,x1,y1,x0,y0)),( AND2 (x2,y2)),( MULT313 (x2,x1,y1,x0,y0)),( AND2 (x1,y2)),( MULT312 (x2,x1,y1,x0,y0)),( AND2 (x0,y2)), {} ));

      correctness ;

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

      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) & ( not q02 is empty iff not ( XOR3 (( AND2 (x2,y0)),( AND2 (x1,y1)), {} )) 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;

      set x0y2 = ( AND2 (x0,y2));

      

       A19: not c11 is empty iff not q02 is empty & not x0y2 is empty or not x0y2 is empty & not c01 is empty or not c01 is empty & not q02 is empty by A6;

      thus not z0 is empty iff not ( MULT310 (x2,x1,y1,x0,y0)) is empty by A1, A13;

      thus not z1 is empty iff not ( MULT311 (x2,x1,y1,x0,y0)) is empty by A2, A14;

      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: m312 = ( XOR3 (x2y0,x1y1,( MAJ3 (x1y0,x0y1, {} )))) by GATE_1:def 35;

      then

       A21: not m312 is empty iff ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not not ( MAJ3 (x1y0,x0y1, {} )) is empty or not ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not ( MAJ3 (x1y0,x0y1, {} )) is empty;

      

       A22: not m312 is empty iff ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not ( not x1y0 is empty & not x0y1 is empty) or not ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not x1y0 is empty & not x0y1 is empty by A20;

       not q11 is empty iff ( not q02 is empty & not not x0y2 is empty or not not q02 is empty & not x0y2 is empty) & not not c01 is empty or not ( not q02 is empty & not not x0y2 is empty or not not q02 is empty & not x0y2 is empty) & not c01 is empty by A5;

      hence not z2 is empty iff not ( MULT321 (x2,y2,x1,y1,x0,y0)) is empty by A3, A15, A21;

      set x1y2 = ( AND2 (x1,y2));

      set x2y1 = ( AND2 (x2,y1));

      

       A23: not q12 is empty iff ( not x2y1 is empty & not not x1y2 is empty or not not x2y1 is empty & not x1y2 is empty) & not not c02 is empty or not ( not x2y1 is empty & not not x1y2 is empty or not not x2y1 is empty & not x1y2 is empty) & not c02 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: m314 = ( MAJ3 ( {} ,x2y1,( CARR2 (x2y0,x1y1,x1y0,x0y1, {} )))) by GATE_1:def 38

      .= ( MAJ3 ( {} ,x2y1,( MAJ3 (x2y0,x1y1,( MAJ3 (x1y0,x0y1, {} )))))) by GATE_1:def 36;

      set m322 = ( MULT322 (x2,y2,x1,y1,x0,y0));

      set m313 = ( MULT313 (x2,x1,y1,x0,y0));

      

       A25: m313 = ( XOR3 ( {} ,x2y1,( CARR2 (x2y0,x1y1,x1y0,x0y1, {} )))) by GATE_1:def 37

      .= ( XOR3 ( {} ,x2y1,( MAJ3 (x2y0,x1y1,( MAJ3 (x1y0,x0y1, {} )))))) by GATE_1:def 36;

      m322 = ( XOR3 (m313,x1y2,( MAJ3 (m312,x0y2, {} )))) 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;

      

       A26: m323 = ( XOR3 (m314,x2y2,( CARR2 (m313,x1y2,m312,x0y2, {} )))) by GATE_1:def 37

      .= ( XOR3 (m314,x2y2,( MAJ3 (m313,x1y2,( MAJ3 (m312,x0y2, {} )))))) by GATE_1:def 36;

       not q22 is empty iff ( not x2y2 is empty & not not c21 is empty or not not x2y2 is empty & not c21 is empty) & not not c12 is empty or not ( not x2y2 is empty & not not c21 is empty or not not x2y2 is empty & not c21 is empty) & not c12 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;

      

       A27: m324 = ( MAJ3 (m314,x2y2,( CARR2 (m313,x1y2,m312,x0y2, {} )))) by GATE_1:def 38

      .= ( MAJ3 (m314,x2y2,( MAJ3 (m313,x1y2,( MAJ3 (m312,x0y2, {} )))))) by GATE_1:def 36;

       not c22 is empty iff not x2y2 is empty & not c21 is empty or not c21 is empty & not c12 is empty or not c12 is empty & not x2y2 is empty by A12;

      hence thesis by A3, A4, A8, A10, A18, A19, A23, A22, A25, A24, A27;

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

      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;

      thus not z0 is empty iff not ( MULT310 (x2,x1,y1,x0,y0)) is empty by A1, A14;

      thus not z1 is empty iff not ( MULT311 (x2,x1,y1,x0,y0)) is empty by A2, A15;

      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: m312 = ( XOR3 (x2y0,x1y1,( MAJ3 (x1y0,x0y1, {} )))) 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 q03 is empty iff not x2y1 is empty & not not x1y2 is empty or not not x2y1 is empty & not x1y2 is empty by A6;

      

       A22: not q02 is empty iff ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not not x0y2 is empty or not ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not x0y2 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;

      

       A23: m313 = ( XOR3 ( {} ,x2y1,( CARR2 (x2y0,x1y1,x1y0,x0y1, {} )))) by GATE_1:def 37

      .= ( XOR3 ( {} ,x2y1,( MAJ3 (x2y0,x1y1,( MAJ3 (x1y0,x0y1, {} )))))) by GATE_1:def 36;

      m322 = ( XOR3 (m313,x1y2,( MAJ3 (m312,x0y2, {} )))) 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;

      

       A24: m314 = ( MAJ3 ( {} ,x2y1,( CARR2 (x2y0,x1y1,x1y0,x0y1, {} )))) by GATE_1:def 38

      .= ( MAJ3 ( {} ,x2y1,( MAJ3 (x2y0,x1y1,( MAJ3 (x1y0,x0y1, {} )))))) by GATE_1:def 36;

      set m324 = ( MULT324 (x2,y2,x1,y1,x0,y0));

      

       A25: m324 = ( MAJ3 (m314,x2y2,( CARR2 (m313,x1y2,m312,x0y2, {} )))) by GATE_1:def 38

      .= ( MAJ3 (m314,x2y2,( MAJ3 (m313,x1y2,( MAJ3 (m312,x0y2, {} )))))) by GATE_1:def 36;

      

       A26: m323 = ( XOR3 (m314,x2y2,( CARR2 (m313,x1y2,m312,x0y2, {} )))) by GATE_1:def 37

      .= ( XOR3 (m314,x2y2,( MAJ3 (m313,x1y2,( MAJ3 (m312,x0y2, {} )))))) by GATE_1:def 36;

       not q13 is empty iff ( not x2y2 is empty & not not c03 is empty or not not x2y2 is empty & not c03 is empty) & not not c12 is empty or not ( not x2y2 is empty & not not c03 is empty or not not x2y2 is empty & not c03 is empty) & not c12 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;

       not c13 is empty iff not x2y2 is empty & not c03 is empty or not c03 is empty & not c12 is empty or not c12 is empty & not x2y2 is empty by A13;

      hence thesis by A3, A5, A7, A9, A11, A19, A22, A21, A20, A23, A24, A25;

    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;

      :: GATE_5:def14

      func CLAADD2 (a2,b2,a1,b1,c) -> set equals ( XOR3 (a2,b2,( MAJ3 (a1,b1,c))));

      correctness ;

      :: GATE_5:def15

      func CLACARR2 (a2,b2,a1,b1,c) -> set equals ( OR2 (( AND2 (a2,b2)),( AND2 (( OR2 (a2,b2)),( MAJ3 (a1,b1,c))))));

      correctness ;

    end

    definition

      let a1,b1,a2,b2,a3,b3,c be set;

      :: GATE_5:def16

      func CLAADD3 (a3,b3,a2,b2,a1,b1,c) -> set equals ( XOR3 (a3,b3,( CLACARR2 (a2,b2,a1,b1,c))));

      correctness ;

      :: GATE_5:def17

      func CLACARR3 (a3,b3,a2,b2,a1,b1,c) -> set equals ( OR3 (( AND2 (a3,b3)),( AND2 (( OR2 (a3,b3)),( AND2 (a2,b2)))),( AND3 (( OR2 (a3,b3)),( OR2 (a2,b2)),( MAJ3 (a1,b1,c))))));

      correctness ;

    end

    definition

      let a1,b1,a2,b2,a3,b3,a4,b4,c be set;

      :: GATE_5:def18

      func CLAADD4 (a4,b4,a3,b3,a2,b2,a1,b1,c) -> set equals ( XOR3 (a4,b4,( CLACARR3 (a3,b3,a2,b2,a1,b1,c))));

      correctness ;

      :: GATE_5:def19

      func CLACARR4 (a4,b4,a3,b3,a2,b2,a1,b1,c) -> set equals ( OR4 (( AND2 (a4,b4)),( AND2 (( OR2 (a4,b4)),( AND2 (a3,b3)))),( AND3 (( OR2 (a4,b4)),( OR2 (a3,b3)),( AND2 (a2,b2)))),( AND4 (( OR2 (a4,b4)),( OR2 (a3,b3)),( OR2 (a2,b2)),( MAJ3 (a1,b1,c))))));

      correctness ;

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

      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;

      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;

      thus not z1 is empty iff not ( MULT311 (x2,x1,y1,x0,y0)) is empty by A2, A9;

      set m312 = ( MULT312 (x2,x1,y1,x0,y0));

      set x0y1 = ( AND2 (x0,y1));

      set x1y0 = ( AND2 (x1,y0));

      

       A14: m312 = ( XOR3 (x2y0,x1y1,( MAJ3 (x1y0,x0y1, {} )))) by GATE_1:def 35;

      then

       A15: not m312 is empty iff ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not ( not x1y0 is empty & not x0y1 is empty) or not ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not x1y0 is empty & not x0y1 is empty;

      set x1y2 = ( AND2 (x1,y2));

      set x2y1 = ( AND2 (x2,y1));

      

       A16: not q03 is empty iff not x2y1 is empty & not not x1y2 is empty or not not x2y1 is empty & not x1y2 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: m314 = ( MAJ3 ( {} ,x2y1,( CARR2 (x2y0,x1y1,x1y0,x0y1, {} )))) by GATE_1:def 38

      .= ( MAJ3 ( {} ,x2y1,( MAJ3 (x2y0,x1y1,( MAJ3 (x1y0,x0y1, {} )))))) by GATE_1:def 36;

      set m322 = ( MULT322 (x2,y2,x1,y1,x0,y0));

      set m313 = ( MULT313 (x2,x1,y1,x0,y0));

      

       A18: m313 = ( XOR3 ( {} ,x2y1,( CARR2 (x2y0,x1y1,x1y0,x0y1, {} )))) by GATE_1:def 37

      .= ( XOR3 ( {} ,x2y1,( MAJ3 (x2y0,x1y1,( MAJ3 (x1y0,x0y1, {} )))))) by GATE_1:def 36;

       not q02 is empty iff ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not not x0y2 is empty or not ( not x2y0 is empty & not not x1y1 is empty or not not x2y0 is empty & not x1y1 is empty) & not x0y2 is empty by A4;

      hence not z2 is empty iff not ( MULT321 (x2,y2,x1,y1,x0,y0)) is empty by A3, A10, A14;

      

       A19: not c02 is empty iff not x2y0 is empty & not x1y1 is empty or not x1y1 is empty & not x0y2 is empty or not x0y2 is empty & not x2y0 is empty by A5;

      m322 = ( XOR3 (m313,x1y2,( MAJ3 (m312,x0y2, {} )))) by GATE_1:def 35;

      then not m322 is empty iff ( not m313 is empty & not not x1y2 is empty or not not m313 is empty & not x1y2 is empty) & not ( not m312 is empty & not x0y2 is empty) or not ( not m313 is empty & not not x1y2 is empty or not not m313 is empty & not x1y2 is empty) & not m312 is empty & not x0y2 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;

      m323 = ( XOR3 (m314,x2y2,( CARR2 (m313,x1y2,m312,x0y2, {} )))) by GATE_1:def 37

      .= ( XOR3 (m314,x2y2,( MAJ3 (m313,x1y2,( MAJ3 (m312,x0y2, {} )))))) by GATE_1:def 36;

      then not m323 is empty iff ( not m314 is empty & not not x2y2 is empty or not not m314 is empty & not x2y2 is empty) & not ( not m313 is empty & not x1y2 is empty or not x1y2 is empty & not m312 is empty & not x0y2 is empty or not m312 is empty & not x0y2 is empty & not m313 is empty) or not ( not m314 is empty & not not x2y2 is empty or not not m314 is empty & not x2y2 is empty) & ( not m313 is empty & not x1y2 is empty or not x1y2 is empty & not m312 is empty & not x0y2 is empty or not m312 is empty & not x0y2 is empty & not m313 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;

      m324 = ( MAJ3 (m314,x2y2,( CARR2 (m313,x1y2,m312,x0y2, {} )))) by GATE_1:def 38

      .= ( MAJ3 (m314,x2y2,( MAJ3 (m313,x1y2,( MAJ3 (m312,x0y2, {} )))))) by GATE_1:def 36;

      then not m324 is empty iff not m314 is empty & not x2y2 is empty or not x2y2 is empty & ( not m313 is empty & not x1y2 is empty or not x1y2 is empty & not m312 is empty & not x0y2 is empty or not m312 is empty & not x0y2 is empty & not m313 is empty) or ( not m313 is empty & not x1y2 is empty or not x1y2 is empty & not m312 is empty & not x0y2 is empty or not m312 is empty & not x0y2 is empty & not m313 is empty) & not m314 is empty;

      hence thesis by A3, A4, A7, A13, A19, A16, A15, A18, A17;

    end;