:: Logic Gates and Logical Equivalence of Adders
:: by Yatsuka Nakamura
::
:: Received February 4, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: GATE_1:1
canceled;
theorem :: GATE_1:2
canceled;
:: deftheorem Def1 defines NOT1 GATE_1:def 1 :
theorem :: GATE_1:3
theorem :: GATE_1:4
theorem :: GATE_1:5
:: deftheorem Def2 defines AND2 GATE_1:def 2 :
theorem :: GATE_1:6
:: deftheorem Def3 defines OR2 GATE_1:def 3 :
theorem :: GATE_1:7
:: deftheorem Def4 defines XOR2 GATE_1:def 4 :
theorem :: GATE_1:8
theorem :: GATE_1:9
theorem :: GATE_1:10
theorem :: GATE_1:11
:: deftheorem Def5 defines EQV2 GATE_1:def 5 :
theorem :: GATE_1:12
theorem :: GATE_1:13
:: deftheorem Def6 defines NAND2 GATE_1:def 6 :
theorem :: GATE_1:14
:: deftheorem Def7 defines NOR2 GATE_1:def 7 :
theorem :: GATE_1:15
:: deftheorem Def8 defines AND3 GATE_1:def 8 :
registration
let a be
empty set ;
let b,
c be
set ;
cluster AND3 a,
b,
c -> empty ;
coherence
AND3 a,b,c is empty
by Def8;
cluster AND3 b,
a,
c -> empty ;
coherence
AND3 b,a,c is empty
by Def8;
cluster AND3 b,
c,
a -> empty ;
coherence
AND3 b,c,a is empty
by Def8;
end;
theorem :: GATE_1:16
:: deftheorem Def9 defines OR3 GATE_1:def 9 :
registration
let a be non
empty set ;
let b,
c be
set ;
cluster OR3 a,
b,
c -> non
empty ;
coherence
not OR3 a,b,c is empty
by Def9;
cluster OR3 b,
a,
c -> non
empty ;
coherence
not OR3 b,a,c is empty
by Def9;
cluster OR3 b,
c,
a -> non
empty ;
coherence
not OR3 b,c,a is empty
by Def9;
end;
theorem :: GATE_1:17
:: deftheorem Def10 defines XOR3 GATE_1:def 10 :
registration
let a,
b be
empty set ;
let c be non
empty set ;
cluster XOR3 a,
b,
c -> non
empty ;
coherence
not XOR3 a,b,c is empty
by Def10;
cluster XOR3 a,
c,
b -> non
empty ;
coherence
not XOR3 a,c,b is empty
by Def10;
cluster XOR3 c,
a,
b -> non
empty ;
coherence
not XOR3 c,a,b is empty
by Def10;
end;
registration
let a,
b be non
empty set ;
let c be
empty set ;
cluster XOR3 a,
b,
c -> empty ;
coherence
XOR3 a,b,c is empty
by Def10;
cluster XOR3 a,
c,
b -> empty ;
coherence
XOR3 a,c,b is empty
by Def10;
cluster XOR3 c,
a,
b -> empty ;
coherence
XOR3 c,a,b is empty
by Def10;
end;
theorem :: GATE_1:18
:: 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
not MAJ3 a,b,c is empty
by Def11;
cluster MAJ3 a,
c,
b -> non
empty ;
coherence
not MAJ3 a,c,b is empty
by Def11;
cluster MAJ3 c,
a,
b -> non
empty ;
coherence
not MAJ3 c,a,b is empty
by Def11;
end;
registration
let a,
b be
empty set ;
let c be
set ;
cluster MAJ3 a,
b,
c -> empty ;
coherence
MAJ3 a,b,c is empty
by Def11;
cluster MAJ3 a,
c,
b -> empty ;
coherence
MAJ3 a,c,b is empty
by Def11;
cluster MAJ3 c,
a,
b -> empty ;
coherence
MAJ3 c,a,b is empty
by Def11;
end;
theorem :: GATE_1:19
:: deftheorem Def12 defines NAND3 GATE_1:def 12 :
theorem :: GATE_1:20
:: deftheorem Def13 defines NOR3 GATE_1:def 13 :
theorem :: GATE_1:21
:: deftheorem Def14 defines AND4 GATE_1:def 14 :
theorem :: GATE_1:22
:: deftheorem Def15 defines OR4 GATE_1:def 15 :
theorem :: GATE_1:23
:: deftheorem Def16 defines NAND4 GATE_1:def 16 :
theorem :: GATE_1:24
:: deftheorem Def17 defines NOR4 GATE_1:def 17 :
theorem :: GATE_1:25
:: deftheorem Def18 defines AND5 GATE_1:def 18 :
for
a,
b,
c,
d,
e being
set holds
( ( not
a is
empty & not
b is
empty & not
c is
empty & not
d is
empty & not
e is
empty implies
AND5 a,
b,
c,
d,
e = NOT1 {} ) & ( (
a is
empty or
b is
empty or
c is
empty or
d is
empty or
e is
empty ) implies
AND5 a,
b,
c,
d,
e = {} ) );
theorem :: GATE_1:26
:: deftheorem Def19 defines OR5 GATE_1:def 19 :
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 ) implies
OR5 a,
b,
c,
d,
e = NOT1 {} ) & ( 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
OR5 a,
b,
c,
d,
e = {} ) );
theorem :: GATE_1:27
:: deftheorem Def20 defines NAND5 GATE_1:def 20 :
for
a,
b,
c,
d,
e being
set holds
( ( (
a is
empty or
b is
empty or
c is
empty or
d is
empty or
e is
empty ) implies
NAND5 a,
b,
c,
d,
e = NOT1 {} ) & ( not
a is
empty & not
b is
empty & not
c is
empty & not
d is
empty & not
e is
empty implies
NAND5 a,
b,
c,
d,
e = {} ) );
theorem :: GATE_1:28
:: deftheorem Def21 defines NOR5 GATE_1:def 21 :
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 or
NOR5 a,
b,
c,
d,
e = NOT1 {} ) & ( ( not
a is
empty or not
b is
empty or not
c is
empty or not
d is
empty or not
e is
empty ) implies
NOR5 a,
b,
c,
d,
e = {} ) );
theorem :: GATE_1:29
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
coherence
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def22 defines AND6 GATE_1:def 22 :
for
a,
b,
c,
d,
e,
f being
set holds
( ( not
a is
empty & not
b is
empty & not
c is
empty & not
d is
empty & not
e is
empty & not
f is
empty implies
AND6 a,
b,
c,
d,
e,
f = NOT1 {} ) & ( (
a is
empty or
b is
empty or
c is
empty or
d is
empty or
e is
empty or
f is
empty ) implies
AND6 a,
b,
c,
d,
e,
f = {} ) );
theorem :: GATE_1:30
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
coherence
( ( ( 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 ) implies NOT1 {} is set ) & ( 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 {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def23 defines OR6 GATE_1:def 23 :
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 ) implies
OR6 a,
b,
c,
d,
e,
f = NOT1 {} ) & ( 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
OR6 a,
b,
c,
d,
e,
f = {} ) );
theorem :: GATE_1:31
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
coherence
( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def24 defines NAND6 GATE_1:def 24 :
for
a,
b,
c,
d,
e,
f being
set holds
( ( (
a is
empty or
b is
empty or
c is
empty or
d is
empty or
e is
empty or
f is
empty ) implies
NAND6 a,
b,
c,
d,
e,
f = NOT1 {} ) & ( not
a is
empty & not
b is
empty & not
c is
empty & not
d is
empty & not
e is
empty & not
f is
empty implies
NAND6 a,
b,
c,
d,
e,
f = {} ) );
theorem :: GATE_1:32
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
coherence
( ( 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 NOT1 {} is set ) & ( ( 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 ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def25 defines NOR6 GATE_1:def 25 :
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 or
NOR6 a,
b,
c,
d,
e,
f = NOT1 {} ) & ( ( 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 ) implies
NOR6 a,
b,
c,
d,
e,
f = {} ) );
theorem :: GATE_1:33
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
coherence
( ( 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 implies NOT1 {} is set ) & ( ( 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 ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def26 defines AND7 GATE_1:def 26 :
for
a,
b,
c,
d,
e,
f,
g being
set holds
( ( 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 implies
AND7 a,
b,
c,
d,
e,
f,
g = NOT1 {} ) & ( (
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 ) implies
AND7 a,
b,
c,
d,
e,
f,
g = {} ) );
theorem :: GATE_1:34
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
coherence
( ( ( 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 ) implies NOT1 {} is set ) & ( 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 {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def27 defines OR7 GATE_1:def 27 :
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 ) implies
OR7 a,
b,
c,
d,
e,
f,
g = NOT1 {} ) & ( 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
OR7 a,
b,
c,
d,
e,
f,
g = {} ) );
theorem :: GATE_1:35
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
coherence
( ( ( 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 ) implies NOT1 {} is set ) & ( 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 implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def28 defines NAND7 GATE_1:def 28 :
for
a,
b,
c,
d,
e,
f,
g being
set holds
( ( (
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 ) implies
NAND7 a,
b,
c,
d,
e,
f,
g = NOT1 {} ) & ( 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 implies
NAND7 a,
b,
c,
d,
e,
f,
g = {} ) );
theorem :: GATE_1:36
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
coherence
( ( 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 NOT1 {} is set ) & ( ( 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 ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def29 defines NOR7 GATE_1:def 29 :
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 or
NOR7 a,
b,
c,
d,
e,
f,
g = NOT1 {} ) & ( ( 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 ) implies
NOR7 a,
b,
c,
d,
e,
f,
g = {} ) );
theorem :: GATE_1:37
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
coherence
( ( 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 implies NOT1 {} is set ) & ( ( 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 ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def30 defines AND8 GATE_1:def 30 :
for
a,
b,
c,
d,
e,
f,
g,
h being
set holds
( ( 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 implies
AND8 a,
b,
c,
d,
e,
f,
g,
h = NOT1 {} ) & ( (
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 ) implies
AND8 a,
b,
c,
d,
e,
f,
g,
h = {} ) );
theorem :: GATE_1:38
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
coherence
( ( ( 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 ) implies NOT1 {} is set ) & ( 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 or {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def31 defines OR8 GATE_1:def 31 :
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 ) implies
OR8 a,
b,
c,
d,
e,
f,
g,
h = NOT1 {} ) & ( 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 or
OR8 a,
b,
c,
d,
e,
f,
g,
h = {} ) );
theorem :: GATE_1:39
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
coherence
( ( ( 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 ) implies NOT1 {} is set ) & ( 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 implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def32 defines NAND8 GATE_1:def 32 :
for
a,
b,
c,
d,
e,
f,
g,
h being
set holds
( ( (
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 ) implies
NAND8 a,
b,
c,
d,
e,
f,
g,
h = NOT1 {} ) & ( 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 implies
NAND8 a,
b,
c,
d,
e,
f,
g,
h = {} ) );
theorem :: GATE_1:40
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
coherence
( ( 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 or NOT1 {} is set ) & ( ( 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 ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def33 defines NOR8 GATE_1:def 33 :
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 or
NOR8 a,
b,
c,
d,
e,
f,
g,
h = NOT1 {} ) & ( ( 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 ) implies
NOR8 a,
b,
c,
d,
e,
f,
g,
h = {} ) );
theorem :: GATE_1:41
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;
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 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 )
:: deftheorem Def34 defines MODADD2 GATE_1:def 34 :
theorem :: GATE_1:43
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;
definition
let a1,
b1,
a2,
b2,
c be
set ;
canceled;canceled;func ADD2 a2,
b2,
a1,
b1,
c -> set equals :: GATE_1:def 37
XOR3 a2,
b2,
(CARR1 a1,b1,c);
coherence
XOR3 a2,b2,(CARR1 a1,b1,c) is set
;
end;
:: deftheorem GATE_1:def 35 :
canceled;
:: deftheorem GATE_1:def 36 :
canceled;
:: deftheorem defines ADD2 GATE_1:def 37 :
for
a1,
b1,
a2,
b2,
c being
set holds
ADD2 a2,
b2,
a1,
b1,
c = XOR3 a2,
b2,
(CARR1 a1,b1,c);
definition
let a1,
b1,
a2,
b2,
c be
set ;
func CARR2 a2,
b2,
a1,
b1,
c -> set equals :: GATE_1:def 38
MAJ3 a2,
b2,
(CARR1 a1,b1,c);
coherence
MAJ3 a2,b2,(CARR1 a1,b1,c) is set
;
end;
:: deftheorem defines CARR2 GATE_1:def 38 :
for
a1,
b1,
a2,
b2,
c being
set holds
CARR2 a2,
b2,
a1,
b1,
c = MAJ3 a2,
b2,
(CARR1 a1,b1,c);
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 39
XOR3 a3,
b3,
(CARR2 a2,b2,a1,b1,c);
coherence
XOR3 a3,b3,(CARR2 a2,b2,a1,b1,c) is set
;
end;
:: deftheorem defines ADD3 GATE_1:def 39 :
for
a1,
b1,
a2,
b2,
a3,
b3,
c being
set holds
ADD3 a3,
b3,
a2,
b2,
a1,
b1,
c = XOR3 a3,
b3,
(CARR2 a2,b2,a1,b1,c);
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 40
MAJ3 a3,
b3,
(CARR2 a2,b2,a1,b1,c);
coherence
MAJ3 a3,b3,(CARR2 a2,b2,a1,b1,c) is set
;
end;
:: deftheorem defines CARR3 GATE_1:def 40 :
for
a1,
b1,
a2,
b2,
a3,
b3,
c being
set holds
CARR3 a3,
b3,
a2,
b2,
a1,
b1,
c = MAJ3 a3,
b3,
(CARR2 a2,b2,a1,b1,c);
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 41
XOR3 a4,
b4,
(CARR3 a3,b3,a2,b2,a1,b1,c);
coherence
XOR3 a4,b4,(CARR3 a3,b3,a2,b2,a1,b1,c) is set
;
end;
:: deftheorem defines ADD4 GATE_1:def 41 :
for
a1,
b1,
a2,
b2,
a3,
b3,
a4,
b4,
c being
set holds
ADD4 a4,
b4,
a3,
b3,
a2,
b2,
a1,
b1,
c = XOR3 a4,
b4,
(CARR3 a3,b3,a2,b2,a1,b1,c);
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 42
MAJ3 a4,
b4,
(CARR3 a3,b3,a2,b2,a1,b1,c);
coherence
MAJ3 a4,b4,(CARR3 a3,b3,a2,b2,a1,b1,c) is set
;
end;
:: deftheorem defines CARR4 GATE_1:def 42 :
for
a1,
b1,
a2,
b2,
a3,
b3,
a4,
b4,
c being
set holds
CARR4 a4,
b4,
a3,
b3,
a2,
b2,
a1,
b1,
c = MAJ3 a4,
b4,
(CARR3 a3,b3,a2,b2,a1,b1,c);
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
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 ) ) )