GATE_1: Logic Gates and Logical Equivalence of Adders

:: Logic Gates and Logical Equivalence of Adders
:: by Yatsuka Nakamura
::
:: Received February 4, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

definition

let a be set ;

func NOT1 a -> set equals :Def1: :: GATE_1:def 1
{} if not a is empty
otherwise {{}};

correctness ;

end;

:: deftheorem Def1 defines NOT1 GATE_1:def 1 :

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 being set holds
( not NOT1 a is empty iff a is empty ) ;

theorem :: GATE_1:3

not NOT1 {} is empty ;

definition

let a, b be set ;

func AND2 (a,b) -> set equals :Def2: :: GATE_1:def 2
NOT1 {} if ( not a is empty & not b is empty )
otherwise {} ;

correctness ;
commutativity ;

end;

:: deftheorem Def2 defines AND2 GATE_1:def 2 :

registration

let a, b be non empty set ;

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

coherence by Def2;

end;

registration

let a be empty set ;
let b be set ;

cluster AND2 (a,b) -> empty ;

coherence by Def2;

end;

theorem :: GATE_1:4

for a, b being set holds
( not AND2 (a,b) is empty iff ( not a is empty & not b is empty ) ) ;

definition

let a, b be set ;

func OR2 (a,b) -> set equals :Def3: :: GATE_1:def 3
NOT1 {} if ( not a is empty or not b is empty )
otherwise {} ;

correctness ;
commutativity ;

end;

:: deftheorem Def3 defines OR2 GATE_1:def 3 :

registration

let a be set ;
let 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

for a, b being set holds
( ( not a is empty or not b is empty ) iff not OR2 (a,b) is empty ) ;

definition

let a, b be set ;

func XOR2 (a,b) -> set equals :Def4: :: GATE_1:def 4
NOT1 {} if ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) )
otherwise {} ;

correctness ;
commutativity ;

end;

:: deftheorem Def4 defines XOR2 GATE_1:def 4 :

registration

let a be empty set ;
let 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

for a, b being set holds
( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) iff not XOR2 (a,b) is empty ) ;

theorem :: GATE_1:7

for a being set holds XOR2 (a,a) is empty

proof end;

theorem :: GATE_1:8

for a being set holds
( not XOR2 (a,{}) is empty iff not a is empty ) ;

theorem :: GATE_1:9

for a, b being set holds
( not XOR2 (a,b) is empty iff not XOR2 (b,a) is empty ) ;

definition

let a, b be set ;

func EQV2 (a,b) -> set equals :Def5: :: GATE_1:def 5
NOT1 {} if ( not a is empty iff not b is empty )
otherwise {} ;

correctness ;
commutativity ;

end;

:: deftheorem Def5 defines EQV2 GATE_1:def 5 :

registration

let a be empty set ;
let 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

for a, b being set holds
( not EQV2 (a,b) is empty iff ( not a is empty iff not b is empty ) ) ;

theorem :: GATE_1:11

for a, b being set holds
( not EQV2 (a,b) is empty iff XOR2 (a,b) is empty )

proof end;

definition

let a, b be set ;

func NAND2 (a,b) -> set equals :Def6: :: GATE_1:def 6
NOT1 {} if ( a is empty or b is empty )
otherwise {} ;

correctness ;
commutativity ;

end;

:: deftheorem Def6 defines NAND2 GATE_1:def 6 :

registration

let a be empty set ;
let 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

for a, b being set holds
( not NAND2 (a,b) is empty & not a is empty iff b is empty ) ;

definition

let a, b be set ;

func NOR2 (a,b) -> set equals :Def7: :: GATE_1:def 7
NOT1 {} if ( a is empty & b is empty )
otherwise {} ;

correctness ;
commutativity ;

end;

:: deftheorem Def7 defines NOR2 GATE_1:def 7 :

registration

let a, b be empty set ;

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

coherence by Def7;

end;

registration

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

cluster NOR2 (a,b) -> empty ;

coherence by Def7;

end;

theorem :: GATE_1:13

for a, b being set holds
( not NOR2 (a,b) is empty iff ( a is empty & b is empty ) ) ;

definition

let a, b, c be set ;

func AND3 (a,b,c) -> set equals :Def8: :: GATE_1:def 8
NOT1 {} if ( not a is empty & not b is empty & not c is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def8 defines AND3 GATE_1:def 8 :

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

for a, b, c being set holds
( not AND3 (a,b,c) is empty iff ( not a is empty & not b is empty & not c is empty ) ) ;

definition

let a, b, c be set ;

func OR3 (a,b,c) -> set equals :Def9: :: GATE_1:def 9
NOT1 {} if ( not a is empty or not b is empty or not c is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def9 defines OR3 GATE_1:def 9 :

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

for a, b, c being set holds
( ( not a is empty or not b is empty or not c is empty ) iff not OR3 (a,b,c) is empty ) ;

definition

let a, b, c be set ;

func XOR3 (a,b,c) -> set equals :Def10: :: GATE_1:def 10
NOT1 {} if ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) )
otherwise {} ;

correctness ;

end;

:: deftheorem Def10 defines XOR3 GATE_1:def 10 :

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

for a, b, c being set holds
( ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) ) iff not XOR3 (a,b,c) is empty ) ;

definition

let a, b, c be set ;

func MAJ3 (a,b,c) -> set equals :Def11: :: GATE_1:def 11
NOT1 {} if ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) )
otherwise {} ;

correctness ;

end;

:: deftheorem Def11 defines MAJ3 GATE_1:def 11 :

registration

let a, b be non empty set ;
let 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 ;
let 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

for a, b, c being set holds
( ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) ) iff not MAJ3 (a,b,c) is empty ) ;

definition

let a, b, c be set ;

func NAND3 (a,b,c) -> set equals :Def12: :: GATE_1:def 12
NOT1 {} if ( a is empty or b is empty or c is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def12 defines NAND3 GATE_1:def 12 :

theorem :: GATE_1:18

for a, b, c being set holds
( not NAND3 (a,b,c) is empty & not a is empty & not b is empty iff c is empty ) by Def12;

definition

let a, b, c be set ;

func NOR3 (a,b,c) -> set equals :Def13: :: GATE_1:def 13
NOT1 {} if ( a is empty & b is empty & c is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def13 defines NOR3 GATE_1:def 13 :

theorem :: GATE_1:19

for a, b, c being set holds
( not NOR3 (a,b,c) is empty iff ( a is empty & b is empty & c is empty ) ) by Def13;

definition

let a, b, c, d be set ;

func AND4 (a,b,c,d) -> set equals :Def14: :: GATE_1:def 14
NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def14 defines AND4 GATE_1:def 14 :

theorem :: GATE_1:20

for a, b, c, d being set holds
( not AND4 (a,b,c,d) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty ) ) by Def14;

definition

let a, b, c, d be set ;

func OR4 (a,b,c,d) -> set equals :Def15: :: GATE_1:def 15
NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def15 defines OR4 GATE_1:def 15 :

theorem :: GATE_1:21

for a, b, c, d being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty ) iff not OR4 (a,b,c,d) is empty ) by Def15;

definition

let a, b, c, d be set ;

func NAND4 (a,b,c,d) -> set equals :Def16: :: GATE_1:def 16
NOT1 {} if ( a is empty or b is empty or c is empty or d is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def16 defines NAND4 GATE_1:def 16 :

theorem :: GATE_1:22

for a, b, c, d being set holds
( not NAND4 (a,b,c,d) is empty & not a is empty & not b is empty & not c is empty iff d is empty ) by Def16;

definition

let a, b, c, d be set ;

func NOR4 (a,b,c,d) -> set equals :Def17: :: GATE_1:def 17
NOT1 {} if ( a is empty & b is empty & c is empty & d is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def17 defines NOR4 GATE_1:def 17 :

theorem :: GATE_1:23

for a, b, c, d being set holds
( not NOR4 (a,b,c,d) is empty iff ( a is empty & b is empty & c is empty & d is empty ) ) by Def17;

definition

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

func AND5 (a,b,c,d,e) -> set equals :Def18: :: GATE_1:def 18
NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def18 defines AND5 GATE_1:def 18 :

theorem :: GATE_1:24

for a, b, c, d, e being set holds
( not AND5 (a,b,c,d,e) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty ) ) by Def18;

definition

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

func OR5 (a,b,c,d,e) -> set equals :Def19: :: GATE_1:def 19
NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def19 defines OR5 GATE_1:def 19 :

theorem :: GATE_1:25

for a, b, c, d, e being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) iff not OR5 (a,b,c,d,e) is empty ) by Def19;

definition

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

func NAND5 (a,b,c,d,e) -> set equals :Def20: :: GATE_1:def 20
NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def20 defines NAND5 GATE_1:def 20 :

theorem :: GATE_1:26

for a, b, c, d, e being set holds
( not NAND5 (a,b,c,d,e) is empty & not a is empty & not b is empty & not c is empty & not d is empty iff e is empty ) by Def20;

definition

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

func NOR5 (a,b,c,d,e) -> set equals :Def21: :: GATE_1:def 21
NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def21 defines NOR5 GATE_1:def 21 :

theorem :: GATE_1:27

for a, b, c, d, e being set holds
( not NOR5 (a,b,c,d,e) is empty iff ( a is empty & b is empty & c is empty & d is empty & e is empty ) ) by Def21;

definition

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

func AND6 (a,b,c,d,e,f) -> set equals :Def22: :: GATE_1:def 22
NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def22 defines AND6 GATE_1:def 22 :

theorem :: GATE_1:28

for a, b, c, d, e, f being set holds
( not AND6 (a,b,c,d,e,f) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty ) ) by Def22;

definition

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

func OR6 (a,b,c,d,e,f) -> set equals :Def23: :: GATE_1:def 23
NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def23 defines OR6 GATE_1:def 23 :

theorem :: GATE_1:29

for a, b, c, d, e, f being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) iff not OR6 (a,b,c,d,e,f) is empty ) by Def23;

definition

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

func NAND6 (a,b,c,d,e,f) -> set equals :Def24: :: GATE_1:def 24
NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def24 defines NAND6 GATE_1:def 24 :

theorem :: GATE_1:30

for a, b, c, d, e, f being set holds
( not NAND6 (a,b,c,d,e,f) is empty & not a is empty & not b is empty & not c is empty & not d is empty & not e is empty iff f is empty ) by Def24;

definition

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

func NOR6 (a,b,c,d,e,f) -> set equals :Def25: :: GATE_1:def 25
NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def25 defines NOR6 GATE_1:def 25 :

theorem :: GATE_1:31

for a, b, c, d, e, f being set holds
( not NOR6 (a,b,c,d,e,f) is empty iff ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty ) ) by Def25;

definition

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

func AND7 (a,b,c,d,e,f,g) -> set equals :Def26: :: GATE_1:def 26
NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def26 defines AND7 GATE_1:def 26 :

theorem :: GATE_1:32

for a, b, c, d, e, f, g being set holds
( not AND7 (a,b,c,d,e,f,g) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty ) ) by Def26;

definition

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

func OR7 (a,b,c,d,e,f,g) -> set equals :Def27: :: GATE_1:def 27
NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def27 defines OR7 GATE_1:def 27 :

theorem :: GATE_1:33

for a, b, c, d, e, f, g being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) iff not OR7 (a,b,c,d,e,f,g) is empty ) by Def27;

definition

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

func NAND7 (a,b,c,d,e,f,g) -> set equals :Def28: :: GATE_1:def 28
NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def28 defines NAND7 GATE_1:def 28 :

theorem :: GATE_1:34

for a, b, c, d, e, f, g being set holds
( not NAND7 (a,b,c,d,e,f,g) is empty & not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty iff g is empty ) by Def28;

definition

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

func NOR7 (a,b,c,d,e,f,g) -> set equals :Def29: :: GATE_1:def 29
NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty & g is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def29 defines NOR7 GATE_1:def 29 :

theorem :: GATE_1:35

for a, b, c, d, e, f, g being set holds
( not NOR7 (a,b,c,d,e,f,g) is empty iff ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty & g is empty ) ) by Def29;

definition

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

func AND8 (a,b,c,d,e,f,g,h) -> set equals :Def30: :: GATE_1:def 30
NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def30 defines AND8 GATE_1:def 30 :

theorem :: GATE_1:36

for a, b, c, d, e, f, g, h being set holds
( not AND8 (a,b,c,d,e,f,g,h) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty ) ) by Def30;

definition

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

func OR8 (a,b,c,d,e,f,g,h) -> set equals :Def31: :: GATE_1:def 31
NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def31 defines OR8 GATE_1:def 31 :

theorem :: GATE_1:37

for a, b, c, d, e, f, g, h being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) iff not OR8 (a,b,c,d,e,f,g,h) is empty ) by Def31;

definition

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

func NAND8 (a,b,c,d,e,f,g,h) -> set equals :Def32: :: GATE_1:def 32
NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def32 defines NAND8 GATE_1:def 32 :

theorem :: GATE_1:38

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

definition

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

func NOR8 (a,b,c,d,e,f,g,h) -> set equals :Def33: :: GATE_1:def 33
NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty & g is empty & h is empty )
otherwise {} ;

correctness ;

end;

:: deftheorem Def33 defines NOR8 GATE_1:def 33 :

theorem :: GATE_1:39

for a, b, c, d, e, f, g, h being set holds
( not NOR8 (a,b,c,d,e,f,g,h) is empty iff ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty & g is empty & h is empty ) ) by Def33;

:: The following theorem shows that an MSB carry of '4 Bit Carry Skip Adder'
:: is equivalent to an MSB carry of a normal 4 bit adder.
:: We assume that there is no feedback loop in adders.

theorem :: GATE_1:40

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

proof end;

::Definition of mod 2 adder used in 'Carry Look Ahead Adder'

definition

let a, b be set ;

func MODADD2 (a,b) -> set equals :Def34: :: GATE_1:def 34
NOT1 {} if ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) )
otherwise {} ;

correctness ;
commutativity ;

end;

:: deftheorem Def34 defines MODADD2 GATE_1:def 34 :

theorem :: GATE_1:41

for a, b being set holds
( not MODADD2 (a,b) is empty iff ( ( not a is empty or not b is empty ) & ( a is empty or b is 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;

::The following two definitions are for normal 2 bit adder.

definition

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

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

coherence ;

end;

:: deftheorem defines ADD2 GATE_1:def 35 :

definition

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

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

coherence ;

end;

:: deftheorem defines CARR2 GATE_1:def 36 :

::The following two definitions are for normal 3 bit adder.

definition

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

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

coherence ;

end;

:: deftheorem defines ADD3 GATE_1:def 37 :

definition

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

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

coherence ;

end;

:: deftheorem defines CARR3 GATE_1:def 38 :

::The following two definitions are for normal 4 bit adder.

definition

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

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

coherence ;

end;

:: deftheorem defines ADD4 GATE_1:def 39 :

definition

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

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

coherence ;

end;

:: deftheorem defines CARR4 GATE_1:def 40 :

::The following theorem shows that outputs of
:: '4 Bit Carry Look Ahead Adder'
:: are equivalent to outputs of normal 4 bits adder.
:: We assume that there is no feedback loop in adders.

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

proof end;