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


begin

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
( NOT1 {{}} = {} & NOT1 {} = {{}} ) by Def1;

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 being set
for 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 being set
for 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 being set
for 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
proofend;

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

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 being set
for 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 being set
for 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;

begin

:: 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 )
proofend;

::Definition of mod 2 adder used in 'Carry Look Ahead Adder'
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 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 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
:: '4 Bit Carry Look Ahead Adder'
:: are equivalent to outputs of normal 4 bits adder.
:: We assume that there is no feedback loop in adders.
theorem :: GATE_1:42
for c1, x1, y1, x2, y2, x3, y3, x4, y4, c4, q1, p1, sd1, q2, p2, sd2, q3, p3, sd3, q4, p4, sd4, cb1, cb2, l2, t2, l3, m3, t3, l4, m4, n4, t4, l5, m5, n5, o5, s1, s2, s3, s4 being set holds
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 ) ) )
proofend;