:: Logic Gates and Logical Equivalence of Adders
:: by Yatsuka Nakamura
::
:: Received February 4, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users

begin

theorem :: GATE_1:1

canceled;

theorem :: GATE_1:2

canceled;

definition

let a be set ;
func NOT1 a -> set equals :Def1: :: GATE_1:def 1
{} if not a is empty
otherwise {{}};
correctness
coherence
( ( not a is empty implies {} is set ) & ( a is empty implies {{}} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def1 defines NOT1 GATE_1:def 1 :
for a being set holds
( ( not a is empty implies NOT1 a = {} ) & ( a is empty implies NOT1 a = {{}} ) );

registration

let a be empty set ;
cluster NOT1 a -> non empty ;
coherence
not NOT1 a is empty by Def1;

end;

registration

let a be non empty set ;
cluster NOT1 a -> empty ;
coherence
NOT1 a is empty by Def1;

end;

theorem :: GATE_1:3

( NOT1 {{}} = {} & NOT1 {} = {{}} ) by Def1;

theorem :: GATE_1:4

for a being set holds
( not NOT1 a is empty iff a is empty ) ;

theorem :: GATE_1:5

not NOT1 {} is empty ;

definition

let a, b be set ;
func AND2 (a,b) -> set equals :Def2: :: GATE_1:def 2
NOT1 {} if ( not a is empty & not b is empty )
otherwise {} ;
correctness
coherence
( ( not a is empty & not b is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;
commutativity
for b₁ being set
for a, b being set st ( not a is empty & not b is empty implies b₁ = NOT1 {} ) & ( ( a is empty or b is empty ) implies b₁ = {} ) holds
( ( not b is empty & not a is empty implies b₁ = NOT1 {} ) & ( ( b is empty or a is empty ) implies b₁ = {} ) ) ;

end;

:: deftheorem Def2 defines AND2 GATE_1:def 2 :
for a, b being set holds
( ( not a is empty & not b is empty implies AND2 (a,b) = NOT1 {} ) & ( ( a is empty or b is empty ) implies AND2 (a,b) = {} ) );

registration

let a, b be non empty set ;
cluster AND2 (a,b) -> non empty ;
coherence
not AND2 (a,b) is empty by Def2;

end;

registration

let a be empty set ;
let b be set ;
cluster AND2 (a,b) -> empty ;
coherence
AND2 (a,b) is empty by Def2;

end;

theorem :: GATE_1:6

for a, b being set holds
( not AND2 (a,b) is empty iff ( not a is empty & not b is empty ) ) ;

definition

let a, b be set ;
func OR2 (a,b) -> set equals :Def3: :: GATE_1:def 3
NOT1 {} if ( not a is empty or not b is empty )
otherwise {} ;
correctness
coherence
( ( ( not a is empty or not b is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or {} is set ) );
consistency
for b₁ being set holds verum;
;
commutativity
for b₁ being set
for a, b being set st ( ( not a is empty or not b is empty ) implies b₁ = NOT1 {} ) & ( not a is empty or not b is empty or b₁ = {} ) holds
( ( ( not b is empty or not a is empty ) implies b₁ = NOT1 {} ) & ( not b is empty or not a is empty or b₁ = {} ) ) ;

end;

:: deftheorem Def3 defines OR2 GATE_1:def 3 :
for a, b being set holds
( ( ( not a is empty or not b is empty ) implies OR2 (a,b) = NOT1 {} ) & ( not a is empty or not b is empty or OR2 (a,b) = {} ) );

registration

let a be set ;
let b be non empty set ;
cluster OR2 (a,b) -> non empty ;
coherence
not OR2 (a,b) is empty by Def3;

end;

registration

let a, b be empty set ;
cluster OR2 (a,b) -> empty ;
coherence
OR2 (a,b) is empty by Def3;

end;

theorem :: GATE_1:7

for a, b being set holds
( ( not a is empty or not b is empty ) iff not OR2 (a,b) is empty ) ;

definition

let a, b be set ;
func XOR2 (a,b) -> set equals :Def4: :: GATE_1:def 4
NOT1 {} if ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) )
otherwise {} ;
correctness
coherence
( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies NOT1 {} is set ) & ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) or {} is set ) );
consistency
for b₁ being set holds verum;
;
commutativity
for b₁ being set
for a, b being set st ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies b₁ = NOT1 {} ) & ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) or b₁ = {} ) holds
( ( ( ( not b is empty & a is empty ) or ( b is empty & not a is empty ) ) implies b₁ = NOT1 {} ) & ( ( not b is empty & a is empty ) or ( b is empty & not a is empty ) or b₁ = {} ) ) ;

end;

:: deftheorem Def4 defines XOR2 GATE_1:def 4 :
for a, b being set holds
( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies XOR2 (a,b) = NOT1 {} ) & ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) or XOR2 (a,b) = {} ) );

registration

let a be empty set ;
let b be non empty set ;
cluster XOR2 (a,b) -> non empty ;
coherence
not XOR2 (a,b) is empty by Def4;

end;

registration

let a, b be empty set ;
cluster XOR2 (a,b) -> empty ;
coherence
XOR2 (a,b) is empty by Def4;

end;

registration

let a, b be non empty set ;
cluster XOR2 (a,b) -> empty ;
coherence
XOR2 (a,b) is empty by Def4;

end;

theorem :: GATE_1:8

for a, b being set holds
( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) iff not XOR2 (a,b) is empty ) ;

theorem :: GATE_1:9

for a being set holds XOR2 (a,a) is empty

proof end;

theorem :: GATE_1:10

for a being set holds
( not XOR2 (a,{}) is empty iff not a is empty ) ;

theorem :: GATE_1:11

for a, b being set holds
( not XOR2 (a,b) is empty iff not XOR2 (b,a) is empty ) ;

definition

let a, b be set ;
func EQV2 (a,b) -> set equals :Def5: :: GATE_1:def 5
NOT1 {} if ( not a is empty iff not b is empty )
otherwise {} ;
correctness
coherence
( not ( ( not a is empty implies not b is empty ) & ( not b is empty implies not a is empty ) & NOT1 {} is not set ) & ( ( ( not a is empty & b is empty ) or ( not b is empty & a is empty ) ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;
commutativity
for b₁ being set
for a, b being set st not ( ( not a is empty implies not b is empty ) & ( not b is empty implies not a is empty ) & not b₁ = NOT1 {} ) & ( ( ( not a is empty & b is empty ) or ( not b is empty & a is empty ) ) implies b₁ = {} ) holds
( not ( ( not b is empty implies not a is empty ) & ( not a is empty implies not b is empty ) & not b₁ = NOT1 {} ) & ( ( ( not b is empty & a is empty ) or ( not a is empty & b is empty ) ) implies b₁ = {} ) ) ;

end;

:: deftheorem Def5 defines EQV2 GATE_1:def 5 :
for a, b being set holds
( not ( ( not a is empty implies not b is empty ) & ( not b is empty implies not a is empty ) & not EQV2 (a,b) = NOT1 {} ) & ( ( ( not a is empty & b is empty ) or ( not b is empty & a is empty ) ) implies EQV2 (a,b) = {} ) );

registration

let a be empty set ;
let b be non empty set ;
cluster EQV2 (a,b) -> empty ;
coherence
EQV2 (a,b) is empty by Def5;

end;

registration

let a, b be empty set ;
cluster EQV2 (a,b) -> non empty ;
coherence
not EQV2 (a,b) is empty by Def5;

end;

registration

let a, b be non empty set ;
cluster EQV2 (a,b) -> non empty ;
coherence
not EQV2 (a,b) is empty by Def5;

end;

theorem :: GATE_1:12

for a, b being set holds
( not EQV2 (a,b) is empty iff ( not a is empty iff not b is empty ) ) ;

theorem :: GATE_1:13

for a, b being set holds
( not EQV2 (a,b) is empty iff XOR2 (a,b) is empty )

proof end;

definition

let a, b be set ;
func NAND2 (a,b) -> set equals :Def6: :: GATE_1:def 6
NOT1 {} if ( a is empty or b is empty )
otherwise {} ;
correctness
coherence
( ( ( a is empty or b is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty implies {} is set ) );
consistency
for b₁ being set holds verum;
;
commutativity
for b₁ being set
for a, b being set st ( ( a is empty or b is empty ) implies b₁ = NOT1 {} ) & ( not a is empty & not b is empty implies b₁ = {} ) holds
( ( ( b is empty or a is empty ) implies b₁ = NOT1 {} ) & ( not b is empty & not a is empty implies b₁ = {} ) ) ;

end;

:: deftheorem Def6 defines NAND2 GATE_1:def 6 :
for a, b being set holds
( ( ( a is empty or b is empty ) implies NAND2 (a,b) = NOT1 {} ) & ( not a is empty & not b is empty implies NAND2 (a,b) = {} ) );

registration

let a be empty set ;
let b be set ;
cluster NAND2 (a,b) -> non empty ;
coherence
not NAND2 (a,b) is empty by Def6;

end;

registration

let a, b be non empty set ;
cluster NAND2 (a,b) -> empty ;
coherence
NAND2 (a,b) is empty by Def6;

end;

theorem :: GATE_1:14

for a, b being set holds
( not NAND2 (a,b) is empty & not a is empty iff b is empty ) ;

definition

let a, b be set ;
func NOR2 (a,b) -> set equals :Def7: :: GATE_1:def 7
NOT1 {} if ( a is empty & b is empty )
otherwise {} ;
correctness
coherence
( ( not a is empty or not b is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;
commutativity
for b₁ being set
for a, b being set st ( not a is empty or not b is empty or b₁ = NOT1 {} ) & ( ( not a is empty or not b is empty ) implies b₁ = {} ) holds
( ( not b is empty or not a is empty or b₁ = NOT1 {} ) & ( ( not b is empty or not a is empty ) implies b₁ = {} ) ) ;

end;

:: deftheorem Def7 defines NOR2 GATE_1:def 7 :
for a, b being set holds
( ( not a is empty or not b is empty or NOR2 (a,b) = NOT1 {} ) & ( ( not a is empty or not b is empty ) implies NOR2 (a,b) = {} ) );

registration

let a, b be empty set ;
cluster NOR2 (a,b) -> non empty ;
coherence
not NOR2 (a,b) is empty by Def7;

end;

registration

let a be non empty set ;
let b be set ;
cluster NOR2 (a,b) -> empty ;
coherence
NOR2 (a,b) is empty by Def7;

end;

theorem :: GATE_1:15

for a, b being set holds
( not NOR2 (a,b) is empty iff ( a is empty & b is empty ) ) ;

definition

let a, b, c be set ;
func AND3 (a,b,c) -> set equals :Def8: :: GATE_1:def 8
NOT1 {} if ( not a is empty & not b is empty & not c is empty )
otherwise {} ;
correctness
coherence
( ( not a is empty & not b is empty & not c is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def8 defines AND3 GATE_1:def 8 :
for a, b, c being set holds
( ( not a is empty & not b is empty & not c is empty implies AND3 (a,b,c) = NOT1 {} ) & ( ( a is empty or b is empty or c is empty ) implies AND3 (a,b,c) = {} ) );

registration

let a, b, c be non empty set ;
cluster AND3 (a,b,c) -> non empty ;
coherence
not AND3 (a,b,c) is empty by Def8;

end;

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

for a, b, c being set holds
( not AND3 (a,b,c) is empty iff ( not a is empty & not b is empty & not c is empty ) ) ;

definition

let a, b, c be set ;
func OR3 (a,b,c) -> set equals :Def9: :: GATE_1:def 9
NOT1 {} if ( not a is empty or not b is empty or not c is empty )
otherwise {} ;
correctness
coherence
( ( ( not a is empty or not b is empty or not c is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def9 defines OR3 GATE_1:def 9 :
for a, b, c being set holds
( ( ( not a is empty or not b is empty or not c is empty ) implies OR3 (a,b,c) = NOT1 {} ) & ( not a is empty or not b is empty or not c is empty or OR3 (a,b,c) = {} ) );

registration

let a, b, c be empty set ;
cluster OR3 (a,b,c) -> empty ;
coherence
OR3 (a,b,c) is empty by Def9;

end;

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

for a, b, c being set holds
( ( not a is empty or not b is empty or not c is empty ) iff not OR3 (a,b,c) is empty ) ;

definition

let a, b, c be set ;
func XOR3 (a,b,c) -> set equals :Def10: :: GATE_1:def 10
NOT1 {} if ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) )
otherwise {} ;
correctness
coherence
( ( ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) ) implies NOT1 {} is set ) & ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) or {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def10 defines XOR3 GATE_1:def 10 :
for a, b, c being set holds
( ( ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) ) implies XOR3 (a,b,c) = NOT1 {} ) & ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) or XOR3 (a,b,c) = {} ) );

registration

let a, b, c be empty set ;
cluster XOR3 (a,b,c) -> empty ;
coherence
XOR3 (a,b,c) is empty by Def10;

end;

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;

registration

let a, b, c be non empty set ;
cluster XOR3 (a,b,c) -> non empty ;
coherence
not XOR3 (a,b,c) is empty by Def10;

end;

theorem :: GATE_1:18

for a, b, c being set holds
( ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) ) iff not XOR3 (a,b,c) is empty ) ;

definition

let a, b, c be set ;
func MAJ3 (a,b,c) -> set equals :Def11: :: GATE_1:def 11
NOT1 {} if ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) )
otherwise {} ;
correctness
coherence
( ( ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) ) implies NOT1 {} is set ) & ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) or {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def11 defines MAJ3 GATE_1:def 11 :
for a, b, c being set holds
( ( ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) ) implies MAJ3 (a,b,c) = NOT1 {} ) & ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) or MAJ3 (a,b,c) = {} ) );

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

for a, b, c being set holds
( ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) ) iff not MAJ3 (a,b,c) is empty ) ;

definition

let a, b, c be set ;
func NAND3 (a,b,c) -> set equals :Def12: :: GATE_1:def 12
NOT1 {} if ( a is empty or b is empty or c is empty )
otherwise {} ;
correctness
coherence
( ( ( a is empty or b is empty or c is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty implies {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def12 defines NAND3 GATE_1:def 12 :
for a, b, c being set holds
( ( ( a is empty or b is empty or c is empty ) implies NAND3 (a,b,c) = NOT1 {} ) & ( not a is empty & not b is empty & not c is empty implies NAND3 (a,b,c) = {} ) );

theorem :: GATE_1:20

for a, b, c being set holds
( not NAND3 (a,b,c) is empty & not a is empty & not b is empty iff c is empty ) by Def12;

definition

let a, b, c be set ;
func NOR3 (a,b,c) -> set equals :Def13: :: GATE_1:def 13
NOT1 {} if ( a is empty & b is empty & c is empty )
otherwise {} ;
correctness
coherence
( ( not a is empty or not b is empty or not c is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def13 defines NOR3 GATE_1:def 13 :
for a, b, c being set holds
( ( not a is empty or not b is empty or not c is empty or NOR3 (a,b,c) = NOT1 {} ) & ( ( not a is empty or not b is empty or not c is empty ) implies NOR3 (a,b,c) = {} ) );

theorem :: GATE_1:21

for a, b, c being set holds
( not NOR3 (a,b,c) is empty iff ( a is empty & b is empty & c is empty ) ) by Def13;

definition

let a, b, c, d be set ;
func AND4 (a,b,c,d) -> set equals :Def14: :: GATE_1:def 14
NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty )
otherwise {} ;
correctness
coherence
( ( not a is empty & not b is empty & not c is empty & not d is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def14 defines AND4 GATE_1:def 14 :
for a, b, c, d being set holds
( ( not a is empty & not b is empty & not c is empty & not d is empty implies AND4 (a,b,c,d) = NOT1 {} ) & ( ( a is empty or b is empty or c is empty or d is empty ) implies AND4 (a,b,c,d) = {} ) );

theorem :: GATE_1:22

for a, b, c, d being set holds
( not AND4 (a,b,c,d) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty ) ) by Def14;

definition

let a, b, c, d be set ;
func OR4 (a,b,c,d) -> set equals :Def15: :: GATE_1:def 15
NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty )
otherwise {} ;
correctness
coherence
( ( ( not a is empty or not b is empty or not c is empty or not d 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 {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def15 defines OR4 GATE_1:def 15 :
for a, b, c, d being set holds
( ( ( not a is empty or not b is empty or not c is empty or not d is empty ) implies OR4 (a,b,c,d) = NOT1 {} ) & ( not a is empty or not b is empty or not c is empty or not d is empty or OR4 (a,b,c,d) = {} ) );

theorem :: GATE_1:23

for a, b, c, d being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty ) iff not OR4 (a,b,c,d) is empty ) by Def15;

definition

let a, b, c, d be set ;
func NAND4 (a,b,c,d) -> set equals :Def16: :: GATE_1:def 16
NOT1 {} if ( a is empty or b is empty or c is empty or d is empty )
otherwise {} ;
correctness
coherence
( ( ( a is empty or b is empty or c is empty or d is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty implies {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def16 defines NAND4 GATE_1:def 16 :
for a, b, c, d being set holds
( ( ( a is empty or b is empty or c is empty or d is empty ) implies NAND4 (a,b,c,d) = NOT1 {} ) & ( not a is empty & not b is empty & not c is empty & not d is empty implies NAND4 (a,b,c,d) = {} ) );

theorem :: GATE_1:24

for a, b, c, d being set holds
( not NAND4 (a,b,c,d) is empty & not a is empty & not b is empty & not c is empty iff d is empty ) by Def16;

definition

let a, b, c, d be set ;
func NOR4 (a,b,c,d) -> set equals :Def17: :: GATE_1:def 17
NOT1 {} if ( a is empty & b is empty & c is empty & d 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 NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem Def17 defines NOR4 GATE_1:def 17 :
for a, b, c, d being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or NOR4 (a,b,c,d) = NOT1 {} ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty ) implies NOR4 (a,b,c,d) = {} ) );

theorem :: GATE_1:25

for a, b, c, d being set holds
( not NOR4 (a,b,c,d) is empty iff ( a is empty & b is empty & c is empty & d is empty ) ) by Def17;

definition

let a, b, c, d, e be set ;
func AND5 (a,b,c,d,e) -> set equals :Def18: :: GATE_1:def 18
NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e 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 implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

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

for a, b, c, d, e being set holds
( not AND5 (a,b,c,d,e) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty ) ) by Def18;

definition

let a, b, c, d, e be set ;
func OR5 (a,b,c,d,e) -> set equals :Def19: :: GATE_1:def 19
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 )
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 ) 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 {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

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

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 ) iff not OR5 (a,b,c,d,e) is empty ) by Def19;

definition

let a, b, c, d, e be set ;
func NAND5 (a,b,c,d,e) -> set equals :Def20: :: GATE_1:def 20
NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty )
otherwise {} ;
correctness
coherence
( ( ( a is empty or b is empty or c is empty or d is empty or e 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 implies {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

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

for a, b, c, d, e being set holds
( not NAND5 (a,b,c,d,e) is empty & not a is empty & not b is empty & not c is empty & not d is empty iff e is empty ) by Def20;

definition

let a, b, c, d, e be set ;
func NOR5 (a,b,c,d,e) -> set equals :Def21: :: GATE_1:def 21
NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e 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 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 ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;

end;

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

for a, b, c, d, e being set holds
( not NOR5 (a,b,c,d,e) is empty iff ( a is empty & b is empty & c is empty & d is empty & e is empty ) ) by Def21;

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 b₁ 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 b₁ 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 b₁ 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 b₁ 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 b₁ 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 b₁ 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 b₁ 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 b₁ 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 b₁ 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 b₁ 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 b₁ 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 b₁ 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;

begin

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 )

proof end;

definition

let a, b be set ;
func MODADD2 (a,b) -> set equals :Def34: :: GATE_1:def 34
NOT1 {} if ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) )
otherwise {} ;
correctness
coherence
( ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) implies NOT1 {} is set ) & ( ( ( a is empty & b is empty ) or ( not a is empty & not b is empty ) ) implies {} is set ) );
consistency
for b₁ being set holds verum;
;
commutativity
for b₁ being set
for a, b being set st ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) implies b₁ = NOT1 {} ) & ( ( ( a is empty & b is empty ) or ( not a is empty & not b is empty ) ) implies b₁ = {} ) holds
( ( ( not b is empty or not a is empty ) & ( b is empty or a is empty ) implies b₁ = NOT1 {} ) & ( ( ( b is empty & a is empty ) or ( not b is empty & not a is empty ) ) implies b₁ = {} ) ) ;

end;

:: deftheorem Def34 defines MODADD2 GATE_1:def 34 :
for a, b being set holds
( ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) implies MODADD2 (a,b) = NOT1 {} ) & ( ( ( a is empty & b is empty ) or ( not a is empty & not b is empty ) ) implies MODADD2 (a,b) = {} ) );

theorem :: GATE_1:43

for a, b being set holds
( not MODADD2 (a,b) is empty iff ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) ) ) by Def34;

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

proof end;