:: Logic Gates and Logical Equivalence of Adders
:: by Yatsuka Nakamura
::
:: Received February 4, 1999
:: Copyright (c) 1999-2026 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
: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
NOT1 {{}} = {} & NOT1 {} = {{}} by Def1;
theorem
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
NOT1 {} is non empty;
definition
let a,b be set;
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
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
: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
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
: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
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
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
XOR2(a,{}) is non empty iff a is non empty;
theorem
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
: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
EQV2(a, b) is non empty iff (a is non empty iff b is non empty);
theorem
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;
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
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
: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
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
: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
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
: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
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
: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
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
: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
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
:Def12:
NOT1 {} if not (a is non empty & b is non
empty & c is non empty) otherwise {};
correctness;
end;
theorem
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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 :: 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
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)
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 of mod 2 adder used in 'Carry Look Ahead Adder'
definition
let a,b be set;
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
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;
::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
XOR3(a2,b2,CARR1(a1,b1,c));
coherence;
end;
definition
let a1,b1,a2,b2,c be set;
func CARR2(a2,b2,a1,b1,c) -> set equals
MAJ3(a2,b2,CARR1(a1,b1,c));
coherence;
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
XOR3(a3,b3,CARR2(a2,b2,a1,b1,c));
coherence;
end;
definition
let a1,b1,a2,b2,a3,b3,c be set;
func CARR3(a3,b3,a2,b2,a1,b1,c) -> set equals
MAJ3(a3,b3,CARR2(a2,b2,a1,b1,c));
coherence;
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
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;
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;
::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
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)
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;