gate_1.miz



    begin

    definition

      let a be set;

      :: GATE_1:def1

      func NOT1 a -> set equals

      : Def1: {} if a is non empty

      otherwise { {} };

      correctness ;

    end

    registration

      let a be empty set;

      cluster ( NOT1 a) -> non empty;

      coherence by Def1;

    end

    registration

      let a be non empty set;

      cluster ( NOT1 a) -> empty;

      coherence by Def1;

    end

    theorem :: GATE_1:1

    ( NOT1 { {} }) = {} & ( NOT1 {} ) = { {} } by Def1;

    theorem :: GATE_1:2

    for a be set holds ( NOT1 a) is non empty iff not a is non empty;

    reserve a,b,c,d,e,f,g,h for set;

    theorem :: GATE_1:3

    ( NOT1 {} ) is non empty;

    definition

      let a,b be set;

      :: GATE_1:def2

      func AND2 (a,b) -> set equals

      : Def2: ( NOT1 {} ) if a is non empty & b is non empty

      otherwise {} ;

      correctness ;

      commutativity ;

    end

    registration

      let a,b be non empty set;

      cluster ( AND2 (a,b)) -> non empty;

      coherence by Def2;

    end

    registration

      let a be empty set, b be set;

      cluster ( AND2 (a,b)) -> empty;

      coherence by Def2;

    end

    theorem :: GATE_1:4

    ( AND2 (a,b)) is non empty iff a is non empty & b is non empty;

    definition

      let a,b be set;

      :: GATE_1:def3

      func OR2 (a,b) -> set equals

      : Def3: ( NOT1 {} ) if a is non empty or b is non empty

      otherwise {} ;

      correctness ;

      commutativity ;

    end

    registration

      let a be set, b be non empty set;

      cluster ( OR2 (a,b)) -> non empty;

      coherence by Def3;

    end

    registration

      let a,b be empty set;

      cluster ( OR2 (a,b)) -> empty;

      coherence by Def3;

    end

    theorem :: GATE_1:5

    ( OR2 (a,b)) is non empty iff (a is non empty or b is non empty);

    definition

      let a,b be set;

      :: GATE_1:def4

      func XOR2 (a,b) -> set equals

      : Def4: ( NOT1 {} ) if a is non empty & not b is non empty or not a is non empty & b is non empty

      otherwise {} ;

      correctness ;

      commutativity ;

    end

    registration

      let a be empty set, b be non empty set;

      cluster ( XOR2 (a,b)) -> non empty;

      coherence by Def4;

    end

    registration

      let a,b be empty set;

      cluster ( XOR2 (a,b)) -> empty;

      coherence by Def4;

    end

    registration

      let a,b be non empty set;

      cluster ( XOR2 (a,b)) -> empty;

      coherence by Def4;

    end

    theorem :: GATE_1:6

    ( XOR2 (a,b)) is non empty iff a is non empty & not b is non empty or not a is non empty & b is non empty;

    theorem :: GATE_1:7

     not ( XOR2 (a,a)) is non empty

    proof

      ( XOR2 (a,a)) is non empty iff a is non empty & not a is non empty or not a is non empty & a is non empty;

      hence thesis;

    end;

    theorem :: GATE_1:8

    ( XOR2 (a, {} )) is non empty iff a is non empty;

    theorem :: GATE_1:9

    ( XOR2 (a,b)) is non empty iff ( XOR2 (b,a)) is non empty;

    definition

      let a,b be set;

      :: GATE_1:def5

      func EQV2 (a,b) -> set equals

      : Def5: ( NOT1 {} ) if a is non empty iff b is non empty

      otherwise {} ;

      correctness ;

      commutativity ;

    end

    registration

      let a be empty set, b be non empty set;

      cluster ( EQV2 (a,b)) -> empty;

      coherence by Def5;

    end

    registration

      let a,b be empty set;

      cluster ( EQV2 (a,b)) -> non empty;

      coherence by Def5;

    end

    registration

      let a,b be non empty set;

      cluster ( EQV2 (a,b)) -> non empty;

      coherence by Def5;

    end

    theorem :: GATE_1:10

    ( EQV2 (a,b)) is non empty iff (a is non empty iff b is non empty);

    theorem :: GATE_1:11

    ( EQV2 (a,b)) is non empty iff not ( XOR2 (a,b)) is non empty

    proof

      ( EQV2 (a,b)) is non empty iff (a is non empty iff b is non empty);

      hence thesis;

    end;

    definition

      let a,b be set;

      :: GATE_1:def6

      func NAND2 (a,b) -> set equals

      : Def6: ( NOT1 {} ) if not (a is non empty & b is non empty)

      otherwise {} ;

      correctness ;

      commutativity ;

    end

    registration

      let a be empty set, b be set;

      cluster ( NAND2 (a,b)) -> non empty;

      coherence by Def6;

    end

    registration

      let a,b be non empty set;

      cluster ( NAND2 (a,b)) -> empty;

      coherence by Def6;

    end

    theorem :: GATE_1:12

    ( NAND2 (a,b)) is non empty iff not (a is non empty & b is non empty);

    definition

      let a,b be set;

      :: GATE_1:def7

      func NOR2 (a,b) -> set equals

      : Def7: ( NOT1 {} ) if not (a is non empty or b is non empty)

      otherwise {} ;

      correctness ;

      commutativity ;

    end

    registration

      let a,b be empty set;

      cluster ( NOR2 (a,b)) -> non empty;

      coherence by Def7;

    end

    registration

      let a be non empty set, b be set;

      cluster ( NOR2 (a,b)) -> empty;

      coherence by Def7;

    end

    theorem :: GATE_1:13

    ( NOR2 (a,b)) is non empty iff not (a is non empty or b is non empty);

    definition

      let a,b,c be set;

      :: GATE_1:def8

      func AND3 (a,b,c) -> set equals

      : Def8: ( NOT1 {} ) if a is non empty & b is non empty & c is non empty

      otherwise {} ;

      correctness ;

    end

    registration

      let a,b,c be non empty set;

      cluster ( AND3 (a,b,c)) -> non empty;

      coherence by Def8;

    end

    registration

      let a be empty set, b,c be set;

      cluster ( AND3 (a,b,c)) -> empty;

      coherence by Def8;

      cluster ( AND3 (b,a,c)) -> empty;

      coherence by Def8;

      cluster ( AND3 (b,c,a)) -> empty;

      coherence by Def8;

    end

    theorem :: GATE_1:14

    ( AND3 (a,b,c)) is non empty iff a is non empty & b is non empty & c is non empty;

    definition

      let a,b,c be set;

      :: GATE_1:def9

      func OR3 (a,b,c) -> set equals

      : Def9: ( NOT1 {} ) if a is non empty or b is non empty or c is non empty

      otherwise {} ;

      correctness ;

    end

    registration

      let a,b,c be empty set;

      cluster ( OR3 (a,b,c)) -> empty;

      coherence by Def9;

    end

    registration

      let a be non empty set, b,c be set;

      cluster ( OR3 (a,b,c)) -> non empty;

      coherence by Def9;

      cluster ( OR3 (b,a,c)) -> non empty;

      coherence by Def9;

      cluster ( OR3 (b,c,a)) -> non empty;

      coherence by Def9;

    end

    theorem :: GATE_1:15

    ( OR3 (a,b,c)) is non empty iff a is non empty or b is non empty or c is non empty;

    definition

      let a,b,c be set;

      :: GATE_1:def10

      func XOR3 (a,b,c) -> set equals

      : Def10: ( NOT1 {} ) if (a is non empty & not b is non empty or not a is non empty & b is non empty) & not c is non empty or not (a is non empty & not b is non empty or not a is non empty & b is non empty) & c is non empty

      otherwise {} ;

      correctness ;

    end

    registration

      let a,b,c be empty set;

      cluster ( XOR3 (a,b,c)) -> empty;

      coherence by Def10;

    end

    registration

      let a,b be empty set, c be non empty set;

      cluster ( XOR3 (a,b,c)) -> non empty;

      coherence by Def10;

      cluster ( XOR3 (a,c,b)) -> non empty;

      coherence by Def10;

      cluster ( XOR3 (c,a,b)) -> non empty;

      coherence by Def10;

    end

    registration

      let a,b be non empty set, c be empty set;

      cluster ( XOR3 (a,b,c)) -> empty;

      coherence by Def10;

      cluster ( XOR3 (a,c,b)) -> empty;

      coherence by Def10;

      cluster ( XOR3 (c,a,b)) -> empty;

      coherence by Def10;

    end

    registration

      let a,b,c be non empty set;

      cluster ( XOR3 (a,b,c)) -> non empty;

      coherence by Def10;

    end

    theorem :: GATE_1:16

    ( XOR3 (a,b,c)) is non empty iff (a is non empty & not b is non empty or not a is non empty & b is non empty) & not c is non empty or not (a is non empty & not b is non empty or not a is non empty & b is non empty) & c is non empty;

    definition

      let a,b,c be set;

      :: GATE_1:def11

      func MAJ3 (a,b,c) -> set equals

      : Def11: ( NOT1 {} ) if a is non empty & b is non empty or b is non empty & c is non empty or c is non empty & a is non empty

      otherwise {} ;

      correctness ;

    end

    registration

      let a,b be non empty set, c be set;

      cluster ( MAJ3 (a,b,c)) -> non empty;

      coherence by Def11;

      cluster ( MAJ3 (a,c,b)) -> non empty;

      coherence by Def11;

      cluster ( MAJ3 (c,a,b)) -> non empty;

      coherence by Def11;

    end

    registration

      let a,b be empty set, c be set;

      cluster ( MAJ3 (a,b,c)) -> empty;

      coherence by Def11;

      cluster ( MAJ3 (a,c,b)) -> empty;

      coherence by Def11;

      cluster ( MAJ3 (c,a,b)) -> empty;

      coherence by Def11;

    end

    theorem :: GATE_1:17

    ( MAJ3 (a,b,c)) is non empty iff a is non empty & b is non empty or b is non empty & c is non empty or c is non empty & a is non empty;

    definition

      let a,b,c be set;

      :: GATE_1:def12

      func NAND3 (a,b,c) -> set equals

      : Def12: ( NOT1 {} ) if not (a is non empty & b is non empty & c is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:18

    ( NAND3 (a,b,c)) is non empty iff not (a is non empty & b is non empty & c is non empty) by Def12;

    definition

      let a,b,c be set;

      :: GATE_1:def13

      func NOR3 (a,b,c) -> set equals

      : Def13: ( NOT1 {} ) if not (a is non empty or b is non empty or c is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:19

    ( NOR3 (a,b,c)) is non empty iff not (a is non empty or b is non empty or c is non empty) by Def13;

    definition

      let a,b,c,d be set;

      :: GATE_1:def14

      func AND4 (a,b,c,d) -> set equals

      : Def14: ( NOT1 {} ) if a is non empty & b is non empty & c is non empty & d is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:20

    ( AND4 (a,b,c,d)) is non empty iff a is non empty & b is non empty & c is non empty & d is non empty by Def14;

    definition

      let a,b,c,d be set;

      :: GATE_1:def15

      func OR4 (a,b,c,d) -> set equals

      : Def15: ( NOT1 {} ) if a is non empty or b is non empty or c is non empty or d is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:21

    ( OR4 (a,b,c,d)) is non empty iff a is non empty or b is non empty or c is non empty or d is non empty by Def15;

    definition

      let a,b,c,d be set;

      :: GATE_1:def16

      func NAND4 (a,b,c,d) -> set equals

      : Def16: ( NOT1 {} ) if not (a is non empty & b is non empty & c is non empty & d is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:22

    ( NAND4 (a,b,c,d)) is non empty iff not (a is non empty & b is non empty & c is non empty & d is non empty) by Def16;

    definition

      let a,b,c,d be set;

      :: GATE_1:def17

      func NOR4 (a,b,c,d) -> set equals

      : Def17: ( NOT1 {} ) if not (a is non empty or b is non empty or c is non empty or d is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:23

    ( NOR4 (a,b,c,d)) is non empty iff not (a is non empty or b is non empty or c is non empty or d is non empty) by Def17;

    definition

      let a,b,c,d,e be set;

      :: GATE_1:def18

      func AND5 (a,b,c,d,e) -> set equals

      : Def18: ( NOT1 {} ) if a is non empty & b is non empty & c is non empty & d is non empty & e is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:24

    ( AND5 (a,b,c,d,e)) is non empty iff a is non empty & b is non empty & c is non empty & d is non empty & e is non empty by Def18;

    definition

      let a,b,c,d,e be set;

      :: GATE_1:def19

      func OR5 (a,b,c,d,e) -> set equals

      : Def19: ( NOT1 {} ) if a is non empty or b is non empty or c is non empty or d is non empty or e is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:25

    ( OR5 (a,b,c,d,e)) is non empty iff a is non empty or b is non empty or c is non empty or d is non empty or e is non empty by Def19;

    definition

      let a,b,c,d,e be set;

      :: GATE_1:def20

      func NAND5 (a,b,c,d,e) -> set equals

      : Def20: ( NOT1 {} ) if not (a is non empty & b is non empty & c is non empty & d is non empty & e is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:26

    ( NAND5 (a,b,c,d,e)) is non empty iff not (a is non empty & b is non empty & c is non empty & d is non empty & e is non empty) by Def20;

    definition

      let a,b,c,d,e be set;

      :: GATE_1:def21

      func NOR5 (a,b,c,d,e) -> set equals

      : Def21: ( NOT1 {} ) if not (a is non empty or b is non empty or c is non empty or d is non empty or e is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:27

    ( NOR5 (a,b,c,d,e)) is non empty iff not (a is non empty or b is non empty or c is non empty or d is non empty or e is non empty) by Def21;

    definition

      let a,b,c,d,e,f be set;

      :: GATE_1:def22

      func AND6 (a,b,c,d,e,f) -> set equals

      : Def22: ( NOT1 {} ) if a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:28

    ( AND6 (a,b,c,d,e,f)) is non empty iff a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty by Def22;

    definition

      let a,b,c,d,e,f be set;

      :: GATE_1:def23

      func OR6 (a,b,c,d,e,f) -> set equals

      : Def23: ( NOT1 {} ) if a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:29

    ( OR6 (a,b,c,d,e,f)) is non empty iff a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty by Def23;

    definition

      let a,b,c,d,e,f be set;

      :: GATE_1:def24

      func NAND6 (a,b,c,d,e,f) -> set equals

      : Def24: ( NOT1 {} ) if not (a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:30

    ( NAND6 (a,b,c,d,e,f)) is non empty iff not (a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty) by Def24;

    definition

      let a,b,c,d,e,f be set;

      :: GATE_1:def25

      func NOR6 (a,b,c,d,e,f) -> set equals

      : Def25: ( NOT1 {} ) if not (a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:31

    ( NOR6 (a,b,c,d,e,f)) is non empty iff not (a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty) by Def25;

    definition

      let a,b,c,d,e,f,g be set;

      :: GATE_1:def26

      func AND7 (a,b,c,d,e,f,g) -> set equals

      : Def26: ( NOT1 {} ) if a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty & g is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:32

    ( AND7 (a,b,c,d,e,f,g)) is non empty iff a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty & g is non empty by Def26;

    definition

      let a,b,c,d,e,f,g be set;

      :: GATE_1:def27

      func OR7 (a,b,c,d,e,f,g) -> set equals

      : Def27: ( NOT1 {} ) if a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty or g is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:33

    ( OR7 (a,b,c,d,e,f,g)) is non empty iff a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty or g is non empty by Def27;

    definition

      let a,b,c,d,e,f,g be set;

      :: GATE_1:def28

      func NAND7 (a,b,c,d,e,f,g) -> set equals

      : Def28: ( NOT1 {} ) if not (a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty & g is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:34

    ( NAND7 (a,b,c,d,e,f,g)) is non empty iff not (a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty & g is non empty) by Def28;

    definition

      let a,b,c,d,e,f,g be set;

      :: GATE_1:def29

      func NOR7 (a,b,c,d,e,f,g) -> set equals

      : Def29: ( NOT1 {} ) if not (a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty or g is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:35

    ( NOR7 (a,b,c,d,e,f,g)) is non empty iff not (a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty or g is non empty) by Def29;

    definition

      let a,b,c,d,e,f,g,h be set;

      :: GATE_1:def30

      func AND8 (a,b,c,d,e,f,g,h) -> set equals

      : Def30: ( NOT1 {} ) if a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty & g is non empty & h is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:36

    ( AND8 (a,b,c,d,e,f,g,h)) is non empty iff a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty & g is non empty & h is non empty by Def30;

    definition

      let a,b,c,d,e,f,g,h be set;

      :: GATE_1:def31

      func OR8 (a,b,c,d,e,f,g,h) -> set equals

      : Def31: ( NOT1 {} ) if a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty or g is non empty or h is non empty

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:37

    ( OR8 (a,b,c,d,e,f,g,h)) is non empty iff a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty or g is non empty or h is non empty by Def31;

    definition

      let a,b,c,d,e,f,g,h be set;

      :: GATE_1:def32

      func NAND8 (a,b,c,d,e,f,g,h) -> set equals

      : Def32: ( NOT1 {} ) if not (a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty & g is non empty & h is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:38

    ( NAND8 (a,b,c,d,e,f,g,h)) is non empty iff not (a is non empty & b is non empty & c is non empty & d is non empty & e is non empty & f is non empty & g is non empty & h is non empty) by Def32;

    definition

      let a,b,c,d,e,f,g,h be set;

      :: GATE_1:def33

      func NOR8 (a,b,c,d,e,f,g,h) -> set equals

      : Def33: ( NOT1 {} ) if not (a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty or g is non empty or h is non empty)

      otherwise {} ;

      correctness ;

    end

    theorem :: GATE_1:39

    ( NOR8 (a,b,c,d,e,f,g,h)) is non empty iff not (a is non empty or b is non empty or c is non empty or d is non empty or e is non empty or f is non empty or g is non empty or h is non empty) by Def33;

    begin

    theorem :: GATE_1:40

    for c1,x1,x2,x3,x4,y1,y2,y3,y4,c2,c3,c4,c5,n1,n2,n3,n4,n,c5b be set holds (( MAJ3 (x1,y1,c1)) is non empty implies c2 is non empty) & (( MAJ3 (x2,y2,c2)) is non empty implies c3 is non empty) & (( MAJ3 (x3,y3,c3)) is non empty implies c4 is non empty) & (( MAJ3 (x4,y4,c4)) is non empty implies c5 is non empty) & (n1 is non empty implies ( OR2 (x1,y1)) is non empty) & (n2 is non empty implies ( OR2 (x2,y2)) is non empty) & (n3 is non empty implies ( OR2 (x3,y3)) is non empty) & (n4 is non empty implies ( OR2 (x4,y4)) is non empty) & (n is non empty implies ( AND5 (c1,n1,n2,n3,n4)) is non empty) & (c5b is non empty iff ( OR2 (c5,n)) is non empty) implies (c5 is non empty iff c5b is non empty)

    proof

      let c1,x1,x2,x3,x4,y1,y2,y3,y4,c2,c3,c4,c5,n1,n2,n3,n4,n,c5b be set;

      thus (( MAJ3 (x1,y1,c1)) is non empty implies c2 is non empty) & (( MAJ3 (x2,y2,c2)) is non empty implies c3 is non empty) & (( MAJ3 (x3,y3,c3)) is non empty implies c4 is non empty) & (( MAJ3 (x4,y4,c4)) is non empty implies c5 is non empty) & (n1 is non empty implies ( OR2 (x1,y1)) is non empty) & (n2 is non empty implies ( OR2 (x2,y2)) is non empty) & (n3 is non empty implies ( OR2 (x3,y3)) is non empty) & (n4 is non empty implies ( OR2 (x4,y4)) is non empty) & (n is non empty implies ( AND5 (c1,n1,n2,n3,n4)) is non empty) & (c5b is non empty iff ( OR2 (c5,n)) is non empty) implies (c5 is non empty iff c5b is non empty)

      proof

        assume that

         A1: (( MAJ3 (x1,y1,c1)) is non empty implies c2 is non empty) & (( MAJ3 (x2,y2,c2)) is non empty implies c3 is non empty) & (( MAJ3 (x3,y3,c3)) is non empty implies c4 is non empty) and

         A2: ( MAJ3 (x4,y4,c4)) is non empty implies c5 is non empty and

         A3: n1 is non empty implies ( OR2 (x1,y1)) is non empty and

         A4: n2 is non empty implies ( OR2 (x2,y2)) is non empty and

         A5: n3 is non empty implies ( OR2 (x3,y3)) is non empty and

         A6: n4 is non empty implies ( OR2 (x4,y4)) is non empty and

         A7: n is non empty implies ( AND5 (c1,n1,n2,n3,n4)) is non empty and

         A8: c5b is non empty implies ( OR2 (c5,n)) is non empty and

         A9: ( OR2 (c5,n)) is non empty implies c5b is non empty;

         A10:

        now

          assume

           A11: n is non empty;

          then

           A12: c1 is non empty by A7, Def18;

          

           A13: x3 is non empty or y3 is non empty by A5, A7, A11, Def18;

          

           A14: x2 is non empty or y2 is non empty by A4, A7, A11, Def18;

          

           A15: x4 is non empty or y4 is non empty by A6, A7, A11, Def18;

          x1 is non empty or y1 is non empty by A3, A7, A11, Def18;

          hence ( MAJ3 (x4,y4,c4)) is non empty by A1, A12, A14, A13, A15;

        end;

        thus c5 is non empty implies c5b is non empty by A9;

        assume c5b is non empty;

        hence thesis by A2, A8, A10;

      end;

    end;

    definition

      let a,b be set;

      :: GATE_1:def34

      func MODADD2 (a,b) -> set equals

      : Def34: ( NOT1 {} ) if (a is non empty or b is non empty) & not (a is non empty & b is non empty)

      otherwise {} ;

      correctness ;

      commutativity ;

    end

    theorem :: GATE_1:41

    ( MODADD2 (a,b)) is non empty iff (a is non empty or b is non empty) & not (a is non empty & b is non empty) by Def34;

    notation

      let a,b,c be set;

      synonym ADD1 (a,b,c) for XOR3 (a,b,c);

      synonym CARR1 (a,b,c) for MAJ3 (a,b,c);

    end

    definition

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

      :: GATE_1:def35

      func ADD2 (a2,b2,a1,b1,c) -> set equals ( XOR3 (a2,b2,( CARR1 (a1,b1,c))));

      coherence ;

    end

    definition

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

      :: GATE_1:def36

      func CARR2 (a2,b2,a1,b1,c) -> set equals ( MAJ3 (a2,b2,( CARR1 (a1,b1,c))));

      coherence ;

    end

    definition

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

      :: GATE_1:def37

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

      coherence ;

    end

    definition

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

      :: GATE_1:def38

      func CARR3 (a3,b3,a2,b2,a1,b1,c) -> set equals ( MAJ3 (a3,b3,( CARR2 (a2,b2,a1,b1,c))));

      coherence ;

    end

    definition

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

      :: GATE_1:def39

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

      coherence ;

    end

    definition

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

      :: GATE_1:def40

      func CARR4 (a4,b4,a3,b3,a2,b2,a1,b1,c) -> set equals ( MAJ3 (a4,b4,( CARR3 (a3,b3,a2,b2,a1,b1,c))));

      coherence ;

    end

    theorem :: GATE_1:42

    for c1,x1,y1,x2,y2,x3,y3,x4,y4,c4,q1,p1,sd1,q2,p2,sd2,q3,p3,sd3,q4,p4,sd4,cb1,cb2,l2,t2,l3,m3,t3,l4,m4,n4,t4,l5,m5,n5,o5,s1,s2,s3,s4 be set holds (q1 is non empty iff ( NOR2 (x1,y1)) is non empty) & (p1 is non empty iff ( NAND2 (x1,y1)) is non empty) & (sd1 is non empty iff ( MODADD2 (x1,y1)) is non empty) & (q2 is non empty iff ( NOR2 (x2,y2)) is non empty) & (p2 is non empty iff ( NAND2 (x2,y2)) is non empty) & (sd2 is non empty iff ( MODADD2 (x2,y2)) is non empty) & (q3 is non empty iff ( NOR2 (x3,y3)) is non empty) & (p3 is non empty iff ( NAND2 (x3,y3)) is non empty) & (sd3 is non empty iff ( MODADD2 (x3,y3)) is non empty) & (q4 is non empty iff ( NOR2 (x4,y4)) is non empty) & (p4 is non empty iff ( NAND2 (x4,y4)) is non empty) & (sd4 is non empty iff ( MODADD2 (x4,y4)) is non empty) & (cb1 is non empty iff ( NOT1 c1) is non empty) & (cb2 is non empty iff ( NOT1 cb1) is non empty) & (s1 is non empty iff ( XOR2 (cb2,sd1)) is non empty) & (l2 is non empty iff ( AND2 (cb1,p1)) is non empty) & (t2 is non empty iff ( NOR2 (l2,q1)) is non empty) & (s2 is non empty iff ( XOR2 (t2,sd2)) is non empty) & (l3 is non empty iff ( AND2 (q1,p2)) is non empty) & (m3 is non empty iff ( AND3 (p2,p1,cb1)) is non empty) & (t3 is non empty iff ( NOR3 (l3,m3,q2)) is non empty) & (s3 is non empty iff ( XOR2 (t3,sd3)) is non empty) & (l4 is non empty iff ( AND2 (q2,p3)) is non empty) & (m4 is non empty iff ( AND3 (q1,p3,p2)) is non empty) & (n4 is non empty iff ( AND4 (p3,p2,p1,cb1)) is non empty) & (t4 is non empty iff ( NOR4 (l4,m4,n4,q3)) is non empty) & (s4 is non empty iff ( XOR2 (t4,sd4)) is non empty) & (l5 is non empty iff ( AND2 (q3,p4)) is non empty) & (m5 is non empty iff ( AND3 (q2,p4,p3)) is non empty) & (n5 is non empty iff ( AND4 (q1,p4,p3,p2)) is non empty) & (o5 is non empty iff ( AND5 (p4,p3,p2,p1,cb1)) is non empty) & (c4 is non empty iff ( NOR5 (q4,l5,m5,n5,o5)) is non empty) implies (s1 is non empty iff ( ADD1 (x1,y1,c1)) is non empty) & (s2 is non empty iff ( ADD2 (x2,y2,x1,y1,c1)) is non empty) & (s3 is non empty iff ( ADD3 (x3,y3,x2,y2,x1,y1,c1)) is non empty) & (s4 is non empty iff ( ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty) & (c4 is non empty iff ( CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty)

    proof

      let c1,x1,y1,x2,y2,x3,y3,x4,y4,c4,q1,p1,sd1,q2,p2,sd2,q3,p3,sd3,q4,p4,sd4,cb1,cb2,l2,t2,l3,m3,t3,l4,m4,n4,t4,l5,m5,n5,o5,s1,s2,s3,s4 be set;

      assume that

       A1: q1 is non empty iff ( NOR2 (x1,y1)) is non empty and

       A2: p1 is non empty iff ( NAND2 (x1,y1)) is non empty and

       A3: sd1 is non empty iff ( MODADD2 (x1,y1)) is non empty and

       A4: q2 is non empty iff ( NOR2 (x2,y2)) is non empty;

      thus (p2 is non empty iff ( NAND2 (x2,y2)) is non empty) & (sd2 is non empty iff ( MODADD2 (x2,y2)) is non empty) & (q3 is non empty iff ( NOR2 (x3,y3)) is non empty) & (p3 is non empty iff ( NAND2 (x3,y3)) is non empty) & (sd3 is non empty iff ( MODADD2 (x3,y3)) is non empty) & (q4 is non empty iff ( NOR2 (x4,y4)) is non empty) & (p4 is non empty iff ( NAND2 (x4,y4)) is non empty) & (sd4 is non empty iff ( MODADD2 (x4,y4)) is non empty) & (cb1 is non empty iff ( NOT1 c1) is non empty) & (cb2 is non empty iff ( NOT1 cb1) is non empty) & (s1 is non empty iff ( XOR2 (cb2,sd1)) is non empty) & (l2 is non empty iff ( AND2 (cb1,p1)) is non empty) & (t2 is non empty iff ( NOR2 (l2,q1)) is non empty) & (s2 is non empty iff ( XOR2 (t2,sd2)) is non empty) & (l3 is non empty iff ( AND2 (q1,p2)) is non empty) & (m3 is non empty iff ( AND3 (p2,p1,cb1)) is non empty) & (t3 is non empty iff ( NOR3 (l3,m3,q2)) is non empty) & (s3 is non empty iff ( XOR2 (t3,sd3)) is non empty) & (l4 is non empty iff ( AND2 (q2,p3)) is non empty) & (m4 is non empty iff ( AND3 (q1,p3,p2)) is non empty) & (n4 is non empty iff ( AND4 (p3,p2,p1,cb1)) is non empty) & (t4 is non empty iff ( NOR4 (l4,m4,n4,q3)) is non empty) & (s4 is non empty iff ( XOR2 (t4,sd4)) is non empty) & (l5 is non empty iff ( AND2 (q3,p4)) is non empty) & (m5 is non empty iff ( AND3 (q2,p4,p3)) is non empty) & (n5 is non empty iff ( AND4 (q1,p4,p3,p2)) is non empty) & (o5 is non empty iff ( AND5 (p4,p3,p2,p1,cb1)) is non empty) & (c4 is non empty iff ( NOR5 (q4,l5,m5,n5,o5)) is non empty) implies (s1 is non empty iff ( ADD1 (x1,y1,c1)) is non empty) & (s2 is non empty iff ( ADD2 (x2,y2,x1,y1,c1)) is non empty) & (s3 is non empty iff ( ADD3 (x3,y3,x2,y2,x1,y1,c1)) is non empty) & (s4 is non empty iff ( ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty) & (c4 is non empty iff ( CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty)

      proof

        assume that

         A5: p2 is non empty iff ( NAND2 (x2,y2)) is non empty and

         A6: sd2 is non empty iff ( MODADD2 (x2,y2)) is non empty and

         A7: q3 is non empty iff ( NOR2 (x3,y3)) is non empty and

         A8: p3 is non empty iff ( NAND2 (x3,y3)) is non empty and

         A9: sd3 is non empty iff ( MODADD2 (x3,y3)) is non empty and

         A10: q4 is non empty iff ( NOR2 (x4,y4)) is non empty and

         A11: p4 is non empty iff ( NAND2 (x4,y4)) is non empty and

         A12: sd4 is non empty iff ( MODADD2 (x4,y4)) is non empty and

         A13: cb1 is non empty iff ( NOT1 c1) is non empty and

         A14: (cb2 is non empty iff ( NOT1 cb1) is non empty) & (s1 is non empty iff ( XOR2 (cb2,sd1)) is non empty) and

         A15: l2 is non empty iff ( AND2 (cb1,p1)) is non empty and

         A16: (t2 is non empty iff ( NOR2 (l2,q1)) is non empty) & (s2 is non empty iff ( XOR2 (t2,sd2)) is non empty) and

         A17: l3 is non empty iff ( AND2 (q1,p2)) is non empty and

         A18: m3 is non empty iff ( AND3 (p2,p1,cb1)) is non empty and

         A19: (t3 is non empty iff ( NOR3 (l3,m3,q2)) is non empty) & (s3 is non empty iff ( XOR2 (t3,sd3)) is non empty) and

         A20: l4 is non empty iff ( AND2 (q2,p3)) is non empty and

         A21: (m4 is non empty iff ( AND3 (q1,p3,p2)) is non empty) & (n4 is non empty iff ( AND4 (p3,p2,p1,cb1)) is non empty) & (t4 is non empty iff ( NOR4 (l4,m4,n4,q3)) is non empty) & (s4 is non empty iff ( XOR2 (t4,sd4)) is non empty) and

         A22: l5 is non empty iff ( AND2 (q3,p4)) is non empty and

         A23: (m5 is non empty iff ( AND3 (q2,p4,p3)) is non empty) & (n5 is non empty iff ( AND4 (q1,p4,p3,p2)) is non empty) & (o5 is non empty iff ( AND5 (p4,p3,p2,p1,cb1)) is non empty) and

         A24: c4 is non empty iff ( NOR5 (q4,l5,m5,n5,o5)) is non empty;

        

         A25: p1 is non empty iff not (x1 is non empty & y1 is non empty) by A2;

        

         A26: sd1 is non empty iff (x1 is non empty or y1 is non empty) & not (x1 is non empty & y1 is non empty) by A3, Def34;

        hereby

          assume

           A27: s1 is non empty;

          per cases by A13, A14, A27;

            suppose c1 is non empty & sd1 is empty;

            hence ( ADD1 (x1,y1,c1)) is non empty by A26;

          end;

            suppose c1 is empty & sd1 is non empty;

            hence ( ADD1 (x1,y1,c1)) is non empty by A26;

          end;

        end;

        hereby

          assume

           A28: ( ADD1 (x1,y1,c1)) is non empty;

          per cases by A26, A28;

            suppose c1 is non empty & sd1 is empty;

            hence s1 is non empty by A13, A14;

          end;

            suppose c1 is empty & sd1 is non empty;

            hence s1 is non empty by A13, A14;

          end;

        end;

        

         A29: q1 is non empty iff not (x1 is non empty or y1 is non empty) by A1;

        

         A30: sd2 is non empty iff (x2 is non empty or y2 is non empty) & not (x2 is non empty & y2 is non empty) by A6, Def34;

        hereby

          assume

           A31: s2 is non empty;

          per cases by A13, A15, A16, A31;

            suppose (c1 is non empty or p1 is empty) & q1 is empty & sd2 is empty;

            hence ( ADD2 (x2,y2,x1,y1,c1)) is non empty by A29, A25, A30;

          end;

            suppose (c1 is empty & p1 is non empty or q1 is non empty) & sd2 is non empty;

            hence ( ADD2 (x2,y2,x1,y1,c1)) is non empty by A29, A25, A30;

          end;

        end;

        

         A32: cb1 is non empty iff not c1 is non empty by A13;

        hereby

          assume

           A33: ( ADD2 (x2,y2,x1,y1,c1)) is non empty;

          per cases by A15, A29, A25, A30, A32, A33;

            suppose l2 is empty & q1 is empty & sd2 is empty;

            hence s2 is non empty by A16;

          end;

            suppose (l2 is non empty or q1 is non empty) & sd2 is non empty;

            hence s2 is non empty by A16;

          end;

        end;

        

         A34: q2 is non empty iff not (x2 is non empty or y2 is non empty) by A4;

        

         A35: p2 is non empty iff not (x2 is non empty & y2 is non empty) by A5;

        

         A36: sd3 is non empty iff (x3 is non empty or y3 is non empty) & not (x3 is non empty & y3 is non empty) by A9, Def34;

        hereby

          assume

           A37: s3 is non empty;

          per cases by A9, A19, A37, Def13, Def34;

            suppose l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty;

            hence ( ADD3 (x3,y3,x2,y2,x1,y1,c1)) is non empty by A17, A18, A29, A25, A34, A35, A32;

          end;

            suppose l3 is empty & m3 is empty & q2 is empty & x3 is non empty & y3 is non empty;

            hence ( ADD3 (x3,y3,x2,y2,x1,y1,c1)) is non empty by A17, A18, A29, A25, A34, A35, A32;

          end;

            suppose

             A38: l3 is non empty & sd3 is non empty;

            then

             A39: x2 is empty or y2 is empty by A5, A17;

            x1 is empty & y1 is empty by A1, A17, A38;

            hence ( ADD3 (x3,y3,x2,y2,x1,y1,c1)) is non empty by A36, A38, A39;

          end;

            suppose

             A40: m3 is non empty & sd3 is non empty;

            then c1 is empty by A13, A18;

            hence ( ADD3 (x3,y3,x2,y2,x1,y1,c1)) is non empty by A18, A25, A35, A36, A40;

          end;

            suppose q2 is non empty & sd3 is non empty;

            hence ( ADD3 (x3,y3,x2,y2,x1,y1,c1)) is non empty by A34, A36;

          end;

        end;

        hereby

          assume

           A41: ( ADD3 (x3,y3,x2,y2,x1,y1,c1)) is non empty;

          per cases by A17, A18, A29, A25, A34, A35, A36, A32, A41;

            suppose l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty;

            hence s3 is non empty by A9, A19, Def13, Def34;

          end;

            suppose l3 is empty & m3 is empty & q2 is empty & x3 is non empty & y3 is non empty;

            hence s3 is non empty by A9, A19, Def13, Def34;

          end;

            suppose l3 is non empty & sd3 is non empty;

            hence s3 is non empty by A19, Def13;

          end;

            suppose m3 is non empty & sd3 is non empty;

            hence s3 is non empty by A19, Def13;

          end;

            suppose q2 is non empty & sd3 is non empty;

            hence s3 is non empty by A19, Def13;

          end;

        end;

        

         A42: p3 is non empty iff not (x3 is non empty & y3 is non empty) by A8;

        

         A43: sd4 is non empty iff (x4 is non empty or y4 is non empty) & not (x4 is non empty & y4 is non empty) by A12, Def34;

        

         A44: q3 is non empty iff not (x3 is non empty or y3 is non empty) by A7;

        hereby

          assume

           A45: s4 is non empty;

          per cases by A13, A21, A45, Def14, Def17;

            suppose l4 is empty & (q1 is empty or p3 is empty or p2 is empty) & (p3 is empty or p2 is empty or p1 is empty or c1 is non empty) & q3 is empty & sd4 is empty;

            hence ( ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A20, A29, A25, A34, A35, A44, A42, A43;

          end;

            suppose l4 is non empty & sd4 is non empty;

            hence ( ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A20, A34, A42, A43;

          end;

            suppose q1 is non empty & p3 is non empty & p2 is non empty & sd4 is non empty;

            hence ( ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A29, A35, A42, A43;

          end;

            suppose p3 is non empty & p2 is non empty & p1 is non empty & c1 is empty & sd4 is non empty;

            hence ( ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A25, A35, A42, A43;

          end;

            suppose q3 is non empty & sd4 is non empty;

            hence ( ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A44, A43;

          end;

        end;

        hereby

          assume

           A46: ( ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty;

          thus s4 is non empty

          proof

            assume

             A47: s4 is empty;

            per cases by A13, A21, A47, Def14, Def17;

              suppose l4 is empty & (q1 is empty or p3 is empty or p2 is empty) & (p3 is empty or p2 is empty or p1 is empty or c1 is non empty) & q3 is empty & sd4 is non empty;

              hence thesis by A20, A29, A25, A34, A35, A44, A42, A43, A46;

            end;

              suppose l4 is non empty & sd4 is empty;

              hence thesis by A20, A34, A42, A43, A46;

            end;

              suppose q1 is non empty & p3 is non empty & p2 is non empty & sd4 is empty;

              hence thesis by A29, A35, A42, A43, A46;

            end;

              suppose p3 is non empty & p2 is non empty & p1 is non empty & c1 is empty & sd4 is empty;

              hence thesis by A25, A35, A42, A43, A46;

            end;

              suppose q3 is non empty & sd4 is empty;

              hence thesis by A44, A43, A46;

            end;

          end;

        end;

        

         A48: p4 is non empty iff not (x4 is non empty & y4 is non empty) by A11;

        

         A49: q4 is non empty iff not (x4 is non empty or y4 is non empty) by A10;

        now

          assume that

           A50: q4 is empty and

           A51: l5 is empty and

           A52: m5 is empty & n5 is empty & o5 is empty;

          per cases by A13, A23, A52, Def14, Def18;

            suppose p4 is empty;

            hence ( CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A48;

          end;

            suppose p3 is empty;

            hence ( CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A42, A49, A50;

          end;

            suppose p2 is empty & q2 is empty;

            hence ( CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A22, A35, A44, A49, A48, A50, A51;

          end;

            suppose p1 is empty & q2 is empty;

            hence ( CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A22, A25, A34, A44, A49, A48, A50, A51;

          end;

            suppose c1 is non empty & q1 is empty & q2 is empty;

            hence ( CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A22, A29, A34, A44, A49, A48, A50, A51;

          end;

        end;

        hence c4 is non empty implies ( CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty by A24, Def21;

        assume

         A53: ( CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1)) is non empty;

        assume

         A54: c4 is empty;

        per cases by A13, A22, A23, A24, A54, Def14, Def18, Def21;

          suppose q4 is non empty;

          hence thesis by A49, A53;

        end;

          suppose q3 is non empty & p4 is non empty;

          hence thesis by A44, A48, A53;

        end;

          suppose q2 is non empty & p4 is non empty & p3 is non empty;

          hence thesis by A34, A42, A48, A53;

        end;

          suppose q1 is non empty & p4 is non empty & p3 is non empty & p2 is non empty;

          hence thesis by A29, A35, A42, A48, A53;

        end;

          suppose p4 is non empty & p3 is non empty & p2 is non empty & p1 is non empty & c1 is empty;

          hence thesis by A25, A35, A42, A48, A53;

        end;

      end;

    end;