:: Logic Gates and Logical Equivalence of Adders :: by Yatsuka Nakamura :: :: Received February 4, 1999 :: Copyright (c) 1999-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, GATE_1; notations TARSKI, XBOOLE_0; constructors TARSKI, XBOOLE_0; registrations XBOOLE_0; begin :: Definition of Logical Values and Logic Gates definition let a be set; func NOT1 a -> set equals :: GATE_1:def 1 {} if a is non empty otherwise {{}}; end; registration let a be empty set; cluster NOT1 a -> non empty; end; registration let a be non empty set; cluster NOT1 a -> empty; end; theorem :: GATE_1:1 NOT1 {{}} = {} & NOT1 {} = {{}}; theorem :: GATE_1:2 for a being 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; func AND2(a,b) -> set equals :: GATE_1:def 2 NOT1 {} if a is non empty & b is non empty otherwise {}; commutativity; end; registration let a,b be non empty set; cluster AND2(a,b) -> non empty; end; registration let a be empty set, b be set; cluster AND2(a,b) -> empty; 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; func OR2(a, b) -> set equals :: GATE_1:def 3 NOT1 {} if a is non empty or b is non empty otherwise {}; commutativity; end; registration let a be set,b be non empty set; cluster OR2(a,b) -> non empty; end; registration let a,b be empty set; cluster OR2(a,b) -> empty; 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; func XOR2(a,b) -> set equals :: GATE_1:def 4 NOT1 {} if a is non empty & not b is non empty or not a is non empty & b is non empty otherwise {}; commutativity; end; registration let a be empty set,b be non empty set; cluster XOR2(a,b) -> non empty; end; registration let a,b be empty set; cluster XOR2(a,b) -> empty; end; registration let a,b be non empty set; cluster XOR2(a,b) -> empty; 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; 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; func EQV2(a, b) -> set equals :: GATE_1:def 5 NOT1 {} if a is non empty iff b is non empty otherwise {}; commutativity; end; registration let a be empty set,b be non empty set; cluster EQV2(a,b) -> empty; end; registration let a,b be empty set; cluster EQV2(a,b) -> non empty; end; registration let a,b be non empty set; cluster EQV2(a,b) -> non empty; 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; definition let a,b be set; func NAND2(a, b) -> set equals :: GATE_1:def 6 NOT1 {} if not (a is non empty & b is non empty) otherwise {}; commutativity; end; registration let a be empty set, b be set; cluster NAND2(a,b) -> non empty; end; registration let a,b be non empty set; cluster NAND2(a,b) -> empty; 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; func NOR2(a, b) -> set equals :: GATE_1:def 7 NOT1 {} if not (a is non empty or b is non empty) otherwise {}; commutativity; end; registration let a,b be empty set; cluster NOR2(a,b) -> non empty; end; registration let a be non empty set, b be set; cluster NOR2(a,b) -> empty; 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; func AND3(a,b,c) -> set equals :: GATE_1:def 8 NOT1 {} if a is non empty & b is non empty & c is non empty otherwise {}; end; registration let a,b,c be non empty set; cluster AND3(a,b,c) -> non empty; end; registration let a be empty set, b,c be set; cluster AND3(a,b,c) -> empty; cluster AND3(b,a,c) -> empty; cluster AND3(b,c,a) -> empty; 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; func OR3(a,b,c) -> set equals :: GATE_1:def 9 NOT1 {} if a is non empty or b is non empty or c is non empty otherwise {}; end; registration let a,b,c be empty set; cluster OR3(a,b,c) -> empty; end; registration let a be non empty set, b,c be set; cluster OR3(a,b,c) -> non empty; cluster OR3(b,a,c) -> non empty; cluster OR3(b,c,a) -> non empty; 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; func XOR3(a,b,c) -> set equals :: GATE_1:def 10 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 {}; end; registration let a,b,c be empty set; cluster XOR3(a,b,c) -> empty; end; registration let a,b be empty set, c be non empty set; cluster XOR3(a,b,c) -> non empty; cluster XOR3(a,c,b) -> non empty; cluster XOR3(c,a,b) -> non empty; end; registration let a,b be non empty set, c be empty set; cluster XOR3(a,b,c) -> empty; cluster XOR3(a,c,b) -> empty; cluster XOR3(c,a,b) -> empty; end; registration let a,b,c be non empty set; cluster XOR3(a,b,c) -> non empty; 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; func MAJ3(a,b,c) -> set equals :: GATE_1:def 11 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 {}; end; registration let a,b be non empty set, c be set; cluster MAJ3(a,b,c) -> non empty; cluster MAJ3(a,c,b) -> non empty; cluster MAJ3(c,a,b) -> non empty; end; registration let a,b be empty set, c be set; cluster MAJ3(a,b,c) -> empty; cluster MAJ3(a,c,b) -> empty; cluster MAJ3(c,a,b) -> empty; 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; func NAND3(a,b,c) -> set equals :: GATE_1:def 12 NOT1 {} if not (a is non empty & b is non empty & c is non empty) otherwise {}; 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); definition let a,b,c be set; func NOR3(a,b,c) -> set equals :: GATE_1:def 13 NOT1 {} if not (a is non empty or b is non empty or c is non empty) otherwise {}; 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); definition let a,b,c,d be set; func AND4(a,b,c,d) -> set equals :: GATE_1:def 14 NOT1 {} if a is non empty & b is non empty & c is non empty & d is non empty otherwise {}; 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; definition let a,b,c,d be set; func OR4(a,b,c,d) -> set equals :: GATE_1:def 15 NOT1 {} if a is non empty or b is non empty or c is non empty or d is non empty otherwise {}; 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; definition let a,b,c,d be set; func NAND4(a,b,c,d) -> set equals :: GATE_1:def 16 NOT1 {} if not (a is non empty & b is non empty & c is non empty & d is non empty) otherwise {}; 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); definition let a,b,c,d be set; func NOR4(a,b,c,d) -> set equals :: GATE_1:def 17 NOT1 {} if not (a is non empty or b is non empty or c is non empty or d is non empty) otherwise {}; 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); definition let a,b,c,d,e be set; func AND5(a,b,c,d,e) -> set equals :: GATE_1:def 18 NOT1 {} if a is non empty & b is non empty & c is non empty & d is non empty & e is non empty otherwise {}; 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; definition let a,b,c,d,e be set; func OR5(a,b,c,d,e) -> set equals :: GATE_1:def 19 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 {}; 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; definition let a,b,c,d,e be set; func NAND5(a,b,c,d,e) -> set equals :: GATE_1:def 20 NOT1 {} if not (a is non empty & b is non empty & c is non empty & d is non empty & e is non empty) otherwise {}; 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); definition let a,b,c,d,e be set; func NOR5(a,b,c,d,e) -> set equals :: GATE_1:def 21 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 {}; 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); definition let a,b,c,d,e,f be set; func AND6(a,b,c,d,e,f) -> set equals :: GATE_1:def 22 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 {}; 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; definition let a,b,c,d,e,f be set; func OR6(a,b,c,d,e,f) -> set equals :: GATE_1:def 23 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 {}; 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; definition let a,b,c,d,e,f be set; func NAND6(a,b,c,d,e,f) -> set equals :: GATE_1:def 24 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 {}; 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); definition let a,b,c,d,e,f be set; func NOR6(a,b,c,d,e,f) -> set equals :: GATE_1:def 25 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 {}; 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); definition let a,b,c,d,e,f,g be set; func AND7(a,b,c,d,e,f,g) -> set equals :: GATE_1:def 26 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 {}; 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; definition let a,b,c,d,e,f,g be set; func OR7(a,b,c,d,e,f,g) -> set equals :: GATE_1:def 27 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 {}; 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; definition let a,b,c,d,e,f,g be set; func NAND7(a,b,c,d,e,f,g) -> set equals :: GATE_1:def 28 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 {}; 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); definition let a,b,c,d,e,f,g be set; func NOR7(a,b,c,d,e,f,g) -> set equals :: GATE_1:def 29 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 {}; 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); definition let a,b,c,d,e,f,g,h be set; func AND8(a,b,c,d,e,f,g,h) -> set equals :: GATE_1:def 30 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 {}; 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; definition let a,b,c,d,e,f,g,h be set; func OR8(a,b,c,d,e,f,g,h) -> set equals :: GATE_1:def 31 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 {}; 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; definition let a,b,c,d,e,f,g,h be set; func NAND8(a,b,c,d,e,f,g,h) -> set equals :: GATE_1:def 32 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 {}; 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); definition let a,b,c,d,e,f,g,h be set; func NOR8(a,b,c,d,e,f,g,h) -> set equals :: GATE_1:def 33 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 {}; 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); 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:40 for c1,x1,x2,x3,x4,y1,y2,y3,y4,c2,c3,c4,c5,n1,n2,n3,n4,n,c5b being 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); ::Definition of mod 2 adder used in 'Carry Look Ahead Adder' definition let a,b be set; func MODADD2(a,b) -> set equals :: GATE_1:def 34 NOT1 {} if (a is non empty or b is non empty) & not(a is non empty & b is non empty) otherwise {}; 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); ::The following two definitions are for normal 1 bit adder. 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)); end; 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)); 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) -> set equals :: GATE_1:def 37 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) -> set equals :: GATE_1:def 38 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) -> set equals :: GATE_1:def 39 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) -> set equals :: GATE_1:def 40 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: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 (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);