:: GATE_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

notation
let a be set ;
antonym $ a for empty a;
end;

theorem Th1: :: GATE_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set st a = {{} } holds
$ a ;

theorem :: GATE_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex a being set st $ a
proof end;

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

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

theorem :: GATE_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: GATE_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds
( $ NOT1 a iff not $ a ) by Def1;

theorem Th5: :: GATE_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
$ NOT1 {} by Th4;

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

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

theorem :: GATE_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds
( $ AND2 a,b iff ( $ a & $ b ) ) by Def2, Th5;

definition
let a, b be set ;
func OR2 a,b -> set equals :Def3: :: GATE_1:def 3
 NOT1 {} if ( $ a or $ b )
otherwise {} ;
correctness
coherence
( ( ( $ a or $ b ) implies NOT1 {} is set ) & ( $ a or $ b or {} is set ) );
consistency
for b1 being set holds verum;
;
end;

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

theorem Th7: :: GATE_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds
( ( $ a or $ b ) iff $ OR2 a,b ) by Def3, Th5;

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

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

theorem :: GATE_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds
( ( ( $ a & not $ b ) or ( not $ a & $ b ) ) iff $ XOR2 a,b ) by Def4, Th5;

theorem :: GATE_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds
( contradiction iff $ XOR2 a,a )
proof end;

theorem :: GATE_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds
( $ XOR2 a,{} iff $ a ) by Def4, Th5;

theorem :: GATE_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds
( $ XOR2 a,b iff $ XOR2 b,a )
proof end;

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

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

theorem :: GATE_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds
( $ EQV2 a,b iff ( $ a iff $ b ) ) by Def5, Th5;

theorem :: GATE_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds
( $ EQV2 a,b iff not $ XOR2 a,b )
proof end;

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

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

theorem :: GATE_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds
( $ NAND2 a,b & $ a iff not $ b ) by Def6, Th5;

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

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

theorem :: GATE_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds
( $ NOR2 a,b iff ( not $ a & not $ b ) ) by Def7, Th5;

definition
let a, b, c be set ;
func AND3 a,b,c -> set equals :Def8: :: GATE_1:def 8
 NOT1 {} if ( $ a & $ b & $ c )
otherwise {} ;
correctness
coherence
( ( $ a & $ b & $ c implies NOT1 {} is set ) & ( ( not $ a or not $ b or not $ c ) 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
( ( $ a & $ b & $ c implies AND3 a,b,c = NOT1 {} ) & ( ( not $ a or not $ b or not $ c ) implies AND3 a,b,c = {} ) );

theorem :: GATE_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being set holds
( $ AND3 a,b,c iff ( $ a & $ b & $ c ) ) by Def8, Th5;

definition
let a, b, c be set ;
func OR3 a,b,c -> set equals :Def9: :: GATE_1:def 9
 NOT1 {} if ( $ a or $ b or $ c )
otherwise {} ;
correctness
coherence
( ( ( $ a or $ b or $ c ) implies NOT1 {} is set ) & ( $ a or $ b or $ c 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
( ( ( $ a or $ b or $ c ) implies OR3 a,b,c = NOT1 {} ) & ( $ a or $ b or $ c or OR3 a,b,c = {} ) );

theorem :: GATE_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being set holds
( ( $ a or $ b or $ c ) iff $ OR3 a,b,c ) by Def9, Th5;

definition
let a, b, c be set ;
func XOR3 a,b,c -> set equals :Def10: :: GATE_1:def 10
 NOT1 {} if ( ( ( ( $ a & not $ b ) or ( not $ a & $ b ) ) & not $ c ) or ( not ( $ a & not $ b ) & not ( not $ a & $ b ) & $ c ) )
otherwise {} ;
correctness
coherence
( ( ( ( ( ( $ a & not $ b ) or ( not $ a & $ b ) ) & not $ c ) or ( not ( $ a & not $ b ) & not ( not $ a & $ b ) & $ c ) ) implies NOT1 {} is set ) & ( ( ( ( $ a & not $ b ) or ( not $ a & $ b ) ) & not $ c ) or ( not ( $ a & not $ b ) & not ( not $ a & $ b ) & $ c ) 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
( ( ( ( ( ( $ a & not $ b ) or ( not $ a & $ b ) ) & not $ c ) or ( not ( $ a & not $ b ) & not ( not $ a & $ b ) & $ c ) ) implies XOR3 a,b,c = NOT1 {} ) & ( ( ( ( $ a & not $ b ) or ( not $ a & $ b ) ) & not $ c ) or ( not ( $ a & not $ b ) & not ( not $ a & $ b ) & $ c ) or XOR3 a,b,c = {} ) );

theorem Th18: :: GATE_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being set holds
( ( ( ( ( $ a & not $ b ) or ( not $ a & $ b ) ) & not $ c ) or ( not ( $ a & not $ b ) & not ( not $ a & $ b ) & $ c ) ) iff $ XOR3 a,b,c ) by Def10, Th5;

definition
let a, b, c be set ;
func MAJ3 a,b,c -> set equals :Def11: :: GATE_1:def 11
 NOT1 {} if ( ( $ a & $ b ) or ( $ b & $ c ) or ( $ c & $ a ) )
otherwise {} ;
correctness
coherence
( ( ( ( $ a & $ b ) or ( $ b & $ c ) or ( $ c & $ a ) ) implies NOT1 {} is set ) & ( ( $ a & $ b ) or ( $ b & $ c ) or ( $ c & $ a ) 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
( ( ( ( $ a & $ b ) or ( $ b & $ c ) or ( $ c & $ a ) ) implies MAJ3 a,b,c = NOT1 {} ) & ( ( $ a & $ b ) or ( $ b & $ c ) or ( $ c & $ a ) or MAJ3 a,b,c = {} ) );

theorem Th19: :: GATE_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being set holds
( ( ( $ a & $ b ) or ( $ b & $ c ) or ( $ c & $ a ) ) iff $ MAJ3 a,b,c ) by Def11, Th5;

definition
let a, b, c be set ;
func NAND3 a,b,c -> set equals :Def12: :: GATE_1:def 12
 NOT1 {} if ( not $ a or not $ b or not $ c )
otherwise {} ;
correctness
coherence
( ( ( not $ a or not $ b or not $ c ) implies NOT1 {} is set ) & ( $ a & $ b & $ c 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
( ( ( not $ a or not $ b or not $ c ) implies NAND3 a,b,c = NOT1 {} ) & ( $ a & $ b & $ c implies NAND3 a,b,c = {} ) );

theorem :: GATE_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being set holds
( $ NAND3 a,b,c & $ a & $ b iff not $ c ) by Def12, Th5;

definition
let a, b, c be set ;
func NOR3 a,b,c -> set equals :Def13: :: GATE_1:def 13
 NOT1 {} if ( not $ a & not $ b & not $ c )
otherwise {} ;
correctness
coherence
( ( $ a or $ b or $ c or NOT1 {} is set ) & ( ( $ a or $ b or $ c ) 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
( ( $ a or $ b or $ c or NOR3 a,b,c = NOT1 {} ) & ( ( $ a or $ b or $ c ) implies NOR3 a,b,c = {} ) );

theorem :: GATE_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being set holds
( $ NOR3 a,b,c iff ( not $ a & not $ b & not $ c ) ) by Def13, Th5;

definition
let a, b, c, d be set ;
func AND4 a,b,c,d -> set equals :Def14: :: GATE_1:def 14
 NOT1 {} if ( $ a & $ b & $ c & $ d )
otherwise {} ;
correctness
coherence
( ( $ a & $ b & $ c & $ d implies NOT1 {} is set ) & ( ( not $ a or not $ b or not $ c or not $ d ) 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
( ( $ a & $ b & $ c & $ d implies AND4 a,b,c,d = NOT1 {} ) & ( ( not $ a or not $ b or not $ c or not $ d ) implies AND4 a,b,c,d = {} ) );

theorem :: GATE_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being set holds
( $ AND4 a,b,c,d iff ( $ a & $ b & $ c & $ d ) ) by Def14, Th5;

definition
let a, b, c, d be set ;
func OR4 a,b,c,d -> set equals :Def15: :: GATE_1:def 15
 NOT1 {} if ( $ a or $ b or $ c or $ d )
otherwise {} ;
correctness
coherence
( ( ( $ a or $ b or $ c or $ d ) implies NOT1 {} is set ) & ( $ a or $ b or $ c or $ d 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
( ( ( $ a or $ b or $ c or $ d ) implies OR4 a,b,c,d = NOT1 {} ) & ( $ a or $ b or $ c or $ d or OR4 a,b,c,d = {} ) );

theorem :: GATE_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being set holds
( ( $ a or $ b or $ c or $ d ) iff $ OR4 a,b,c,d ) by Def15, Th5;

definition
let a, b, c, d be set ;
func NAND4 a,b,c,d -> set equals :Def16: :: GATE_1:def 16
 NOT1 {} if ( not $ a or not $ b or not $ c or not $ d )
otherwise {} ;
correctness
coherence
( ( ( not $ a or not $ b or not $ c or not $ d ) implies NOT1 {} is set ) & ( $ a & $ b & $ c & $ d 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
( ( ( not $ a or not $ b or not $ c or not $ d ) implies NAND4 a,b,c,d = NOT1 {} ) & ( $ a & $ b & $ c & $ d implies NAND4 a,b,c,d = {} ) );

theorem :: GATE_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being set holds
( $ NAND4 a,b,c,d & $ a & $ b & $ c iff not $ d ) by Def16, Th5;

definition
let a, b, c, d be set ;
func NOR4 a,b,c,d -> set equals :Def17: :: GATE_1:def 17
 NOT1 {} if ( not $ a & not $ b & not $ c & not $ d )
otherwise {} ;
correctness
coherence
( ( $ a or $ b or $ c or $ d or NOT1 {} is set ) & ( ( $ a or $ b or $ c or $ d ) 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
( ( $ a or $ b or $ c or $ d or NOR4 a,b,c,d = NOT1 {} ) & ( ( $ a or $ b or $ c or $ d ) implies NOR4 a,b,c,d = {} ) );

theorem :: GATE_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being set holds
( $ NOR4 a,b,c,d iff ( not $ a & not $ b & not $ c & not $ d ) ) by Def17, Th5;

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 ( $ a & $ b & $ c & $ d & $ e )
otherwise {} ;
correctness
coherence
( ( $ a & $ b & $ c & $ d & $ e implies NOT1 {} is set ) & ( ( not $ a or not $ b or not $ c or not $ d or not $ e ) 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
( ( $ a & $ b & $ c & $ d & $ e implies AND5 a,b,c,d,e = NOT1 {} ) & ( ( not $ a or not $ b or not $ c or not $ d or not $ e ) implies AND5 a,b,c,d,e = {} ) );

theorem :: GATE_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e being set holds
( $ AND5 a,b,c,d,e iff ( $ a & $ b & $ c & $ d & $ e ) ) by Def18, Th5;

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 ( $ a or $ b or $ c or $ d or $ e )
otherwise {} ;
correctness
coherence
( ( ( $ a or $ b or $ c or $ d or $ e ) implies NOT1 {} is set ) & ( $ a or $ b or $ c or $ d or $ e 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
( ( ( $ a or $ b or $ c or $ d or $ e ) implies OR5 a,b,c,d,e = NOT1 {} ) & ( $ a or $ b or $ c or $ d or $ e or OR5 a,b,c,d,e = {} ) );

theorem :: GATE_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e being set holds
( ( $ a or $ b or $ c or $ d or $ e ) iff $ OR5 a,b,c,d,e ) by Def19, Th5;

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 ( not $ a or not $ b or not $ c or not $ d or not $ e )
otherwise {} ;
correctness
coherence
( ( ( not $ a or not $ b or not $ c or not $ d or not $ e ) implies NOT1 {} is set ) & ( $ a & $ b & $ c & $ d & $ e 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
( ( ( not $ a or not $ b or not $ c or not $ d or not $ e ) implies NAND5 a,b,c,d,e = NOT1 {} ) & ( $ a & $ b & $ c & $ d & $ e implies NAND5 a,b,c,d,e = {} ) );

theorem :: GATE_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e being set holds
( $ NAND5 a,b,c,d,e & $ a & $ b & $ c & $ d iff not $ e ) by Def20, Th5;

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 ( not $ a & not $ b & not $ c & not $ d & not $ e )
otherwise {} ;
correctness
coherence
( ( $ a or $ b or $ c or $ d or $ e or NOT1 {} is set ) & ( ( $ a or $ b or $ c or $ d or $ e ) 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
( ( $ a or $ b or $ c or $ d or $ e or NOR5 a,b,c,d,e = NOT1 {} ) & ( ( $ a or $ b or $ c or $ d or $ e ) implies NOR5 a,b,c,d,e = {} ) );

theorem :: GATE_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e being set holds
( $ NOR5 a,b,c,d,e iff ( not $ a & not $ b & not $ c & not $ d & not $ e ) ) by Def21, Th5;

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 ( $ a & $ b & $ c & $ d & $ e & $ f )
otherwise {} ;
correctness
coherence
( ( $ a & $ b & $ c & $ d & $ e & $ f implies NOT1 {} is set ) & ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f ) 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
( ( $ a & $ b & $ c & $ d & $ e & $ f implies AND6 a,b,c,d,e,f = NOT1 {} ) & ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f ) implies AND6 a,b,c,d,e,f = {} ) );

theorem :: GATE_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f being set holds
( $ AND6 a,b,c,d,e,f iff ( $ a & $ b & $ c & $ d & $ e & $ f ) ) by Def22, Th5;

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 ( $ a or $ b or $ c or $ d or $ e or $ f )
otherwise {} ;
correctness
coherence
( ( ( $ a or $ b or $ c or $ d or $ e or $ f ) implies NOT1 {} is set ) & ( $ a or $ b or $ c or $ d or $ e or $ f 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
( ( ( $ a or $ b or $ c or $ d or $ e or $ f ) implies OR6 a,b,c,d,e,f = NOT1 {} ) & ( $ a or $ b or $ c or $ d or $ e or $ f or OR6 a,b,c,d,e,f = {} ) );

theorem :: GATE_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f being set holds
( ( $ a or $ b or $ c or $ d or $ e or $ f ) iff $ OR6 a,b,c,d,e,f ) by Def23, Th5;

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 ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f )
otherwise {} ;
correctness
coherence
( ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f ) implies NOT1 {} is set ) & ( $ a & $ b & $ c & $ d & $ e & $ f 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
( ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f ) implies NAND6 a,b,c,d,e,f = NOT1 {} ) & ( $ a & $ b & $ c & $ d & $ e & $ f implies NAND6 a,b,c,d,e,f = {} ) );

theorem :: GATE_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f being set holds
( $ NAND6 a,b,c,d,e,f & $ a & $ b & $ c & $ d & $ e iff not $ f ) by Def24, Th5;

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 ( not $ a & not $ b & not $ c & not $ d & not $ e & not $ f )
otherwise {} ;
correctness
coherence
( ( $ a or $ b or $ c or $ d or $ e or $ f or NOT1 {} is set ) & ( ( $ a or $ b or $ c or $ d or $ e or $ f ) 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
( ( $ a or $ b or $ c or $ d or $ e or $ f or NOR6 a,b,c,d,e,f = NOT1 {} ) & ( ( $ a or $ b or $ c or $ d or $ e or $ f ) implies NOR6 a,b,c,d,e,f = {} ) );

theorem :: GATE_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f being set holds
( $ NOR6 a,b,c,d,e,f iff ( not $ a & not $ b & not $ c & not $ d & not $ e & not $ f ) ) by Def25, Th5;

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 ( $ a & $ b & $ c & $ d & $ e & $ f & $ g )
otherwise {} ;
correctness
coherence
( ( $ a & $ b & $ c & $ d & $ e & $ f & $ g implies NOT1 {} is set ) & ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g ) 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
( ( $ a & $ b & $ c & $ d & $ e & $ f & $ g implies AND7 a,b,c,d,e,f,g = NOT1 {} ) & ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g ) implies AND7 a,b,c,d,e,f,g = {} ) );

theorem :: GATE_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f, g being set holds
( $ AND7 a,b,c,d,e,f,g iff ( $ a & $ b & $ c & $ d & $ e & $ f & $ g ) ) by Def26, Th5;

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 ( $ a or $ b or $ c or $ d or $ e or $ f or $ g )
otherwise {} ;
correctness
coherence
( ( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g ) implies NOT1 {} is set ) & ( $ a or $ b or $ c or $ d or $ e or $ f or $ g 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
( ( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g ) implies OR7 a,b,c,d,e,f,g = NOT1 {} ) & ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or OR7 a,b,c,d,e,f,g = {} ) );

theorem :: GATE_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f, g being set holds
( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g ) iff $ OR7 a,b,c,d,e,f,g ) by Def27, Th5;

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 ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g )
otherwise {} ;
correctness
coherence
( ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g ) implies NOT1 {} is set ) & ( $ a & $ b & $ c & $ d & $ e & $ f & $ g 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
( ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g ) implies NAND7 a,b,c,d,e,f,g = NOT1 {} ) & ( $ a & $ b & $ c & $ d & $ e & $ f & $ g implies NAND7 a,b,c,d,e,f,g = {} ) );

theorem :: GATE_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f, g being set holds
( $ NAND7 a,b,c,d,e,f,g & $ a & $ b & $ c & $ d & $ e & $ f iff not $ g ) by Def28, Th5;

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 ( not $ a & not $ b & not $ c & not $ d & not $ e & not $ f & not $ g )
otherwise {} ;
correctness
coherence
( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or NOT1 {} is set ) & ( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g ) 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
( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or NOR7 a,b,c,d,e,f,g = NOT1 {} ) & ( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g ) implies NOR7 a,b,c,d,e,f,g = {} ) );

theorem :: GATE_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f, g being set holds
( $ NOR7 a,b,c,d,e,f,g iff ( not $ a & not $ b & not $ c & not $ d & not $ e & not $ f & not $ g ) ) by Def29, Th5;

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 ( $ a & $ b & $ c & $ d & $ e & $ f & $ g & $ h )
otherwise {} ;
correctness
coherence
( ( $ a & $ b & $ c & $ d & $ e & $ f & $ g & $ h implies NOT1 {} is set ) & ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g or not $ h ) 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
( ( $ a & $ b & $ c & $ d & $ e & $ f & $ g & $ h implies AND8 a,b,c,d,e,f,g,h = NOT1 {} ) & ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g or not $ h ) implies AND8 a,b,c,d,e,f,g,h = {} ) );

theorem :: GATE_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f, g, h being set holds
( $ AND8 a,b,c,d,e,f,g,h iff ( $ a & $ b & $ c & $ d & $ e & $ f & $ g & $ h ) ) by Def30, Th5;

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 ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h )
otherwise {} ;
correctness
coherence
( ( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h ) implies NOT1 {} is set ) & ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h 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
( ( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h ) implies OR8 a,b,c,d,e,f,g,h = NOT1 {} ) & ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h or OR8 a,b,c,d,e,f,g,h = {} ) );

theorem :: GATE_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f, g, h being set holds
( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h ) iff $ OR8 a,b,c,d,e,f,g,h ) by Def31, Th5;

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 ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g or not $ h )
otherwise {} ;
correctness
coherence
( ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g or not $ h ) implies NOT1 {} is set ) & ( $ a & $ b & $ c & $ d & $ e & $ f & $ g & $ h 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
( ( ( not $ a or not $ b or not $ c or not $ d or not $ e or not $ f or not $ g or not $ h ) implies NAND8 a,b,c,d,e,f,g,h = NOT1 {} ) & ( $ a & $ b & $ c & $ d & $ e & $ f & $ g & $ h implies NAND8 a,b,c,d,e,f,g,h = {} ) );

theorem :: GATE_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f, g, h being set holds
( $ NAND8 a,b,c,d,e,f,g,h & $ a & $ b & $ c & $ d & $ e & $ f & $ g iff not $ h ) by Def32, Th5;

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 ( not $ a & not $ b & not $ c & not $ d & not $ e & not $ f & not $ g & not $ h )
otherwise {} ;
correctness
coherence
( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h or NOT1 {} is set ) & ( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h ) 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
( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h or NOR8 a,b,c,d,e,f,g,h = NOT1 {} ) & ( ( $ a or $ b or $ c or $ d or $ e or $ f or $ g or $ h ) implies NOR8 a,b,c,d,e,f,g,h = {} ) );

theorem :: GATE_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d, e, f, g, h being set holds
( $ NOR8 a,b,c,d,e,f,g,h iff ( not $ a & not $ b & not $ c & not $ d & not $ e & not $ f & not $ g & not $ h ) ) by Def33, Th5;

theorem :: GATE_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c1, x1, x2, x3, x4, y1, y2, y3, y4, c2, c3, c4, c5, n1, n2, n3, n4, n, c5b being set st ( $ MAJ3 x1,y1,c1 implies $ c2 ) & ( $ MAJ3 x2,y2,c2 implies $ c3 ) & ( $ MAJ3 x3,y3,c3 implies $ c4 ) & ( $ MAJ3 x4,y4,c4 implies $ c5 ) & ( $ n1 implies $ OR2 x1,y1 ) & ( $ n2 implies $ OR2 x2,y2 ) & ( $ n3 implies $ OR2 x3,y3 ) & ( $ n4 implies $ OR2 x4,y4 ) & ( $ n implies $ AND5 c1,n1,n2,n3,n4 ) & ( $ c5b implies $ OR2 c5,n ) & ( $ OR2 c5,n implies $ c5b ) holds
( $ c5 iff $ c5b )
proof end;

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

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

theorem :: GATE_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds
( $ MODADD2 a,b iff ( ( $ a or $ b ) & ( not $ a or not $ b ) ) ) by Def34, Th5;

notation
let a, b, c be set ;
synonym ADD1 a,b,c for XOR3 a,b,c;
synonym CARR1 a,b,c for MAJ3 a,b,c;
end;

definition
let a1, b1, a2, b2, c be set ;
canceled;
canceled;
func ADD2 a2,b2,a1,b1,c -> set equals :: GATE_1:def 37
 XOR3 a2,b2,(CARR1 a1,b1,c);
correctness
coherence
XOR3 a2,b2,(CARR1 a1,b1,c) is set ;
;
end;

:: deftheorem GATE_1:def 35 :
canceled;

:: deftheorem GATE_1:def 36 :
canceled;

:: deftheorem defines ADD2 GATE_1:def 37 :
for a1, b1, a2, b2, c being set holds ADD2 a2,b2,a1,b1,c = XOR3 a2,b2,(CARR1 a1,b1,c);

definition
let a1, b1, a2, b2, c be set ;
func CARR2 a2,b2,a1,b1,c -> set equals :: GATE_1:def 38
 MAJ3 a2,b2,(CARR1 a1,b1,c);
correctness
coherence
MAJ3 a2,b2,(CARR1 a1,b1,c) is set ;
;
end;

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

definition
let a1, b1, a2, b2, a3, b3, c be set ;
func ADD3 a3,b3,a2,b2,a1,b1,c -> set equals :: GATE_1:def 39
 XOR3 a3,b3,(CARR2 a2,b2,a1,b1,c);
correctness
coherence
XOR3 a3,b3,(CARR2 a2,b2,a1,b1,c) is set ;
;
end;

:: deftheorem defines ADD3 GATE_1:def 39 :
for a1, b1, a2, b2, a3, b3, c being set holds ADD3 a3,b3,a2,b2,a1,b1,c = XOR3 a3,b3,(CARR2 a2,b2,a1,b1,c);

definition
let a1, b1, a2, b2, a3, b3, c be set ;
func CARR3 a3,b3,a2,b2,a1,b1,c -> set equals :: GATE_1:def 40
 MAJ3 a3,b3,(CARR2 a2,b2,a1,b1,c);
correctness
coherence
MAJ3 a3,b3,(CARR2 a2,b2,a1,b1,c) is set ;
;
end;

:: deftheorem defines CARR3 GATE_1:def 40 :
for a1, b1, a2, b2, a3, b3, c being set holds CARR3 a3,b3,a2,b2,a1,b1,c = MAJ3 a3,b3,(CARR2 a2,b2,a1,b1,c);

definition
let a1, b1, a2, b2, a3, b3, a4, b4, c be set ;
func ADD4 a4,b4,a3,b3,a2,b2,a1,b1,c -> set equals :: GATE_1:def 41
 XOR3 a4,b4,(CARR3 a3,b3,a2,b2,a1,b1,c);
correctness
coherence
XOR3 a4,b4,(CARR3 a3,b3,a2,b2,a1,b1,c) is set ;
;
end;

:: deftheorem defines ADD4 GATE_1:def 41 :
for a1, b1, a2, b2, a3, b3, a4, b4, c being set holds ADD4 a4,b4,a3,b3,a2,b2,a1,b1,c = XOR3 a4,b4,(CARR3 a3,b3,a2,b2,a1,b1,c);

definition
let a1, b1, a2, b2, a3, b3, a4, b4, c be set ;
func CARR4 a4,b4,a3,b3,a2,b2,a1,b1,c -> set equals :: GATE_1:def 42
 MAJ3 a4,b4,(CARR3 a3,b3,a2,b2,a1,b1,c);
correctness
coherence
MAJ3 a4,b4,(CARR3 a3,b3,a2,b2,a1,b1,c) is set ;
;
end;

:: deftheorem defines CARR4 GATE_1:def 42 :
for a1, b1, a2, b2, a3, b3, a4, b4, c being set holds CARR4 a4,b4,a3,b3,a2,b2,a1,b1,c = MAJ3 a4,b4,(CARR3 a3,b3,a2,b2,a1,b1,c);

theorem :: GATE_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ( ( $ q1 implies $ NOR2 x1,y1 ) & ( $ NOR2 x1,y1 implies $ q1 ) & ( $ p1 implies $ NAND2 x1,y1 ) & ( $ NAND2 x1,y1 implies $ p1 ) & ( $ sd1 implies $ MODADD2 x1,y1 ) & ( $ MODADD2 x1,y1 implies $ sd1 ) & ( $ q2 implies $ NOR2 x2,y2 ) & ( $ NOR2 x2,y2 implies $ q2 ) & ( $ p2 implies $ NAND2 x2,y2 ) & ( $ NAND2 x2,y2 implies $ p2 ) & ( $ sd2 implies $ MODADD2 x2,y2 ) & ( $ MODADD2 x2,y2 implies $ sd2 ) & ( $ q3 implies $ NOR2 x3,y3 ) & ( $ NOR2 x3,y3 implies $ q3 ) & ( $ p3 implies $ NAND2 x3,y3 ) & ( $ NAND2 x3,y3 implies $ p3 ) & ( $ sd3 implies $ MODADD2 x3,y3 ) & ( $ MODADD2 x3,y3 implies $ sd3 ) & ( $ q4 implies $ NOR2 x4,y4 ) & ( $ NOR2 x4,y4 implies $ q4 ) & ( $ p4 implies $ NAND2 x4,y4 ) & ( $ NAND2 x4,y4 implies $ p4 ) & ( $ sd4 implies $ MODADD2 x4,y4 ) & ( $ MODADD2 x4,y4 implies $ sd4 ) & ( $ cb1 implies $ NOT1 c1 ) & ( $ NOT1 c1 implies $ cb1 ) & ( $ cb2 implies $ NOT1 cb1 ) & ( $ NOT1 cb1 implies $ cb2 ) & ( $ s1 implies $ XOR2 cb2,sd1 ) & ( $ XOR2 cb2,sd1 implies $ s1 ) & ( $ l2 implies $ AND2 cb1,p1 ) & ( $ AND2 cb1,p1 implies $ l2 ) & ( $ t2 implies $ NOR2 l2,q1 ) & ( $ NOR2 l2,q1 implies $ t2 ) & ( $ s2 implies $ XOR2 t2,sd2 ) & ( $ XOR2 t2,sd2 implies $ s2 ) & ( $ l3 implies $ AND2 q1,p2 ) & ( $ AND2 q1,p2 implies $ l3 ) & ( $ m3 implies $ AND3 p2,p1,cb1 ) & ( $ AND3 p2,p1,cb1 implies $ m3 ) & ( $ t3 implies $ NOR3 l3,m3,q2 ) & ( $ NOR3 l3,m3,q2 implies $ t3 ) & ( $ s3 implies $ XOR2 t3,sd3 ) & ( $ XOR2 t3,sd3 implies $ s3 ) & ( $ l4 implies $ AND2 q2,p3 ) & ( $ AND2 q2,p3 implies $ l4 ) & ( $ m4 implies $ AND3 q1,p3,p2 ) & ( $ AND3 q1,p3,p2 implies $ m4 ) & ( $ n4 implies $ AND4 p3,p2,p1,cb1 ) & ( $ AND4 p3,p2,p1,cb1 implies $ n4 ) & ( $ t4 implies $ NOR4 l4,m4,n4,q3 ) & ( $ NOR4 l4,m4,n4,q3 implies $ t4 ) & ( $ s4 implies $ XOR2 t4,sd4 ) & ( $ XOR2 t4,sd4 implies $ s4 ) & ( $ l5 implies $ AND2 q3,p4 ) & ( $ AND2 q3,p4 implies $ l5 ) & ( $ m5 implies $ AND3 q2,p4,p3 ) & ( $ AND3 q2,p4,p3 implies $ m5 ) & ( $ n5 implies $ AND4 q1,p4,p3,p2 ) & ( $ AND4 q1,p4,p3,p2 implies $ n5 ) & ( $ o5 implies $ AND5 p4,p3,p2,p1,cb1 ) & ( $ AND5 p4,p3,p2,p1,cb1 implies $ o5 ) & ( $ c4 implies $ NOR5 q4,l5,m5,n5,o5 ) & ( $ NOR5 q4,l5,m5,n5,o5 implies $ c4 ) & not ( ( $ s1 implies $ ADD1 x1,y1,c1 ) & ( $ ADD1 x1,y1,c1 implies $ s1 ) & ( $ s2 implies $ ADD2 x2,y2,x1,y1,c1 ) & ( $ ADD2 x2,y2,x1,y1,c1 implies $ s2 ) & ( $ s3 implies $ ADD3 x3,y3,x2,y2,x1,y1,c1 ) & ( $ ADD3 x3,y3,x2,y2,x1,y1,c1 implies $ s3 ) & ( $ s4 implies $ ADD4 x4,y4,x3,y3,x2,y2,x1,y1,c1 ) & ( $ ADD4 x4,y4,x3,y3,x2,y2,x1,y1,c1 implies $ s4 ) & ( $ c4 implies $ CARR4 x4,y4,x3,y3,x2,y2,x1,y1,c1 ) & ( $ CARR4 x4,y4,x3,y3,x2,y2,x1,y1,c1 implies $ c4 ) ) )
proof end;