:: Logic Gates and Logical Equivalence of Adders
:: by Yatsuka Nakamura
::
:: Copyright (c) 1999-2021 Association of Mizar Users

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

theorem :: GATE_1:2
for a being set holds
( not NOT1 a is empty iff a is empty ) ;

theorem :: GATE_1:3
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 b1 being set holds verum
;
;
commutativity
for b1, a, b being set st ( not a is empty & not b is empty implies b1 = NOT1 {} ) & ( ( a is empty or b is empty ) implies b1 = {} ) holds
( ( not b is empty & not a is empty implies b1 = NOT1 {} ) & ( ( b is empty or a is empty ) implies b1 = {} ) )
;
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:4
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 b1 being set holds verum
;
;
commutativity
for b1, a, b being set st ( ( not a is empty or not b is empty ) implies b1 = NOT1 {} ) & ( not a is empty or not b is empty or b1 = {} ) holds
( ( ( not b is empty or not a is empty ) implies b1 = NOT1 {} ) & ( not b is empty or not a is empty or b1 = {} ) )
;
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:5
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 b1 being set holds verum
;
;
commutativity
for b1, a, b being set st ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies b1 = NOT1 {} ) & ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) or b1 = {} ) holds
( ( ( ( not b is empty & a is empty ) or ( b is empty & not a is empty ) ) implies b1 = NOT1 {} ) & ( ( not b is empty & a is empty ) or ( b is empty & not a is empty ) or b1 = {} ) )
;
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:6
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:7
for a being set holds XOR2 (a,a) is empty
proof end;

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

theorem :: GATE_1:9
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 b1 being set holds verum
;
;
commutativity
for b1, 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 b1 = NOT1 {} ) & ( ( ( not a is empty & b is empty ) or ( not b is empty & a is empty ) ) implies b1 = {} ) holds
( not ( ( not b is empty implies not a is empty ) & ( not a is empty implies not b is empty ) & not b1 = NOT1 {} ) & ( ( ( not b is empty & a is empty ) or ( not a is empty & b is empty ) ) implies b1 = {} ) )
;
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:10
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:11
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 b1 being set holds verum
;
;
commutativity
for b1, a, b being set st ( ( a is empty or b is empty ) implies b1 = NOT1 {} ) & ( not a is empty & not b is empty implies b1 = {} ) holds
( ( ( b is empty or a is empty ) implies b1 = NOT1 {} ) & ( not b is empty & not a is empty implies b1 = {} ) )
;
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:12
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 b1 being set holds verum
;
;
commutativity
for b1, a, b being set st ( not a is empty or not b is empty or b1 = NOT1 {} ) & ( ( not a is empty or not b is empty ) implies b1 = {} ) holds
( ( not b is empty or not a is empty or b1 = NOT1 {} ) & ( ( not b is empty or not a is empty ) implies b1 = {} ) )
;
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:13
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 b1 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:14
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 b1 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:15
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 b1 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:16
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 b1 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:17
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 b1 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:18
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 b1 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:19
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 b1 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:20
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 b1 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:21
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 b1 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:22
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 b1 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:23
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 b1 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:24
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 b1 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:25
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 b1 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:26
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 b1 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:27
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 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:28
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:29
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:30
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:31
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:32
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:33
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:34
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:35
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:36
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:37
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:38
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:39
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;

:: The following theorem shows that an MSB carry of '4 Bit Carry Skip Adder'
:: is equivalent to an MSB carry of a normal 4 bit adder.
:: We assume that there is no feedback loop in adders.
theorem :: GATE_1:40
for c1, x1, x2, x3, x4, y1, y2, y3, y4, c2, c3, c4, c5, n1, n2, n3, n4, n, c5b being set 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 b1 being set holds verum
;
;
commutativity
for b1, a, b being set st ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) implies b1 = NOT1 {} ) & ( ( ( a is empty & b is empty ) or ( not a is empty & not b is empty ) ) implies b1 = {} ) holds
( ( ( not b is empty or not a is empty ) & ( b is empty or a is empty ) implies b1 = NOT1 {} ) & ( ( ( b is empty & a is empty ) or ( not b is empty & not a is empty ) ) implies b1 = {} ) )
;
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:41
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;

::The following two definitions are for normal 2 bit adder.
definition
let a1, b1, a2, b2, c be set ;
func ADD2 (a2,b2,a1,b1,c) -> set equals :: GATE_1:def 35
XOR3 (a2,b2,(CARR1 (a1,b1,c)));
coherence
XOR3 (a2,b2,(CARR1 (a1,b1,c))) is set
;
end;

:: deftheorem defines ADD2 GATE_1:def 35 :
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 36
MAJ3 (a2,b2,(CARR1 (a1,b1,c)));
coherence
MAJ3 (a2,b2,(CARR1 (a1,b1,c))) is set
;
end;

:: deftheorem defines CARR2 GATE_1:def 36 :
for a1, b1, a2, b2, c being set holds CARR2 (a2,b2,a1,b1,c) = MAJ3 (a2,b2,(CARR1 (a1,b1,c)));

::The following two definitions are for normal 3 bit adder.
definition
let a1, b1, a2, b2, a3, b3, c be set ;
func ADD3 (a3,b3,a2,b2,a1,b1,c) -> set equals :: GATE_1:def 37
XOR3 (a3,b3,(CARR2 (a2,b2,a1,b1,c)));
coherence
XOR3 (a3,b3,(CARR2 (a2,b2,a1,b1,c))) is set
;
end;

:: deftheorem defines ADD3 GATE_1:def 37 :
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 38
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 38 :
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)));

::The following two definitions are for normal 4 bit adder.
definition
let a1, b1, a2, b2, a3, b3, a4, b4, c be set ;
func ADD4 (a4,b4,a3,b3,a2,b2,a1,b1,c) -> set equals :: GATE_1:def 39
XOR3 (a4,b4,(CARR3 (a3,b3,a2,b2,a1,b1,c)));
coherence
XOR3 (a4,b4,(CARR3 (a3,b3,a2,b2,a1,b1,c))) is set
;
end;

:: deftheorem defines ADD4 GATE_1:def 39 :
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 40
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 40 :
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)));

::The following theorem shows that outputs of