:: GATE_1 semantic presentation

begin

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

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

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

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

theorem :: GATE_1:1
( NOT1 {{}} = {} & NOT1 {} = {{}} ) by Def1;

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


theorem :: GATE_1:3
not NOT1 {} is empty ;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: GATE_1:7
for a being set holds XOR2 (a,a) is empty
proof
let a be set ; ::_thesis: XOR2 (a,a) is empty
 ( ( ( not a is empty & a is empty ) or ( a is empty & not a is empty ) ) iff not XOR2 (a,a) is empty ) ;
hence  XOR2 (a,a) is empty ; ::_thesis: verum
end;

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

theorem :: GATE_1:9
for a, b being set holds
( not XOR2 (a,b) is empty iff not XOR2 (b,a) is empty ) ;

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

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

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

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

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

theorem :: GATE_1:10
for a, b being set holds
( not EQV2 (a,b) is empty iff ( not a is empty iff not b is empty ) ) ;

theorem :: GATE_1:11
for a, b being set holds
( not EQV2 (a,b) is empty iff XOR2 (a,b) is empty )
proof
let a, b be set ; ::_thesis: ( not EQV2 (a,b) is empty iff XOR2 (a,b) is empty )
 ( not EQV2 (a,b) is empty iff ( not a is empty iff not b is empty ) ) ;
hence  ( not EQV2 (a,b) is empty iff XOR2 (a,b) is empty ) ; ::_thesis: verum
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

registration
let a, b be non empty set ;
let c be set ;
cluster MAJ3 (a,b,c) ->  non empty ;
coherence
 not MAJ3 (a,b,c) is empty by Def11;
cluster MAJ3 (a,c,b) ->  non empty ;
coherence
 not MAJ3 (a,c,b) is empty by Def11;
cluster MAJ3 (c,a,b) ->  non empty ;
coherence
 not MAJ3 (c,a,b) is empty by Def11;
end;

registration
let a, b be empty set ;
let c be set ;
cluster MAJ3 (a,b,c) ->  empty ;
coherence
 MAJ3 (a,b,c) is empty by Def11;
cluster MAJ3 (a,c,b) ->  empty ;
coherence
 MAJ3 (a,c,b) is empty by Def11;
cluster MAJ3 (c,a,b) ->  empty ;
coherence
 MAJ3 (c,a,b) is empty by Def11;
end;

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

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

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

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

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

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

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

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

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

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

definition
let a, b, c, d be set ;
func OR4 (a,b,c,d) ->  set  equals :Def15: :: GATE_1:def 15
 NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty )
otherwise  {} ;
correctness
coherence
( ( ( not a is empty or not b is empty or not c is empty or not d is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or {} is set ) );
consistency
for b1 being set holds verum;
;
end;

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

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

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

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

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

definition
let a, b, c, d be set ;
func NOR4 (a,b,c,d) ->  set  equals :Def17: :: GATE_1:def 17
 NOT1 {} if ( a is empty & b is empty & c is empty & d is empty )
otherwise  {} ;
correctness
coherence
( ( not a is empty or not b is empty or not c is empty or not d is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

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

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

definition
let a, b, c, d, e be set ;
func AND5 (a,b,c,d,e) ->  set  equals :Def18: :: GATE_1:def 18
 NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty )
otherwise  {} ;
correctness
coherence
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def18 defines AND5 GATE_1:def_18_:_
 for a, b, c, d, e being set holds
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty implies AND5 (a,b,c,d,e) = NOT1 {} ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies AND5 (a,b,c,d,e) = {} ) );

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

definition
let a, b, c, d, e be set ;
func OR5 (a,b,c,d,e) ->  set  equals :Def19: :: GATE_1:def 19
 NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty )
otherwise  {} ;
correctness
coherence
( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def19 defines OR5 GATE_1:def_19_:_
 for a, b, c, d, e being set holds
( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) implies OR5 (a,b,c,d,e) = NOT1 {} ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or OR5 (a,b,c,d,e) = {} ) );

theorem :: GATE_1:25
for a, b, c, d, e being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) iff not OR5 (a,b,c,d,e) is empty ) by Def19;

definition
let a, b, c, d, e be set ;
func NAND5 (a,b,c,d,e) ->  set  equals :Def20: :: GATE_1:def 20
 NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty )
otherwise  {} ;
correctness
coherence
( ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def20 defines NAND5 GATE_1:def_20_:_
 for a, b, c, d, e being set holds
( ( ( a is empty or b is empty or c is empty or d is empty or e is empty ) implies NAND5 (a,b,c,d,e) = NOT1 {} ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty implies NAND5 (a,b,c,d,e) = {} ) );

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

definition
let a, b, c, d, e be set ;
func NOR5 (a,b,c,d,e) ->  set  equals :Def21: :: GATE_1:def 21
 NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty )
otherwise  {} ;
correctness
coherence
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def21 defines NOR5 GATE_1:def_21_:_
 for a, b, c, d, e being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or NOR5 (a,b,c,d,e) = NOT1 {} ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty ) implies NOR5 (a,b,c,d,e) = {} ) );

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

definition
let a, b, c, d, e, f be set ;
func AND6 (a,b,c,d,e,f) ->  set  equals :Def22: :: GATE_1:def 22
 NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty )
otherwise  {} ;
correctness
coherence
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def22 defines AND6 GATE_1:def_22_:_
 for a, b, c, d, e, f being set holds
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies AND6 (a,b,c,d,e,f) = NOT1 {} ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies AND6 (a,b,c,d,e,f) = {} ) );

theorem :: GATE_1:28
for a, b, c, d, e, f being set holds
( not AND6 (a,b,c,d,e,f) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty ) ) by Def22;

definition
let a, b, c, d, e, f be set ;
func OR6 (a,b,c,d,e,f) ->  set  equals :Def23: :: GATE_1:def 23
 NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty )
otherwise  {} ;
correctness
coherence
( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def23 defines OR6 GATE_1:def_23_:_
 for a, b, c, d, e, f being set holds
( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) implies OR6 (a,b,c,d,e,f) = NOT1 {} ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or OR6 (a,b,c,d,e,f) = {} ) );

theorem :: GATE_1:29
for a, b, c, d, e, f being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) iff not OR6 (a,b,c,d,e,f) is empty ) by Def23;

definition
let a, b, c, d, e, f be set ;
func NAND6 (a,b,c,d,e,f) ->  set  equals :Def24: :: GATE_1:def 24
 NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty )
otherwise  {} ;
correctness
coherence
( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def24 defines NAND6 GATE_1:def_24_:_
 for a, b, c, d, e, f being set holds
( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty ) implies NAND6 (a,b,c,d,e,f) = NOT1 {} ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty implies NAND6 (a,b,c,d,e,f) = {} ) );

theorem :: GATE_1:30
for a, b, c, d, e, f being set holds
( not NAND6 (a,b,c,d,e,f) is empty & not a is empty & not b is empty & not c is empty & not d is empty & not e is empty iff f is empty ) by Def24;

definition
let a, b, c, d, e, f be set ;
func NOR6 (a,b,c,d,e,f) ->  set  equals :Def25: :: GATE_1:def 25
 NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty )
otherwise  {} ;
correctness
coherence
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def25 defines NOR6 GATE_1:def_25_:_
 for a, b, c, d, e, f being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or NOR6 (a,b,c,d,e,f) = NOT1 {} ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty ) implies NOR6 (a,b,c,d,e,f) = {} ) );

theorem :: GATE_1:31
for a, b, c, d, e, f being set holds
( not NOR6 (a,b,c,d,e,f) is empty iff ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty ) ) by Def25;

definition
let a, b, c, d, e, f, g be set ;
func AND7 (a,b,c,d,e,f,g) ->  set  equals :Def26: :: GATE_1:def 26
 NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty )
otherwise  {} ;
correctness
coherence
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def26 defines AND7 GATE_1:def_26_:_
 for a, b, c, d, e, f, g being set holds
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty implies AND7 (a,b,c,d,e,f,g) = NOT1 {} ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty ) implies AND7 (a,b,c,d,e,f,g) = {} ) );

theorem :: GATE_1:32
for a, b, c, d, e, f, g being set holds
( not AND7 (a,b,c,d,e,f,g) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty ) ) by Def26;

definition
let a, b, c, d, e, f, g be set ;
func OR7 (a,b,c,d,e,f,g) ->  set  equals :Def27: :: GATE_1:def 27
 NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty )
otherwise  {} ;
correctness
coherence
( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def27 defines OR7 GATE_1:def_27_:_
 for a, b, c, d, e, f, g being set holds
( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) implies OR7 (a,b,c,d,e,f,g) = NOT1 {} ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or OR7 (a,b,c,d,e,f,g) = {} ) );

theorem :: GATE_1:33
for a, b, c, d, e, f, g being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) iff not OR7 (a,b,c,d,e,f,g) is empty ) by Def27;

definition
let a, b, c, d, e, f, g be set ;
func NAND7 (a,b,c,d,e,f,g) ->  set  equals :Def28: :: GATE_1:def 28
 NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty )
otherwise  {} ;
correctness
coherence
( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def28 defines NAND7 GATE_1:def_28_:_
 for a, b, c, d, e, f, g being set holds
( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty ) implies NAND7 (a,b,c,d,e,f,g) = NOT1 {} ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty implies NAND7 (a,b,c,d,e,f,g) = {} ) );

theorem :: GATE_1:34
for a, b, c, d, e, f, g being set holds
( not NAND7 (a,b,c,d,e,f,g) is empty & not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty iff g is empty ) by Def28;

definition
let a, b, c, d, e, f, g be set ;
func NOR7 (a,b,c,d,e,f,g) ->  set  equals :Def29: :: GATE_1:def 29
 NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty & g is empty )
otherwise  {} ;
correctness
coherence
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def29 defines NOR7 GATE_1:def_29_:_
 for a, b, c, d, e, f, g being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or NOR7 (a,b,c,d,e,f,g) = NOT1 {} ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) implies NOR7 (a,b,c,d,e,f,g) = {} ) );

theorem :: GATE_1:35
for a, b, c, d, e, f, g being set holds
( not NOR7 (a,b,c,d,e,f,g) is empty iff ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty & g is empty ) ) by Def29;

definition
let a, b, c, d, e, f, g, h be set ;
func AND8 (a,b,c,d,e,f,g,h) ->  set  equals :Def30: :: GATE_1:def 30
 NOT1 {} if ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty )
otherwise  {} ;
correctness
coherence
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty implies NOT1 {} is set ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def30 defines AND8 GATE_1:def_30_:_
 for a, b, c, d, e, f, g, h being set holds
( ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty implies AND8 (a,b,c,d,e,f,g,h) = NOT1 {} ) & ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty ) implies AND8 (a,b,c,d,e,f,g,h) = {} ) );

theorem :: GATE_1:36
for a, b, c, d, e, f, g, h being set holds
( not AND8 (a,b,c,d,e,f,g,h) is empty iff ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty ) ) by Def30;

definition
let a, b, c, d, e, f, g, h be set ;
func OR8 (a,b,c,d,e,f,g,h) ->  set  equals :Def31: :: GATE_1:def 31
 NOT1 {} if ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty )
otherwise  {} ;
correctness
coherence
( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) implies NOT1 {} is set ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty or {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def31 defines OR8 GATE_1:def_31_:_
 for a, b, c, d, e, f, g, h being set holds
( ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) implies OR8 (a,b,c,d,e,f,g,h) = NOT1 {} ) & ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty or OR8 (a,b,c,d,e,f,g,h) = {} ) );

theorem :: GATE_1:37
for a, b, c, d, e, f, g, h being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) iff not OR8 (a,b,c,d,e,f,g,h) is empty ) by Def31;

definition
let a, b, c, d, e, f, g, h be set ;
func NAND8 (a,b,c,d,e,f,g,h) ->  set  equals :Def32: :: GATE_1:def 32
 NOT1 {} if ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty )
otherwise  {} ;
correctness
coherence
( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty ) implies NOT1 {} is set ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def32 defines NAND8 GATE_1:def_32_:_
 for a, b, c, d, e, f, g, h being set holds
( ( ( a is empty or b is empty or c is empty or d is empty or e is empty or f is empty or g is empty or h is empty ) implies NAND8 (a,b,c,d,e,f,g,h) = NOT1 {} ) & ( not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty & not h is empty implies NAND8 (a,b,c,d,e,f,g,h) = {} ) );

theorem :: GATE_1:38
for a, b, c, d, e, f, g, h being set holds
( not NAND8 (a,b,c,d,e,f,g,h) is empty & not a is empty & not b is empty & not c is empty & not d is empty & not e is empty & not f is empty & not g is empty iff h is empty ) by Def32;

definition
let a, b, c, d, e, f, g, h be set ;
func NOR8 (a,b,c,d,e,f,g,h) ->  set  equals :Def33: :: GATE_1:def 33
 NOT1 {} if ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty & g is empty & h is empty )
otherwise  {} ;
correctness
coherence
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty or NOT1 {} is set ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) implies {} is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def33 defines NOR8 GATE_1:def_33_:_
 for a, b, c, d, e, f, g, h being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty or NOR8 (a,b,c,d,e,f,g,h) = NOT1 {} ) & ( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty or not h is empty ) implies NOR8 (a,b,c,d,e,f,g,h) = {} ) );

theorem :: GATE_1:39
for a, b, c, d, e, f, g, h being set holds
( not NOR8 (a,b,c,d,e,f,g,h) is empty iff ( a is empty & b is empty & c is empty & d is empty & e is empty & f is empty & g is empty & h is empty ) ) by Def33;

begin

theorem :: GATE_1:40
for c1, x1, x2, x3, x4, y1, y2, y3, y4, c2, c3, c4, c5, n1, n2, n3, n4, n, c5b being set st ( not MAJ3 (x1,y1,c1) is empty implies not c2 is empty ) & ( not MAJ3 (x2,y2,c2) is empty implies not c3 is empty ) & ( not MAJ3 (x3,y3,c3) is empty implies not c4 is empty ) & ( not MAJ3 (x4,y4,c4) is empty implies not c5 is empty ) & ( not n1 is empty implies not OR2 (x1,y1) is empty ) & ( not n2 is empty implies not OR2 (x2,y2) is empty ) & ( not n3 is empty implies not OR2 (x3,y3) is empty ) & ( not n4 is empty implies not OR2 (x4,y4) is empty ) & ( not n is empty implies not AND5 (c1,n1,n2,n3,n4) is empty ) & ( not c5b is empty implies not OR2 (c5,n) is empty ) & ( not OR2 (c5,n) is empty implies not c5b is empty ) holds
( not c5 is empty iff not c5b is empty )
proof
let c1, x1, x2, x3, x4, y1, y2, y3, y4, c2, c3, c4, c5, n1, n2, n3, n4, n, c5b be set ; ::_thesis: ( ( 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 ) implies ( not c5 is empty iff not c5b is empty ) )
assume that
A1: ( ( 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 ) ) and
A2: ( not MAJ3 (x4,y4,c4) is empty implies not c5 is empty ) and
A3: ( not n1 is empty implies not OR2 (x1,y1) is empty ) and
A4: ( not n2 is empty implies not OR2 (x2,y2) is empty ) and
A5: ( not n3 is empty implies not OR2 (x3,y3) is empty ) and
A6: ( not n4 is empty implies not OR2 (x4,y4) is empty ) and
A7: ( not n is empty implies not AND5 (c1,n1,n2,n3,n4) is empty ) and
A8: ( not c5b is empty implies not OR2 (c5,n) is empty ) and
A9: ( not OR2 (c5,n) is empty implies not c5b is empty ) ; ::_thesis: ( not c5 is empty iff not c5b is empty )
A10: now__::_thesis:_(_not_n_is_empty_implies_not_MAJ3_(x4,y4,c4)_is_empty_)
assume A11: not n is empty ; ::_thesis: not MAJ3 (x4,y4,c4) is empty
then A12: not c1 is empty by A7, Def18;
A13: ( not x3 is empty or not y3 is empty ) by A5, A7, A11, Def18;
A14: ( not x2 is empty or not y2 is empty ) by A4, A7, A11, Def18;
A15: ( not x4 is empty or not y4 is empty ) by A6, A7, A11, Def18;
 ( not x1 is empty or not y1 is empty ) by A3, A7, A11, Def18;
hence  not MAJ3 (x4,y4,c4) is empty by A1, A12, A14, A13, A15; ::_thesis: verum
end;
thus  ( not c5 is empty implies not c5b is empty ) by A9; ::_thesis: ( not c5b is empty implies not c5 is empty )
assume  not c5b is empty ; ::_thesis: not c5 is empty
hence  not c5 is empty by A2, A8, A10; ::_thesis: verum
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 ) ) )
proof
let 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 be set ; ::_thesis: 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 ) ) )
assume that
A1: ( not q1 is empty iff not NOR2 (x1,y1) is empty ) and
A2: ( not p1 is empty iff not NAND2 (x1,y1) is empty ) and
A3: ( not sd1 is empty iff not MODADD2 (x1,y1) is empty ) and
A4: ( not q2 is empty iff not NOR2 (x2,y2) is empty ) and
A5: ( not p2 is empty iff not NAND2 (x2,y2) is empty ) and
A6: ( not sd2 is empty iff not MODADD2 (x2,y2) is empty ) and
A7: ( not q3 is empty iff not NOR2 (x3,y3) is empty ) and
A8: ( not p3 is empty iff not NAND2 (x3,y3) is empty ) and
A9: ( not sd3 is empty iff not MODADD2 (x3,y3) is empty ) and
A10: ( not q4 is empty iff not NOR2 (x4,y4) is empty ) and
A11: ( not p4 is empty iff not NAND2 (x4,y4) is empty ) and
A12: ( not sd4 is empty iff not MODADD2 (x4,y4) is empty ) and
A13: ( not cb1 is empty iff not NOT1 c1 is empty ) and
A14: ( ( 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 ) ) and
A15: ( not l2 is empty iff not AND2 (cb1,p1) is empty ) and
A16: ( ( 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 ) ) and
A17: ( not l3 is empty iff not AND2 (q1,p2) is empty ) and
A18: ( not m3 is empty iff not AND3 (p2,p1,cb1) is empty ) and
A19: ( ( 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 ) ) and
A20: ( not l4 is empty iff not AND2 (q2,p3) is empty ) and
A21: ( ( 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 ) ) and
A22: ( not l5 is empty iff not AND2 (q3,p4) is empty ) and
A23: ( ( 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 ) ) and
A24: ( not c4 is empty iff not NOR5 (q4,l5,m5,n5,o5) is empty ) ; ::_thesis: ( ( 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 ) )
A25: ( not p1 is empty & not x1 is empty iff y1 is empty ) by A2;
A26: ( not sd1 is empty iff ( ( not x1 is empty or not y1 is empty ) & ( x1 is empty or y1 is empty ) ) ) by A3, Def34;
hereby  ::_thesis: ( ( 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 ) )
assume A27: not s1 is empty ; ::_thesis: not ADD1 (x1,y1,c1) is empty
percases ( ( not c1 is empty & sd1 is empty ) or ( c1 is empty & not sd1 is empty ) ) by A13, A14, A27;
suppose ( not c1 is empty & sd1 is empty ) ; ::_thesis: not ADD1 (x1,y1,c1) is empty
hence  not ADD1 (x1,y1,c1) is empty by A26; ::_thesis: verum
end;
suppose ( c1 is empty & not sd1 is empty ) ; ::_thesis: not ADD1 (x1,y1,c1) is empty
hence  not ADD1 (x1,y1,c1) is empty by A26; ::_thesis: verum
end;
end;
end;
hereby  ::_thesis: ( ( 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 ) )
assume A28: not ADD1 (x1,y1,c1) is empty ; ::_thesis: not s1 is empty
percases ( ( not c1 is empty & sd1 is empty ) or ( c1 is empty & not sd1 is empty ) ) by A26, A28;
suppose ( not c1 is empty & sd1 is empty ) ; ::_thesis: not s1 is empty
hence  not s1 is empty by A13, A14; ::_thesis: verum
end;
suppose ( c1 is empty & not sd1 is empty ) ; ::_thesis: not s1 is empty
hence  not s1 is empty by A13, A14; ::_thesis: verum
end;
end;
end;
A29: ( not q1 is empty iff ( x1 is empty & y1 is empty ) ) by A1;
A30: ( not sd2 is empty iff ( ( not x2 is empty or not y2 is empty ) & ( x2 is empty or y2 is empty ) ) ) by A6, Def34;
hereby  ::_thesis: ( ( 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 ) )
assume A31: not s2 is empty ; ::_thesis: not ADD2 (x2,y2,x1,y1,c1) is empty
percases ( ( ( not c1 is empty or p1 is empty ) & q1 is empty & sd2 is empty ) or ( ( ( c1 is empty & not p1 is empty ) or not q1 is empty ) & not sd2 is empty ) ) by A13, A15, A16, A31;
suppose ( ( not c1 is empty or p1 is empty ) & q1 is empty & sd2 is empty ) ; ::_thesis: not ADD2 (x2,y2,x1,y1,c1) is empty
hence  not ADD2 (x2,y2,x1,y1,c1) is empty by A29, A25, A30; ::_thesis: verum
end;
suppose ( ( ( c1 is empty & not p1 is empty ) or not q1 is empty ) & not sd2 is empty ) ; ::_thesis: not ADD2 (x2,y2,x1,y1,c1) is empty
hence  not ADD2 (x2,y2,x1,y1,c1) is empty by A29, A25, A30; ::_thesis: verum
end;
end;
end;
A32: ( not cb1 is empty iff c1 is empty ) by A13;
hereby  ::_thesis: ( ( 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 ) )
assume A33: not ADD2 (x2,y2,x1,y1,c1) is empty ; ::_thesis: not s2 is empty
percases ( ( l2 is empty & q1 is empty & sd2 is empty ) or ( ( not l2 is empty or not q1 is empty ) & not sd2 is empty ) ) by A15, A29, A25, A30, A32, A33;
suppose ( l2 is empty & q1 is empty & sd2 is empty ) ; ::_thesis: not s2 is empty
hence  not s2 is empty by A16; ::_thesis: verum
end;
suppose ( ( not l2 is empty or not q1 is empty ) & not sd2 is empty ) ; ::_thesis: not s2 is empty
hence  not s2 is empty by A16; ::_thesis: verum
end;
end;
end;
A34: ( not q2 is empty iff ( x2 is empty & y2 is empty ) ) by A4;
A35: ( not p2 is empty & not x2 is empty iff y2 is empty ) by A5;
A36: ( not sd3 is empty iff ( ( not x3 is empty or not y3 is empty ) & ( x3 is empty or y3 is empty ) ) ) by A9, Def34;
hereby  ::_thesis: ( ( 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 ) )
assume A37: not s3 is empty ; ::_thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
percases ( ( l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty ) or ( l3 is empty & m3 is empty & q2 is empty & not x3 is empty & not y3 is empty ) or ( not l3 is empty & not sd3 is empty ) or ( not m3 is empty & not sd3 is empty ) or ( not q2 is empty & not sd3 is empty ) ) by A9, A19, A37, Def13, Def34;
suppose ( l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty ) ; ::_thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
hence  not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A17, A18, A29, A25, A34, A35, A32; ::_thesis: verum
end;
suppose ( l3 is empty & m3 is empty & q2 is empty & not x3 is empty & not y3 is empty ) ; ::_thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
hence  not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A17, A18, A29, A25, A34, A35, A32; ::_thesis: verum
end;
supposeA38: ( not l3 is empty & not sd3 is empty ) ; ::_thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
then A39: ( x2 is empty or y2 is empty ) by A5, A17;
 ( x1 is empty & y1 is empty ) by A1, A17, A38;
hence  not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A36, A38, A39; ::_thesis: verum
end;
supposeA40: ( not m3 is empty & not sd3 is empty ) ; ::_thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
then  c1 is empty by A13, A18;
hence  not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A18, A25, A35, A36, A40; ::_thesis: verum
end;
suppose ( not q2 is empty & not sd3 is empty ) ; ::_thesis: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty
hence  not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty by A34, A36; ::_thesis: verum
end;
end;
end;
hereby  ::_thesis: ( ( 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 ) )
assume A41: not ADD3 (x3,y3,x2,y2,x1,y1,c1) is empty ; ::_thesis: not s3 is empty
percases ( ( l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty ) or ( l3 is empty & m3 is empty & q2 is empty & not x3 is empty & not y3 is empty ) or ( not l3 is empty & not sd3 is empty ) or ( not m3 is empty & not sd3 is empty ) or ( not q2 is empty & not sd3 is empty ) ) by A17, A18, A29, A25, A34, A35, A36, A32, A41;
suppose ( l3 is empty & m3 is empty & q2 is empty & x3 is empty & y3 is empty ) ; ::_thesis: not s3 is empty
hence  not s3 is empty by A9, A19, Def13, Def34; ::_thesis: verum
end;
suppose ( l3 is empty & m3 is empty & q2 is empty & not x3 is empty & not y3 is empty ) ; ::_thesis: not s3 is empty
hence  not s3 is empty by A9, A19, Def13, Def34; ::_thesis: verum
end;
suppose ( not l3 is empty & not sd3 is empty ) ; ::_thesis: not s3 is empty
hence  not s3 is empty by A19, Def13; ::_thesis: verum
end;
suppose ( not m3 is empty & not sd3 is empty ) ; ::_thesis: not s3 is empty
hence  not s3 is empty by A19, Def13; ::_thesis: verum
end;
suppose ( not q2 is empty & not sd3 is empty ) ; ::_thesis: not s3 is empty
hence  not s3 is empty by A19, Def13; ::_thesis: verum
end;
end;
end;
A42: ( not p3 is empty & not x3 is empty iff y3 is empty ) by A8;
A43: ( not sd4 is empty iff ( ( not x4 is empty or not y4 is empty ) & ( x4 is empty or y4 is empty ) ) ) by A12, Def34;
A44: ( not q3 is empty iff ( x3 is empty & y3 is empty ) ) by A7;
hereby  ::_thesis: ( ( 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 ) )
assume A45: not s4 is empty ; ::_thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
percases ( ( l4 is empty & ( q1 is empty or p3 is empty or p2 is empty ) & ( p3 is empty or p2 is empty or p1 is empty or not c1 is empty ) & q3 is empty & sd4 is empty ) or ( not l4 is empty & not sd4 is empty ) or ( not q1 is empty & not p3 is empty & not p2 is empty & not sd4 is empty ) or ( not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty & not sd4 is empty ) or ( not q3 is empty & not sd4 is empty ) ) by A13, A21, A45, Def14, Def17;
suppose ( l4 is empty & ( q1 is empty or p3 is empty or p2 is empty ) & ( p3 is empty or p2 is empty or p1 is empty or not c1 is empty ) & q3 is empty & sd4 is empty ) ; ::_thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A20, A29, A25, A34, A35, A44, A42, A43; ::_thesis: verum
end;
suppose ( not l4 is empty & not sd4 is empty ) ; ::_thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A20, A34, A42, A43; ::_thesis: verum
end;
suppose ( not q1 is empty & not p3 is empty & not p2 is empty & not sd4 is empty ) ; ::_thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A29, A35, A42, A43; ::_thesis: verum
end;
suppose ( not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty & not sd4 is empty ) ; ::_thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A25, A35, A42, A43; ::_thesis: verum
end;
suppose ( not q3 is empty & not sd4 is empty ) ; ::_thesis: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A44, A43; ::_thesis: verum
end;
end;
end;
hereby  ::_thesis: ( not c4 is empty iff not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty )
assume A46: not ADD4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ; ::_thesis: not s4 is empty
thus  not s4 is empty ::_thesis: verum
proof
assume A47: s4 is empty ; ::_thesis: contradiction
percases ( ( l4 is empty & ( q1 is empty or p3 is empty or p2 is empty ) & ( p3 is empty or p2 is empty or p1 is empty or not c1 is empty ) & q3 is empty & not sd4 is empty ) or ( not l4 is empty & sd4 is empty ) or ( not q1 is empty & not p3 is empty & not p2 is empty & sd4 is empty ) or ( not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty & sd4 is empty ) or ( not q3 is empty & sd4 is empty ) ) by A13, A21, A47, Def14, Def17;
suppose ( l4 is empty & ( q1 is empty or p3 is empty or p2 is empty ) & ( p3 is empty or p2 is empty or p1 is empty or not c1 is empty ) & q3 is empty & not sd4 is empty ) ; ::_thesis: contradiction
hence  contradiction by A20, A29, A25, A34, A35, A44, A42, A43, A46; ::_thesis: verum
end;
suppose ( not l4 is empty & sd4 is empty ) ; ::_thesis: contradiction
hence  contradiction by A20, A34, A42, A43, A46; ::_thesis: verum
end;
suppose ( not q1 is empty & not p3 is empty & not p2 is empty & sd4 is empty ) ; ::_thesis: contradiction
hence  contradiction by A29, A35, A42, A43, A46; ::_thesis: verum
end;
suppose ( not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty & sd4 is empty ) ; ::_thesis: contradiction
hence  contradiction by A25, A35, A42, A43, A46; ::_thesis: verum
end;
suppose ( not q3 is empty & sd4 is empty ) ; ::_thesis: contradiction
hence  contradiction by A44, A43, A46; ::_thesis: verum
end;
end;
end;
end;
A48: ( not p4 is empty & not x4 is empty iff y4 is empty ) by A11;
A49: ( not q4 is empty iff ( x4 is empty & y4 is empty ) ) by A10;
now__::_thesis:_(_q4_is_empty_&_l5_is_empty_&_m5_is_empty_&_n5_is_empty_&_o5_is_empty_implies_not_CARR4_(x4,y4,x3,y3,x2,y2,x1,y1,c1)_is_empty_)
assume that
A50: q4 is empty and
A51: l5 is empty and
A52: ( m5 is empty & n5 is empty & o5 is empty ) ; ::_thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
percases ( p4 is empty or p3 is empty or ( p2 is empty & q2 is empty ) or ( p1 is empty & q2 is empty ) or ( not c1 is empty & q1 is empty & q2 is empty ) ) by A13, A23, A52, Def14, Def18;
suppose p4 is empty ; ::_thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A48; ::_thesis: verum
end;
suppose p3 is empty ; ::_thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A42, A49, A50; ::_thesis: verum
end;
suppose ( p2 is empty & q2 is empty ) ; ::_thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A22, A35, A44, A49, A48, A50, A51; ::_thesis: verum
end;
suppose ( p1 is empty & q2 is empty ) ; ::_thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A22, A25, A34, A44, A49, A48, A50, A51; ::_thesis: verum
end;
suppose ( not c1 is empty & q1 is empty & q2 is empty ) ; ::_thesis: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty
hence  not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty by A22, A29, A34, A44, A49, A48, A50, A51; ::_thesis: verum
end;
end;
end;
hence  ( not c4 is empty implies not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ) by A24, Def21; ::_thesis: ( not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty implies not c4 is empty )
assume A53: not CARR4 (x4,y4,x3,y3,x2,y2,x1,y1,c1) is empty ; ::_thesis: not c4 is empty
assume A54: c4 is empty ; ::_thesis: contradiction
percases ( not q4 is empty or ( not q3 is empty & not p4 is empty ) or ( not q2 is empty & not p4 is empty & not p3 is empty ) or ( not q1 is empty & not p4 is empty & not p3 is empty & not p2 is empty ) or ( not p4 is empty & not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty ) ) by A13, A22, A23, A24, A54, Def14, Def18, Def21;
suppose not q4 is empty ; ::_thesis: contradiction
hence  contradiction by A49, A53; ::_thesis: verum
end;
suppose ( not q3 is empty & not p4 is empty ) ; ::_thesis: contradiction
hence  contradiction by A44, A48, A53; ::_thesis: verum
end;
suppose ( not q2 is empty & not p4 is empty & not p3 is empty ) ; ::_thesis: contradiction
hence  contradiction by A34, A42, A48, A53; ::_thesis: verum
end;
suppose ( not q1 is empty & not p4 is empty & not p3 is empty & not p2 is empty ) ; ::_thesis: contradiction
hence  contradiction by A29, A35, A42, A48, A53; ::_thesis: verum
end;
suppose ( not p4 is empty & not p3 is empty & not p2 is empty & not p1 is empty & c1 is empty ) ; ::_thesis: contradiction
hence  contradiction by A25, A35, A42, A48, A53; ::_thesis: verum
end;
end;
end;