Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

### Logic Gates and Logical Equivalence of Adders

by
Yatsuka Nakamura

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

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)) &
(\$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 let a,b be set;
:: 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);
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;

:: 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;
:: 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;
:: 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
:: 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))&
(\$q2 iff \$NOR2(x2,y2))&(\$p2 iff \$NAND2(x2,y2))&
(\$q3 iff \$NOR2(x3,y3))&(\$p3 iff \$NAND2(x3,y3))&
(\$q4 iff \$NOR2(x4,y4))&(\$p4 iff \$NAND2(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))