:: by Yatsuka Nakamura

::

:: Received February 4, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

definition

let a be set ;

correctness

coherence

( ( not a is empty implies {} is set ) & ( a is empty implies {{}} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
correctness

coherence

( ( not a is empty implies {} is set ) & ( a is empty implies {{}} is set ) );

consistency

for b

;

:: 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 = {{}} ) );

for a being set holds

( ( not a is empty implies NOT1 a = {} ) & ( a is empty implies NOT1 a = {{}} ) );

registration
end;

registration
end;

definition

let a, b be set ;

coherence

( ( not a is empty & not b is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

commutativity

for b_{1} being set

for a, b being set st ( not a is empty & not b is empty implies b_{1} = NOT1 {} ) & ( ( a is empty or b is empty ) implies b_{1} = {} ) holds

( ( not b is empty & not a is empty implies b_{1} = NOT1 {} ) & ( ( b is empty or a is empty ) implies b_{1} = {} ) )
;

end;
func AND2 (a,b) -> set equals :Def2: :: GATE_1:def 2

NOT1 {} if ( not a is empty & not b is empty )

otherwise {} ;

correctness NOT1 {} if ( not a is empty & not b is empty )

otherwise {} ;

coherence

( ( not a is empty & not b is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty ) implies {} is set ) );

consistency

for b

;

commutativity

for b

for a, b being set st ( not a is empty & not b is empty implies b

( ( not b is empty & not a is empty implies b

:: 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) = {} ) );

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) = {} ) );

theorem :: GATE_1:4

definition

let a, b be set ;

coherence

( ( ( not a is empty or not b is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or {} is set ) );

consistency

for b_{1} being set holds verum;

;

commutativity

for b_{1} being set

for a, b being set st ( ( not a is empty or not b is empty ) implies b_{1} = NOT1 {} ) & ( not a is empty or not b is empty or b_{1} = {} ) holds

( ( ( not b is empty or not a is empty ) implies b_{1} = NOT1 {} ) & ( not b is empty or not a is empty or b_{1} = {} ) )
;

end;
func OR2 (a,b) -> set equals :Def3: :: GATE_1:def 3

NOT1 {} if ( not a is empty or not b is empty )

otherwise {} ;

correctness NOT1 {} if ( not a is empty or not b is empty )

otherwise {} ;

coherence

( ( ( not a is empty or not b is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or {} is set ) );

consistency

for b

;

commutativity

for b

for a, b being set st ( ( not a is empty or not b is empty ) implies b

( ( ( not b is empty or not a is empty ) implies b

:: 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) = {} ) );

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
end;

theorem :: GATE_1:5

definition

let a, b be set ;

coherence

( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies NOT1 {} is set ) & ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) or {} is set ) );

consistency

for b_{1} being set holds verum;

;

commutativity

for b_{1} being set

for a, b being set st ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies b_{1} = NOT1 {} ) & ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) or b_{1} = {} ) holds

( ( ( ( not b is empty & a is empty ) or ( b is empty & not a is empty ) ) implies b_{1} = NOT1 {} ) & ( ( not b is empty & a is empty ) or ( b is empty & not a is empty ) or b_{1} = {} ) )
;

end;
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 NOT1 {} if ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) )

otherwise {} ;

coherence

( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies NOT1 {} is set ) & ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) or {} is set ) );

consistency

for b

;

commutativity

for b

for a, b being set st ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies b

( ( ( ( not b is empty & a is empty ) or ( b is empty & not a is empty ) ) implies b

:: 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) = {} ) );

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
end;

registration
end;

registration
end;

theorem :: GATE_1:6

theorem :: GATE_1:9

definition

let a, b be set ;

coherence

( not ( ( not a is empty implies not b is empty ) & ( not b is empty implies not a is empty ) & NOT1 {} is not set ) & ( ( ( not a is empty & b is empty ) or ( not b is empty & a is empty ) ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

commutativity

for b_{1} being set

for a, b being set st not ( ( not a is empty implies not b is empty ) & ( not b is empty implies not a is empty ) & not b_{1} = NOT1 {} ) & ( ( ( not a is empty & b is empty ) or ( not b is empty & a is empty ) ) implies b_{1} = {} ) holds

( not ( ( not b is empty implies not a is empty ) & ( not a is empty implies not b is empty ) & not b_{1} = NOT1 {} ) & ( ( ( not b is empty & a is empty ) or ( not a is empty & b is empty ) ) implies b_{1} = {} ) )
;

end;
func EQV2 (a,b) -> set equals :Def5: :: GATE_1:def 5

NOT1 {} if ( not a is empty iff not b is empty )

otherwise {} ;

correctness NOT1 {} if ( not a is empty iff not b is empty )

otherwise {} ;

coherence

( not ( ( not a is empty implies not b is empty ) & ( not b is empty implies not a is empty ) & NOT1 {} is not set ) & ( ( ( not a is empty & b is empty ) or ( not b is empty & a is empty ) ) implies {} is set ) );

consistency

for b

;

commutativity

for b

for a, b being set st not ( ( not a is empty implies not b is empty ) & ( not b is empty implies not a is empty ) & not b

( not ( ( not b is empty implies not a is empty ) & ( not a is empty implies not b is empty ) & not b

:: 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) = {} ) );

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
end;

theorem :: GATE_1:10

definition

let a, b be set ;

coherence

( ( ( a is empty or b is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

commutativity

for b_{1} being set

for a, b being set st ( ( a is empty or b is empty ) implies b_{1} = NOT1 {} ) & ( not a is empty & not b is empty implies b_{1} = {} ) holds

( ( ( b is empty or a is empty ) implies b_{1} = NOT1 {} ) & ( not b is empty & not a is empty implies b_{1} = {} ) )
;

end;
func NAND2 (a,b) -> set equals :Def6: :: GATE_1:def 6

NOT1 {} if ( a is empty or b is empty )

otherwise {} ;

correctness NOT1 {} if ( a is empty or b is empty )

otherwise {} ;

coherence

( ( ( a is empty or b is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty implies {} is set ) );

consistency

for b

;

commutativity

for b

for a, b being set st ( ( a is empty or b is empty ) implies b

( ( ( b is empty or a is empty ) implies b

:: 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) = {} ) );

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
end;

theorem :: GATE_1:12

definition

let a, b be set ;

coherence

( ( not a is empty or not b is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

commutativity

for b_{1} being set

for a, b being set st ( not a is empty or not b is empty or b_{1} = NOT1 {} ) & ( ( not a is empty or not b is empty ) implies b_{1} = {} ) holds

( ( not b is empty or not a is empty or b_{1} = NOT1 {} ) & ( ( not b is empty or not a is empty ) implies b_{1} = {} ) )
;

end;
func NOR2 (a,b) -> set equals :Def7: :: GATE_1:def 7

NOT1 {} if ( a is empty & b is empty )

otherwise {} ;

correctness NOT1 {} if ( a is empty & b is empty )

otherwise {} ;

coherence

( ( not a is empty or not b is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty ) implies {} is set ) );

consistency

for b

;

commutativity

for b

for a, b being set st ( not a is empty or not b is empty or b

( ( not b is empty or not a is empty or b

:: 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) = {} ) );

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) = {} ) );

theorem :: GATE_1:13

definition

let a, b, c be set ;

coherence

( ( not a is empty & not b is empty & not c is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( not a is empty & not b is empty & not c is empty )

otherwise {} ;

coherence

( ( not a is empty & not b is empty & not c is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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 be empty set ;

let b, c be set ;

coherence

AND3 (a,b,c) is empty by Def8;

coherence

AND3 (b,a,c) is empty by Def8;

coherence

AND3 (b,c,a) is empty by Def8;

end;
let b, c be set ;

coherence

AND3 (a,b,c) is empty by Def8;

coherence

AND3 (b,a,c) is empty by Def8;

coherence

AND3 (b,c,a) is empty by Def8;

theorem :: GATE_1:14

definition

let a, b, c be set ;

coherence

( ( ( not a is empty or not b is empty or not c is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( not a is empty or not b is empty or not c is empty )

otherwise {} ;

coherence

( ( ( not a is empty or not b is empty or not c is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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
end;

registration

let a be non empty set ;

let b, c be set ;

coherence

not OR3 (a,b,c) is empty by Def9;

coherence

not OR3 (b,a,c) is empty by Def9;

coherence

not OR3 (b,c,a) is empty by Def9;

end;
let b, c be set ;

coherence

not OR3 (a,b,c) is empty by Def9;

coherence

not OR3 (b,a,c) is empty by Def9;

coherence

not OR3 (b,c,a) is empty by Def9;

theorem :: GATE_1:15

definition

let a, b, c be set ;

coherence

( ( ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) ) implies NOT1 {} is set ) & ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) or {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) ) implies NOT1 {} is set ) & ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) or {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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 be empty set ;

let c be non empty set ;

coherence

not XOR3 (a,b,c) is empty by Def10;

coherence

not XOR3 (a,c,b) is empty by Def10;

coherence

not XOR3 (c,a,b) is empty by Def10;

end;
let c be non empty set ;

coherence

not XOR3 (a,b,c) is empty by Def10;

coherence

not XOR3 (a,c,b) is empty by Def10;

coherence

not XOR3 (c,a,b) is empty by Def10;

registration

let a, b be non empty set ;

let c be empty set ;

coherence

XOR3 (a,b,c) is empty by Def10;

coherence

XOR3 (a,c,b) is empty by Def10;

coherence

XOR3 (c,a,b) is empty by Def10;

end;
let c be empty set ;

coherence

XOR3 (a,b,c) is empty by Def10;

coherence

XOR3 (a,c,b) is empty by Def10;

coherence

XOR3 (c,a,b) is empty by Def10;

theorem :: GATE_1:16

definition

let a, b, c be set ;

coherence

( ( ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) ) implies NOT1 {} is set ) & ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) or {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) ) implies NOT1 {} is set ) & ( ( not a is empty & not b is empty ) or ( not b is empty & not c is empty ) or ( not c is empty & not a is empty ) or {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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 ;

coherence

not MAJ3 (a,b,c) is empty by Def11;

coherence

not MAJ3 (a,c,b) is empty by Def11;

coherence

not MAJ3 (c,a,b) is empty by Def11;

end;
let c be set ;

coherence

not MAJ3 (a,b,c) is empty by Def11;

coherence

not MAJ3 (a,c,b) is empty by Def11;

coherence

not MAJ3 (c,a,b) is empty by Def11;

registration

let a, b be empty set ;

let c be set ;

coherence

MAJ3 (a,b,c) is empty by Def11;

coherence

MAJ3 (a,c,b) is empty by Def11;

coherence

MAJ3 (c,a,b) is empty by Def11;

end;
let c be set ;

coherence

MAJ3 (a,b,c) is empty by Def11;

coherence

MAJ3 (a,c,b) is empty by Def11;

coherence

MAJ3 (c,a,b) is empty by Def11;

theorem :: GATE_1:17

definition

let a, b, c be set ;

coherence

( ( ( a is empty or b is empty or c is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( a is empty or b is empty or c is empty )

otherwise {} ;

coherence

( ( ( a is empty or b is empty or c is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c be set ;

coherence

( ( not a is empty or not b is empty or not c is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( a is empty & b is empty & c is empty )

otherwise {} ;

coherence

( ( not a is empty or not b is empty or not c is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d be set ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty )

otherwise {} ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d be set ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty )

otherwise {} ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d be set ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( a is empty or b is empty or c is empty or d is empty )

otherwise {} ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d be set ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( a is empty & b is empty & c is empty & d is empty )

otherwise {} ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e be set ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty )

otherwise {} ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e be set ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e be set ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty )

otherwise {} ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e be set ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty )

otherwise {} ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f be set ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f be set ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f be set ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f be set ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty )

otherwise {} ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f, g be set ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f, g be set ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f, g be set ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f, g be set ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty & g is empty )

otherwise {} ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f, g, h be set ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f, g, h be set ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty or {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty or {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f, g, h be set ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

definition

let a, b, c, d, e, f, g, h be set ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 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 {} ;

coherence

( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) implies {} is set ) );

consistency

for b

;

:: 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) = {} ) );

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

begin

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 )

( not c5 is empty iff not c5b is empty )

proof end;

::Definition of mod 2 adder used in 'Carry Look Ahead Adder'

definition

let a, b be set ;

coherence

( ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) implies NOT1 {} is set ) & ( ( ( a is empty & b is empty ) or ( not a is empty & not b is empty ) ) implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

commutativity

for b_{1} being set

for a, b being set st ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) implies b_{1} = NOT1 {} ) & ( ( ( a is empty & b is empty ) or ( not a is empty & not b is empty ) ) implies b_{1} = {} ) holds

( ( ( not b is empty or not a is empty ) & ( b is empty or a is empty ) implies b_{1} = NOT1 {} ) & ( ( ( b is empty & a is empty ) or ( not b is empty & not a is empty ) ) implies b_{1} = {} ) )
;

end;
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 NOT1 {} if ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) )

otherwise {} ;

coherence

( ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) implies NOT1 {} is set ) & ( ( ( a is empty & b is empty ) or ( not a is empty & not b is empty ) ) implies {} is set ) );

consistency

for b

;

commutativity

for b

for a, b being set st ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) implies b

( ( ( not b is empty or not a is empty ) & ( b is empty or a is empty ) implies b

:: 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) = {} ) );

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

notation
end;

::The following two definitions are for normal 2 bit adder.

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

for a1, b1, a2, b2, c being set holds ADD2 (a2,b2,a1,b1,c) = XOR3 (a2,b2,(CARR1 (a1,b1,c)));

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

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 ;

XOR3 (a3,b3,(CARR2 (a2,b2,a1,b1,c))) is set ;

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

XOR3 (a3,b3,(CARR2 (a2,b2,a1,b1,c))) is set ;

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

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 ;

MAJ3 (a3,b3,(CARR2 (a2,b2,a1,b1,c))) is set ;

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

MAJ3 (a3,b3,(CARR2 (a2,b2,a1,b1,c))) is set ;

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

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 ;

XOR3 (a4,b4,(CARR3 (a3,b3,a2,b2,a1,b1,c))) is set ;

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

XOR3 (a4,b4,(CARR3 (a3,b3,a2,b2,a1,b1,c))) is set ;

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

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 ;

MAJ3 (a4,b4,(CARR3 (a3,b3,a2,b2,a1,b1,c))) is set ;

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

MAJ3 (a4,b4,(CARR3 (a3,b3,a2,b2,a1,b1,c))) is set ;

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

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.

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

not ( ( not q1 is empty implies not NOR2 (x1,y1) is empty ) & ( not NOR2 (x1,y1) is empty implies not q1 is empty ) & ( not p1 is empty implies not NAND2 (x1,y1) is empty ) & ( not NAND2 (x1,y1) is empty implies not p1 is empty ) & ( not sd1 is empty implies not MODADD2 (x1,y1) is empty ) & ( not MODADD2 (x1,y1) is empty implies not sd1 is empty ) & ( not q2 is empty implies not NOR2 (x2,y2) is empty ) & ( not NOR2 (x2,y2) is empty implies not q2 is empty ) & ( not p2 is empty implies not NAND2 (x2,y2) is empty ) & ( not NAND2 (x2,y2) is empty implies not p2 is empty ) & ( not sd2 is empty implies not MODADD2 (x2,y2) is empty ) & ( not MODADD2 (x2,y2) is empty implies not sd2 is empty ) & ( not q3 is empty implies not NOR2 (x3,y3) is empty ) & ( not NOR2 (x3,y3) is empty implies not q3 is empty ) & ( not p3 is empty implies not NAND2 (x3,y3) is empty ) & ( not NAND2 (x3,y3) is empty implies not p3 is empty ) & ( not sd3 is empty implies not MODADD2 (x3,y3) is empty ) & ( not MODADD2 (x3,y3) is empty implies not sd3 is empty ) & ( not q4 is empty implies not NOR2 (x4,y4) is empty ) & ( not NOR2 (x4,y4) is empty implies not q4 is empty ) & ( not p4 is empty implies not NAND2 (x4,y4) is empty ) & ( not NAND2 (x4,y4) is empty implies not p4 is empty ) & ( not sd4 is empty implies not MODADD2 (x4,y4) is empty ) & ( not MODADD2 (x4,y4) is empty implies not sd4 is empty ) & ( not cb1 is empty implies not NOT1 c1 is empty ) & ( not NOT1 c1 is empty implies not cb1 is empty ) & ( not cb2 is empty implies not NOT1 cb1 is empty ) & ( not NOT1 cb1 is empty implies not cb2 is empty ) & ( not s1 is empty implies not XOR2 (cb2,sd1) is empty ) & ( not XOR2 (cb2,sd1) is empty implies not s1 is empty ) & ( not l2 is empty implies not AND2 (cb1,p1) is empty ) & ( not AND2 (cb1,p1) is empty implies not l2 is empty ) & ( not t2 is empty implies not NOR2 (l2,q1) is empty ) & ( not NOR2 (l2,q1) is empty implies not t2 is empty ) & ( not s2 is empty implies not XOR2 (t2,sd2) is empty ) & ( not XOR2 (t2,sd2) is empty implies not s2 is empty ) & ( not l3 is empty implies not AND2 (q1,p2) is empty ) & ( not AND2 (q1,p2) is empty implies not l3 is empty ) & ( not m3 is empty implies not AND3 (p2,p1,cb1) is empty ) & ( not AND3 (p2,p1,cb1) is empty implies not m3 is empty ) & ( not t3 is empty implies not NOR3 (l3,m3,q2) is empty ) & ( not NOR3 (l3,m3,q2) is empty implies not t3 is empty ) & ( not s3 is empty implies not XOR2 (t3,sd3) is empty ) & ( not XOR2 (t3,sd3) is empty implies not s3 is empty ) & ( not l4 is empty implies not AND2 (q2,p3) is empty ) & ( not AND2 (q2,p3) is empty implies not l4 is empty ) & ( not m4 is empty implies not AND3 (q1,p3,p2) is empty ) & ( not AND3 (q1,p3,p2) is empty implies not m4 is empty ) & ( not n4 is empty implies not AND4 (p3,p2,p1,cb1) is empty ) & ( not AND4 (p3,p2,p1,cb1) is empty implies not n4 is empty ) & ( not t4 is empty implies not NOR4 (l4,m4,n4,q3) is empty ) & ( not NOR4 (l4,m4,n4,q3) is empty implies not t4 is empty ) & ( not s4 is empty implies not XOR2 (t4,sd4) is empty ) & ( not XOR2 (t4,sd4) is empty implies not s4 is empty ) & ( not l5 is empty implies not AND2 (q3,p4) is empty ) & ( not AND2 (q3,p4) is empty implies not l5 is empty ) & ( not m5 is empty implies not AND3 (q2,p4,p3) is empty ) & ( not AND3 (q2,p4,p3) is empty implies not m5 is empty ) & ( not n5 is empty implies not AND4 (q1,p4,p3,p2) is empty ) & ( not AND4 (q1,p4,p3,p2) is empty implies not n5 is empty ) & ( not o5 is empty implies not AND5 (p4,p3,p2,p1,cb1) is empty ) & ( not AND5 (p4,p3,p2,p1,cb1) is empty implies not o5 is empty ) & ( not c4 is empty implies not NOR5 (q4,l5,m5,n5,o5) is empty ) & ( not NOR5 (q4,l5,m5,n5,o5) is empty implies not c4 is empty ) & not ( ( not s1 is empty implies not ADD1 (x1,y1,c1) is empty ) & ( not ADD1 (x1,y1,c1) is empty implies not s1 is empty ) & ( not s2 is empty implies not ADD2 (x2,y2,x1,y1,c1) is empty ) & ( not ADD2 (x2,y2,x1,y1,c1) is empty implies not s2 is empty ) & ( not s3 is empty implies not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty implies not s3 is empty ) & ( not s4 is empty implies not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not s4 is empty ) & ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) & ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty ) ) )

proof end;

:: is equivalent to an MSB carry of a normal 4 bit adder.

:: We assume that there is no feedback loop in adders.