The Mizar abstract of GATE

Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users
The abstract of the Mizar article:: Logic Gates and Logical Equivalence of Adders
by
Yatsuka Nakamura
Received February 4, 1999
MML identifier: GATE_1
[ Mizar article, MML identifier index ]
environ

 vocabulary BOOLE, GATE_1;
 notation XBOOLE_0;
 constructors XBOOLE_0;
 clusters XBOOLE_0;
 requirements BOOLE;


begin :: Definition of Logical Values and Logic Gates

definition let a be set;
  redefine attr a is empty;
  antonym $a;
end;

theorem :: GATE_1:1
for a being set st a={{}:not contradiction} holds $a;

theorem :: GATE_1:2
ex a being set st $a;

definition let a be set;
  func NOT1 a equals
:: GATE_1:def 1
   {} if $a
   otherwise {{}:not contradiction};
end;

canceled;

theorem :: GATE_1:4
  for a being set holds $NOT1 a iff not($a);

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

theorem :: GATE_1:5
  $ NOT1 {};

definition let a,b be set;
  func AND2(a,b) equals
:: GATE_1:def 2
   NOT1 {} if $a & $b
   otherwise {};
 end;

theorem :: GATE_1:6
   $AND2(a,b) iff ($a & $b);

definition let a,b be set;
  func OR2(a, b) equals
:: GATE_1:def 3
   NOT1 {} if ($a or $b)
      otherwise {};
end;

theorem :: GATE_1:7
  $OR2(a,b) iff ($a or $b);

definition let a,b be set;
 func XOR2(a,b) equals
:: GATE_1:def 4
   NOT1 {} if ($a & not $b) or (not $a & $b)
  otherwise {};
end;

theorem :: GATE_1:8
   $XOR2(a, b) iff ($a & not $b) or (not $a & $b);

theorem :: GATE_1:9
    $XOR2(a,a) iff contradiction;

theorem :: GATE_1:10
    $XOR2(a,{}) iff $a;

theorem :: GATE_1:11
    $XOR2(a,b) iff $XOR2(b,a);

definition let a,b be set;
  func EQV2(a, b) equals
:: GATE_1:def 5
   NOT1 {} if ($a iff $b)
  otherwise {};
end;

theorem :: GATE_1:12
   $EQV2(a, b) iff ($a iff $b);

theorem :: GATE_1:13
    $EQV2(a,b) iff not $XOR2(a,b);

definition let a,b be set;
  func NAND2(a, b) equals
:: GATE_1:def 6
   NOT1 {} if not ($a & $b)
  otherwise {};
end;

theorem :: GATE_1:14
   $NAND2(a, b) iff not ($a & $b);

definition let a,b be set;
  func NOR2(a, b) equals
:: GATE_1:def 7
   NOT1 {} if not ($a or $b)
  otherwise {};
end;

theorem :: GATE_1:15
   $NOR2(a,b) iff not ($a or $b);

definition let a,b,c be set;
  func AND3(a,b,c) equals
:: GATE_1:def 8
   NOT1 {} if $a & $b & $c
  otherwise {};
end;

theorem :: GATE_1:16
   $AND3(a,b,c) iff $a & $b & $c;

definition let a,b,c be set;
  func OR3(a,b,c) equals
:: GATE_1:def 9
   NOT1 {} if $a or $b or $c
  otherwise {};
end;

theorem :: GATE_1:17
    $OR3(a,b,c) iff $a or $b or $c;

definition let a,b,c be set;
  func XOR3(a,b,c) equals
:: GATE_1:def 10
   NOT1 {} if
  (($a & not $b) or (not $a & $b)) & not $c or
  not (($a & not $b) or (not $a & $b)) & $c
  otherwise {};
end;

theorem :: GATE_1:18
  $XOR3(a,b,c) iff
  (($a & not $b) or (not $a & $b)) & not $c or
  not (($a & not $b) or (not $a & $b)) & $c;

definition let a,b,c be set;
  func MAJ3(a,b,c) equals
:: GATE_1:def 11
   NOT1 {} if $a & $b or $b & $c or $c & $a
  otherwise {};
end;

theorem :: GATE_1:19
  $MAJ3(a,b,c) iff $a & $b or $b & $c or $c & $a;

definition let a,b,c be set;
  func NAND3(a,b,c) equals
:: GATE_1:def 12
   NOT1 {} if not ($a & $b & $c)
  otherwise {};
end;

theorem :: GATE_1:20
    $NAND3(a,b,c) iff not ($a & $b & $c);

definition let a,b,c be set;
  func NOR3(a,b,c) equals
:: GATE_1:def 13
   NOT1 {} if not ($a or $b or $c)
  otherwise {};
end;

theorem :: GATE_1:21
   $NOR3(a,b,c) iff not ($a or $b or $c);

definition let a,b,c,d be set;
  func AND4(a,b,c,d) equals
:: GATE_1:def 14
    NOT1 {} if $a & $b & $c & $d
  otherwise {};
end;

theorem :: GATE_1:22
   $AND4(a,b,c,d) iff $a & $b & $c & $d;

definition let a,b,c,d be set;
  func OR4(a,b,c,d) equals
:: GATE_1:def 15
   NOT1 {} if $a or $b or $c or $d
  otherwise {};
end;

theorem :: GATE_1:23
    $OR4(a,b,c,d) iff $a or $b or $c or $d;

definition let a,b,c,d be set;
  func NAND4(a,b,c,d) equals
:: GATE_1:def 16
   NOT1 {} if not ($a & $b & $c & $d)
  otherwise {};
end;

theorem :: GATE_1:24
    $NAND4(a,b,c,d) iff not ($a & $b & $c & $d);

definition let a,b,c,d be set;
  func NOR4(a,b,c,d) equals
:: GATE_1:def 17
   NOT1 {} if not ($a or $b or $c or $d)
  otherwise {};
end;

theorem :: GATE_1:25
   $NOR4(a,b,c,d) iff not ($a or $b or $c or $d);

definition let a,b,c,d,e be set;
  func AND5(a,b,c,d,e) equals
:: GATE_1:def 18
   NOT1 {} if $a & $b & $c & $d & $e
  otherwise {};
end;

theorem :: GATE_1:26
   $AND5(a,b,c,d,e) iff $a & $b & $c & $d & $e;

definition let a,b,c,d,e be set;
  func OR5(a,b,c,d,e) equals
:: GATE_1:def 19
   NOT1 {} if $a or $b or $c or $d or $e
  otherwise {};
end;

theorem :: GATE_1:27
    $OR5(a,b,c,d,e) iff $a or $b or $c or $d or $e;

definition let a,b,c,d,e be set;
  func NAND5(a,b,c,d,e) equals
:: GATE_1:def 20
   NOT1 {} if not ($a & $b & $c & $d & $e)
  otherwise {};
end;

theorem :: GATE_1:28
  $NAND5(a,b,c,d,e) iff not ($a & $b & $c & $d & $e);

definition let a,b,c,d,e be set;
  func NOR5(a,b,c,d,e) equals
:: GATE_1:def 21
   NOT1 {} if not ($a or $b or $c or $d or $e)
  otherwise {};
end;

theorem :: GATE_1:29
  $NOR5(a,b,c,d,e) iff not ($a or $b or $c or $d or $e);

definition let a,b,c,d,e,f be set;
  func AND6(a,b,c,d,e,f) equals
:: GATE_1:def 22
   NOT1 {} if $a & $b & $c & $d & $e &$f
  otherwise {};
end;

theorem :: GATE_1:30
  $AND6(a,b,c,d,e,f) iff $a & $b & $c & $d & $e &$f;

definition let a,b,c,d,e,f be set;
  func OR6(a,b,c,d,e,f) equals
:: GATE_1:def 23
   NOT1 {} if $a or $b or $c or $d or $e or $f
  otherwise {};
 end;

theorem :: GATE_1:31
  $OR6(a,b,c,d,e,f) iff $a or $b or $c or $d or $e or $f;

definition let a,b,c,d,e,f be set;
  func NAND6(a,b,c,d,e,f) equals
:: GATE_1:def 24
   NOT1 {} if not ($a & $b & $c & $d & $e &$f)
  otherwise {};
end;

theorem :: GATE_1:32
  $NAND6(a,b,c,d,e,f) iff not ($a & $b & $c & $d & $e &$f);

definition let a,b,c,d,e,f be set;
  func NOR6(a,b,c,d,e,f) equals
:: GATE_1:def 25
   NOT1 {} if not ($a or $b or $c or $d or $e or $f)
  otherwise {};
end;

theorem :: GATE_1:33
  $NOR6(a,b,c,d,e,f) iff not ($a or $b or $c or $d or $e or $f);

definition let a,b,c,d,e,f,g be set;
  func AND7(a,b,c,d,e,f,g) equals
:: GATE_1:def 26
   NOT1 {} if $a & $b & $c & $d & $e & $f & $g
  otherwise {};
end;

theorem :: GATE_1:34
  $AND7(a,b,c,d,e,f,g) iff $a & $b & $c & $d & $e & $f & $g;

definition let a,b,c,d,e,f,g be set;
  func OR7(a,b,c,d,e,f,g) equals
:: GATE_1:def 27
   NOT1 {} if $a or $b or $c or $d or $e or $f or $g
  otherwise {};
end;

theorem :: GATE_1:35
  $OR7(a,b,c,d,e,f,g) iff $a or $b or $c or $d or $e or $f or $g;

definition let a,b,c,d,e,f,g be set;
  func NAND7(a,b,c,d,e,f,g) equals
:: GATE_1:def 28
   NOT1 {} if not ($a & $b & $c & $d & $e & $f & $g)
  otherwise {};
end;

theorem :: GATE_1:36
    $NAND7(a,b,c,d,e,f,g) iff
   not ($a & $b & $c & $d & $e & $f & $g);

definition let a,b,c,d,e,f,g be set;
  func NOR7(a,b,c,d,e,f,g) equals
:: GATE_1:def 29
   NOT1 {} if not ($a or $b or $c or $d or $e or $f or $g)
  otherwise {};
end;

theorem :: GATE_1:37
    $NOR7(a,b,c,d,e,f,g) iff
   not ($a or $b or $c or $d or $e or $f or $g);

definition let a,b,c,d,e,f,g,h be set;
  func AND8(a,b,c,d,e,f,g,h) equals
:: GATE_1:def 30
   NOT1 {} if $a & $b & $c & $d & $e & $f & $g & $h
  otherwise {};
end;

theorem :: GATE_1:38
    $AND8(a,b,c,d,e,f,g,h) iff $a & $b & $c & $d & $e & $f & $g & $h;

definition let a,b,c,d,e,f,g,h be set;
  func OR8(a,b,c,d,e,f,g,h) equals
:: GATE_1:def 31
   NOT1 {} if
  $a or $b or $c or $d or $e or $f or $g or $h
  otherwise {};
end;

theorem :: GATE_1:39
    $OR8(a,b,c,d,e,f,g,h) iff
  $a or $b or $c or $d or $e or $f or $g or $h;

definition let a,b,c,d,e,f,g,h be set;
  func NAND8(a,b,c,d,e,f,g,h) equals
:: GATE_1:def 32
   NOT1 {} if
  not ($a & $b & $c & $d & $e & $f & $g & $h)
  otherwise {};
end;

theorem :: GATE_1:40
    $NAND8(a,b,c,d,e,f,g,h) iff
   not ($a & $b & $c & $d & $e & $f & $g & $h);

definition let a,b,c,d,e,f,g,h be set;
  func NOR8(a,b,c,d,e,f,g,h) equals
:: GATE_1:def 33
   NOT1 {} if not ($a or $b or $c or $d or $e or $f or $g or $h)
  otherwise {};
end;

theorem :: GATE_1:41
    $NOR8(a,b,c,d,e,f,g,h) iff
    not ($a or $b or $c or $d or $e or $f or $g or $h);

begin :: Logical Equivalence of 4 Bits Adders

:: 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:42
   for c1,x1,x2,x3,x4,y1,y2,y3,y4,c2,c3,c4,c5,n1,n2,n3,n4,n,c5b being set holds
        ::Specification of Normal 4 Bit Adder
        ($c2 iff $MAJ3(x1,y1,c1)) &
        ($c3 iff $MAJ3(x2,y2,c2)) &
        ($c4 iff $MAJ3(x3,y3,c3)) &
        ($c5 iff $MAJ3(x4,y4,c4)) &
        ::Specification of Carry Skip Adder
        ($n1 iff $OR2(x1,y1))&
        ($n2 iff $OR2(x2,y2))&
        ($n3 iff $OR2(x3,y3))&
        ($n4 iff $OR2(x4,y4))&
        ($n iff $AND5(c1,n1,n2,n3,n4))&
        ($c5b iff $OR2(c5,n))
        implies ($c5 iff $c5b);

::Definition of mod 2 adder used in 'Carry Look Ahead Adder'
definition let a,b be set;
  func MODADD2(a,b) equals
:: GATE_1:def 34
   NOT1 {} if not not ($a or $b) & not($a & $b)
  otherwise {};
end;

theorem :: GATE_1:43
   $MODADD2(a,b) iff not not ($a or $b) & not($a & $b);

::The following two definitions are for normal 1 bit adder.
definition let a,b,c be set;
  redefine func XOR3(a,b,c);
  synonym ADD1(a,b,c);
  redefine func MAJ3(a,b,c);
  synonym CARR1(a,b,c);
end;

::The following two definitions are for normal 2 bit adder.
definition let a1,b1,a2,b2,c be set;
 canceled 2;

  func ADD2(a2,b2,a1,b1,c) equals
:: GATE_1:def 37
   XOR3(a2,b2,CARR1(a1,b1,c));
end;

definition let a1,b1,a2,b2,c be set;
  func CARR2(a2,b2,a1,b1,c) equals
:: GATE_1:def 38
   MAJ3(a2,b2,CARR1(a1,b1,c));
end;

::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) equals
:: GATE_1:def 39
   XOR3(a3,b3,CARR2(a2,b2,a1,b1,c));
end;

definition let a1,b1,a2,b2,a3,b3,c be set;
  func CARR3(a3,b3,a2,b2,a1,b1,c) equals
:: GATE_1:def 40
   MAJ3(a3,b3,CARR2(a2,b2,a1,b1,c));
end;

::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) equals
:: GATE_1:def 41
   XOR3(a4,b4,CARR3(a3,b3,a2,b2,a1,b1,c));
end;

definition let a1,b1,a2,b2,a3,b3,a4,b4,c be set;
  func CARR4(a4,b4,a3,b3,a2,b2,a1,b1,c) equals
:: GATE_1:def 42
   MAJ3(a4,b4,CARR3(a3,b3,a2,b2,a1,b1,c));
end;

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

Logic Gates and Logical Equivalence of Adders
