:: GATE_1 semantic presentation

notation

let c₁ be set ;
antonym $ c₁ for empty c₁;

end;

theorem Th1: :: GATE_1:1

for b₁ being set st b₁ = {{} } holds
$ b₁ ;

theorem Th2: :: GATE_1:2

ex b₁ being set st $ b₁

proof end;

definition

let c₁ be set ;
func NOT1 c₁ -> set equals :Def1: :: GATE_1:def 1
{} if $ a₁
otherwise {{} };
correctness ;

end;

:: deftheorem Def1 defines NOT1 GATE_1:def 1 :

theorem Th3: :: GATE_1:3

canceled;

theorem Th4: :: GATE_1:4

for b₁ being set holds
( $ NOT1 b₁ iff not $ b₁ ) by Def1;

theorem Th5: :: GATE_1:5

$ NOT1 {} by Th4;

definition

let c₁, c₂ be set ;
func AND2 c₁,c₂ -> set equals :Def2: :: GATE_1:def 2
NOT1 {} if ( $ a₁ & $ a₂ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def2 defines AND2 GATE_1:def 2 :

theorem Th6: :: GATE_1:6

for b₁, b₂ being set holds
( $ AND2 b₁,b₂ iff ( $ b₁ & $ b₂ ) ) by Def2, Th5;

definition

let c₁, c₂ be set ;
func OR2 c₁,c₂ -> set equals :Def3: :: GATE_1:def 3
NOT1 {} if ( $ a₁ or $ a₂ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def3 defines OR2 GATE_1:def 3 :

theorem Th7: :: GATE_1:7

for b₁, b₂ being set holds
( ( $ b₁ or $ b₂ ) iff $ OR2 b₁,b₂ ) by Def3, Th5;

definition

let c₁, c₂ be set ;
func XOR2 c₁,c₂ -> set equals :Def4: :: GATE_1:def 4
NOT1 {} if ( ( $ a₁ & not $ a₂ ) or ( not $ a₁ & $ a₂ ) )
otherwise {} ;
correctness ;

end;

:: deftheorem Def4 defines XOR2 GATE_1:def 4 :

theorem Th8: :: GATE_1:8

for b₁, b₂ being set holds
( ( ( $ b₁ & not $ b₂ ) or ( not $ b₁ & $ b₂ ) ) iff $ XOR2 b₁,b₂ ) by Def4, Th5;

theorem Th9: :: GATE_1:9

for b₁ being set holds
( contradiction iff $ XOR2 b₁,b₁ )

proof end;

theorem Th10: :: GATE_1:10

for b₁ being set holds
( $ XOR2 b₁,{} iff $ b₁ ) by Def4, Th5;

theorem Th11: :: GATE_1:11

for b₁, b₂ being set holds
( $ XOR2 b₁,b₂ iff $ XOR2 b₂,b₁ )

proof end;

definition

let c₁, c₂ be set ;
func EQV2 c₁,c₂ -> set equals :Def5: :: GATE_1:def 5
NOT1 {} if ( $ a₁ iff $ a₂ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def5 defines EQV2 GATE_1:def 5 :

theorem Th12: :: GATE_1:12

for b₁, b₂ being set holds
( $ EQV2 b₁,b₂ iff ( $ b₁ iff $ b₂ ) ) by Def5, Th5;

theorem Th13: :: GATE_1:13

for b₁, b₂ being set holds
( $ EQV2 b₁,b₂ iff not $ XOR2 b₁,b₂ )

proof end;

definition

let c₁, c₂ be set ;
func NAND2 c₁,c₂ -> set equals :Def6: :: GATE_1:def 6
NOT1 {} if ( not $ a₁ or not $ a₂ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def6 defines NAND2 GATE_1:def 6 :

theorem Th14: :: GATE_1:14

for b₁, b₂ being set holds
( $ NAND2 b₁,b₂ & $ b₁ iff not $ b₂ ) by Def6, Th5;

definition

let c₁, c₂ be set ;
func NOR2 c₁,c₂ -> set equals :Def7: :: GATE_1:def 7
NOT1 {} if ( not $ a₁ & not $ a₂ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def7 defines NOR2 GATE_1:def 7 :

theorem Th15: :: GATE_1:15

for b₁, b₂ being set holds
( $ NOR2 b₁,b₂ iff ( not $ b₁ & not $ b₂ ) ) by Def7, Th5;

definition

let c₁, c₂, c₃ be set ;
func AND3 c₁,c₂,c₃ -> set equals :Def8: :: GATE_1:def 8
NOT1 {} if ( $ a₁ & $ a₂ & $ a₃ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def8 defines AND3 GATE_1:def 8 :

theorem Th16: :: GATE_1:16

for b₁, b₂, b₃ being set holds
( $ AND3 b₁,b₂,b₃ iff ( $ b₁ & $ b₂ & $ b₃ ) ) by Def8, Th5;

definition

let c₁, c₂, c₃ be set ;
func OR3 c₁,c₂,c₃ -> set equals :Def9: :: GATE_1:def 9
NOT1 {} if ( $ a₁ or $ a₂ or $ a₃ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def9 defines OR3 GATE_1:def 9 :

theorem Th17: :: GATE_1:17

for b₁, b₂, b₃ being set holds
( ( $ b₁ or $ b₂ or $ b₃ ) iff $ OR3 b₁,b₂,b₃ ) by Def9, Th5;

definition

let c₁, c₂, c₃ be set ;
func XOR3 c₁,c₂,c₃ -> set equals :Def10: :: GATE_1:def 10
NOT1 {} if ( ( ( ( $ a₁ & not $ a₂ ) or ( not $ a₁ & $ a₂ ) ) & not $ a₃ ) or ( not ( $ a₁ & not $ a₂ ) & not ( not $ a₁ & $ a₂ ) & $ a₃ ) )
otherwise {} ;
correctness ;

end;

:: deftheorem Def10 defines XOR3 GATE_1:def 10 :

theorem Th18: :: GATE_1:18

for b₁, b₂, b₃ being set holds
( ( ( ( ( $ b₁ & not $ b₂ ) or ( not $ b₁ & $ b₂ ) ) & not $ b₃ ) or ( not ( $ b₁ & not $ b₂ ) & not ( not $ b₁ & $ b₂ ) & $ b₃ ) ) iff $ XOR3 b₁,b₂,b₃ ) by Def10, Th5;

definition

let c₁, c₂, c₃ be set ;
func MAJ3 c₁,c₂,c₃ -> set equals :Def11: :: GATE_1:def 11
NOT1 {} if ( ( $ a₁ & $ a₂ ) or ( $ a₂ & $ a₃ ) or ( $ a₃ & $ a₁ ) )
otherwise {} ;
correctness ;

end;

:: deftheorem Def11 defines MAJ3 GATE_1:def 11 :

theorem Th19: :: GATE_1:19

for b₁, b₂, b₃ being set holds
( ( ( $ b₁ & $ b₂ ) or ( $ b₂ & $ b₃ ) or ( $ b₃ & $ b₁ ) ) iff $ MAJ3 b₁,b₂,b₃ ) by Def11, Th5;

definition

let c₁, c₂, c₃ be set ;
func NAND3 c₁,c₂,c₃ -> set equals :Def12: :: GATE_1:def 12
NOT1 {} if ( not $ a₁ or not $ a₂ or not $ a₃ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def12 defines NAND3 GATE_1:def 12 :

theorem Th20: :: GATE_1:20

for b₁, b₂, b₃ being set holds
( $ NAND3 b₁,b₂,b₃ & $ b₁ & $ b₂ iff not $ b₃ ) by Def12, Th5;

definition

let c₁, c₂, c₃ be set ;
func NOR3 c₁,c₂,c₃ -> set equals :Def13: :: GATE_1:def 13
NOT1 {} if ( not $ a₁ & not $ a₂ & not $ a₃ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def13 defines NOR3 GATE_1:def 13 :

theorem Th21: :: GATE_1:21

for b₁, b₂, b₃ being set holds
( $ NOR3 b₁,b₂,b₃ iff ( not $ b₁ & not $ b₂ & not $ b₃ ) ) by Def13, Th5;

definition

let c₁, c₂, c₃, c₄ be set ;
func AND4 c₁,c₂,c₃,c₄ -> set equals :Def14: :: GATE_1:def 14
NOT1 {} if ( $ a₁ & $ a₂ & $ a₃ & $ a₄ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def14 defines AND4 GATE_1:def 14 :

theorem Th22: :: GATE_1:22

for b₁, b₂, b₃, b₄ being set holds
( $ AND4 b₁,b₂,b₃,b₄ iff ( $ b₁ & $ b₂ & $ b₃ & $ b₄ ) ) by Def14, Th5;

definition

let c₁, c₂, c₃, c₄ be set ;
func OR4 c₁,c₂,c₃,c₄ -> set equals :Def15: :: GATE_1:def 15
NOT1 {} if ( $ a₁ or $ a₂ or $ a₃ or $ a₄ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def15 defines OR4 GATE_1:def 15 :

theorem Th23: :: GATE_1:23

for b₁, b₂, b₃, b₄ being set holds
( ( $ b₁ or $ b₂ or $ b₃ or $ b₄ ) iff $ OR4 b₁,b₂,b₃,b₄ ) by Def15, Th5;

definition

let c₁, c₂, c₃, c₄ be set ;
func NAND4 c₁,c₂,c₃,c₄ -> set equals :Def16: :: GATE_1:def 16
NOT1 {} if ( not $ a₁ or not $ a₂ or not $ a₃ or not $ a₄ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def16 defines NAND4 GATE_1:def 16 :

theorem Th24: :: GATE_1:24

for b₁, b₂, b₃, b₄ being set holds
( $ NAND4 b₁,b₂,b₃,b₄ & $ b₁ & $ b₂ & $ b₃ iff not $ b₄ ) by Def16, Th5;

definition

let c₁, c₂, c₃, c₄ be set ;
func NOR4 c₁,c₂,c₃,c₄ -> set equals :Def17: :: GATE_1:def 17
NOT1 {} if ( not $ a₁ & not $ a₂ & not $ a₃ & not $ a₄ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def17 defines NOR4 GATE_1:def 17 :

theorem Th25: :: GATE_1:25

for b₁, b₂, b₃, b₄ being set holds
( $ NOR4 b₁,b₂,b₃,b₄ iff ( not $ b₁ & not $ b₂ & not $ b₃ & not $ b₄ ) ) by Def17, Th5;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
func AND5 c₁,c₂,c₃,c₄,c₅ -> set equals :Def18: :: GATE_1:def 18
NOT1 {} if ( $ a₁ & $ a₂ & $ a₃ & $ a₄ & $ a₅ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def18 defines AND5 GATE_1:def 18 :

theorem Th26: :: GATE_1:26

for b₁, b₂, b₃, b₄, b₅ being set holds
( $ AND5 b₁,b₂,b₃,b₄,b₅ iff ( $ b₁ & $ b₂ & $ b₃ & $ b₄ & $ b₅ ) ) by Def18, Th5;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
func OR5 c₁,c₂,c₃,c₄,c₅ -> set equals :Def19: :: GATE_1:def 19
NOT1 {} if ( $ a₁ or $ a₂ or $ a₃ or $ a₄ or $ a₅ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def19 defines OR5 GATE_1:def 19 :

theorem Th27: :: GATE_1:27

for b₁, b₂, b₃, b₄, b₅ being set holds
( ( $ b₁ or $ b₂ or $ b₃ or $ b₄ or $ b₅ ) iff $ OR5 b₁,b₂,b₃,b₄,b₅ ) by Def19, Th5;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
func NAND5 c₁,c₂,c₃,c₄,c₅ -> set equals :Def20: :: GATE_1:def 20
NOT1 {} if ( not $ a₁ or not $ a₂ or not $ a₃ or not $ a₄ or not $ a₅ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def20 defines NAND5 GATE_1:def 20 :

theorem Th28: :: GATE_1:28

for b₁, b₂, b₃, b₄, b₅ being set holds
( $ NAND5 b₁,b₂,b₃,b₄,b₅ & $ b₁ & $ b₂ & $ b₃ & $ b₄ iff not $ b₅ ) by Def20, Th5;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
func NOR5 c₁,c₂,c₃,c₄,c₅ -> set equals :Def21: :: GATE_1:def 21
NOT1 {} if ( not $ a₁ & not $ a₂ & not $ a₃ & not $ a₄ & not $ a₅ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def21 defines NOR5 GATE_1:def 21 :

theorem Th29: :: GATE_1:29

for b₁, b₂, b₃, b₄, b₅ being set holds
( $ NOR5 b₁,b₂,b₃,b₄,b₅ iff ( not $ b₁ & not $ b₂ & not $ b₃ & not $ b₄ & not $ b₅ ) ) by Def21, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆ be set ;
func AND6 c₁,c₂,c₃,c₄,c₅,c₆ -> set equals :Def22: :: GATE_1:def 22
NOT1 {} if ( $ a₁ & $ a₂ & $ a₃ & $ a₄ & $ a₅ & $ a₆ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def22 defines AND6 GATE_1:def 22 :

theorem Th30: :: GATE_1:30

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds
( $ AND6 b₁,b₂,b₃,b₄,b₅,b₆ iff ( $ b₁ & $ b₂ & $ b₃ & $ b₄ & $ b₅ & $ b₆ ) ) by Def22, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆ be set ;
func OR6 c₁,c₂,c₃,c₄,c₅,c₆ -> set equals :Def23: :: GATE_1:def 23
NOT1 {} if ( $ a₁ or $ a₂ or $ a₃ or $ a₄ or $ a₅ or $ a₆ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def23 defines OR6 GATE_1:def 23 :

theorem Th31: :: GATE_1:31

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds
( ( $ b₁ or $ b₂ or $ b₃ or $ b₄ or $ b₅ or $ b₆ ) iff $ OR6 b₁,b₂,b₃,b₄,b₅,b₆ ) by Def23, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆ be set ;
func NAND6 c₁,c₂,c₃,c₄,c₅,c₆ -> set equals :Def24: :: GATE_1:def 24
NOT1 {} if ( not $ a₁ or not $ a₂ or not $ a₃ or not $ a₄ or not $ a₅ or not $ a₆ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def24 defines NAND6 GATE_1:def 24 :

theorem Th32: :: GATE_1:32

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds
( $ NAND6 b₁,b₂,b₃,b₄,b₅,b₆ & $ b₁ & $ b₂ & $ b₃ & $ b₄ & $ b₅ iff not $ b₆ ) by Def24, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆ be set ;
func NOR6 c₁,c₂,c₃,c₄,c₅,c₆ -> set equals :Def25: :: GATE_1:def 25
NOT1 {} if ( not $ a₁ & not $ a₂ & not $ a₃ & not $ a₄ & not $ a₅ & not $ a₆ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def25 defines NOR6 GATE_1:def 25 :

theorem Th33: :: GATE_1:33

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds
( $ NOR6 b₁,b₂,b₃,b₄,b₅,b₆ iff ( not $ b₁ & not $ b₂ & not $ b₃ & not $ b₄ & not $ b₅ & not $ b₆ ) ) by Def25, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
func AND7 c₁,c₂,c₃,c₄,c₅,c₆,c₇ -> set equals :Def26: :: GATE_1:def 26
NOT1 {} if ( $ a₁ & $ a₂ & $ a₃ & $ a₄ & $ a₅ & $ a₆ & $ a₇ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def26 defines AND7 GATE_1:def 26 :

theorem Th34: :: GATE_1:34

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds
( $ AND7 b₁,b₂,b₃,b₄,b₅,b₆,b₇ iff ( $ b₁ & $ b₂ & $ b₃ & $ b₄ & $ b₅ & $ b₆ & $ b₇ ) ) by Def26, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
func OR7 c₁,c₂,c₃,c₄,c₅,c₆,c₇ -> set equals :Def27: :: GATE_1:def 27
NOT1 {} if ( $ a₁ or $ a₂ or $ a₃ or $ a₄ or $ a₅ or $ a₆ or $ a₇ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def27 defines OR7 GATE_1:def 27 :

theorem Th35: :: GATE_1:35

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds
( ( $ b₁ or $ b₂ or $ b₃ or $ b₄ or $ b₅ or $ b₆ or $ b₇ ) iff $ OR7 b₁,b₂,b₃,b₄,b₅,b₆,b₇ ) by Def27, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
func NAND7 c₁,c₂,c₃,c₄,c₅,c₆,c₇ -> set equals :Def28: :: GATE_1:def 28
NOT1 {} if ( not $ a₁ or not $ a₂ or not $ a₃ or not $ a₄ or not $ a₅ or not $ a₆ or not $ a₇ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def28 defines NAND7 GATE_1:def 28 :

theorem Th36: :: GATE_1:36

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds
( $ NAND7 b₁,b₂,b₃,b₄,b₅,b₆,b₇ & $ b₁ & $ b₂ & $ b₃ & $ b₄ & $ b₅ & $ b₆ iff not $ b₇ ) by Def28, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
func NOR7 c₁,c₂,c₃,c₄,c₅,c₆,c₇ -> set equals :Def29: :: GATE_1:def 29
NOT1 {} if ( not $ a₁ & not $ a₂ & not $ a₃ & not $ a₄ & not $ a₅ & not $ a₆ & not $ a₇ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def29 defines NOR7 GATE_1:def 29 :

theorem Th37: :: GATE_1:37

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds
( $ NOR7 b₁,b₂,b₃,b₄,b₅,b₆,b₇ iff ( not $ b₁ & not $ b₂ & not $ b₃ & not $ b₄ & not $ b₅ & not $ b₆ & not $ b₇ ) ) by Def29, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇, c₈ be set ;
func AND8 c₁,c₂,c₃,c₄,c₅,c₆,c₇,c₈ -> set equals :Def30: :: GATE_1:def 30
NOT1 {} if ( $ a₁ & $ a₂ & $ a₃ & $ a₄ & $ a₅ & $ a₆ & $ a₇ & $ a₈ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def30 defines AND8 GATE_1:def 30 :

theorem Th38: :: GATE_1:38

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds
( $ AND8 b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈ iff ( $ b₁ & $ b₂ & $ b₃ & $ b₄ & $ b₅ & $ b₆ & $ b₇ & $ b₈ ) ) by Def30, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇, c₈ be set ;
func OR8 c₁,c₂,c₃,c₄,c₅,c₆,c₇,c₈ -> set equals :Def31: :: GATE_1:def 31
NOT1 {} if ( $ a₁ or $ a₂ or $ a₃ or $ a₄ or $ a₅ or $ a₆ or $ a₇ or $ a₈ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def31 defines OR8 GATE_1:def 31 :

theorem Th39: :: GATE_1:39

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds
( ( $ b₁ or $ b₂ or $ b₃ or $ b₄ or $ b₅ or $ b₆ or $ b₇ or $ b₈ ) iff $ OR8 b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈ ) by Def31, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇, c₈ be set ;
func NAND8 c₁,c₂,c₃,c₄,c₅,c₆,c₇,c₈ -> set equals :Def32: :: GATE_1:def 32
NOT1 {} if ( not $ a₁ or not $ a₂ or not $ a₃ or not $ a₄ or not $ a₅ or not $ a₆ or not $ a₇ or not $ a₈ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def32 defines NAND8 GATE_1:def 32 :

theorem Th40: :: GATE_1:40

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds
( $ NAND8 b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈ & $ b₁ & $ b₂ & $ b₃ & $ b₄ & $ b₅ & $ b₆ & $ b₇ iff not $ b₈ ) by Def32, Th5;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇, c₈ be set ;
func NOR8 c₁,c₂,c₃,c₄,c₅,c₆,c₇,c₈ -> set equals :Def33: :: GATE_1:def 33
NOT1 {} if ( not $ a₁ & not $ a₂ & not $ a₃ & not $ a₄ & not $ a₅ & not $ a₆ & not $ a₇ & not $ a₈ )
otherwise {} ;
correctness ;

end;

:: deftheorem Def33 defines NOR8 GATE_1:def 33 :

theorem Th41: :: GATE_1:41

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds
( $ NOR8 b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈ iff ( not $ b₁ & not $ b₂ & not $ b₃ & not $ b₄ & not $ b₅ & not $ b₆ & not $ b₇ & not $ b₈ ) ) by Def33, Th5;

theorem Th42: :: GATE_1:42

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅, b₁₆, b₁₇, b₁₈, b₁₉ being set st ( $ MAJ3 b₂,b₆,b₁ implies $ b₁₀ ) & ( $ MAJ3 b₃,b₇,b₁₀ implies $ b₁₁ ) & ( $ MAJ3 b₄,b₈,b₁₁ implies $ b₁₂ ) & ( $ MAJ3 b₅,b₉,b₁₂ implies $ b₁₃ ) & ( $ b₁₄ implies $ OR2 b₂,b₆ ) & ( $ b₁₅ implies $ OR2 b₃,b₇ ) & ( $ b₁₆ implies $ OR2 b₄,b₈ ) & ( $ b₁₇ implies $ OR2 b₅,b₉ ) & ( $ b₁₈ implies $ AND5 b₁,b₁₄,b₁₅,b₁₆,b₁₇ ) & ( $ b₁₉ implies $ OR2 b₁₃,b₁₈ ) & ( $ OR2 b₁₃,b₁₈ implies $ b₁₉ ) holds
( $ b₁₃ iff $ b₁₉ )

proof end;

definition

let c₁, c₂ be set ;
func MODADD2 c₁,c₂ -> set equals :Def34: :: GATE_1:def 34
NOT1 {} if ( ( $ a₁ or $ a₂ ) & ( not $ a₁ or not $ a₂ ) )
otherwise {} ;
correctness ;

end;

:: deftheorem Def34 defines MODADD2 GATE_1:def 34 :

theorem Th43: :: GATE_1:43

for b₁, b₂ being set holds
( $ MODADD2 b₁,b₂ iff ( ( $ b₁ or $ b₂ ) & ( not $ b₁ or not $ b₂ ) ) ) by Def34, Th5;

notation

let c₁, c₂, c₃ be set ;
synonym ADD1 c₁,c₂,c₃ for XOR3 c₁,c₂,c₃;
synonym CARR1 c₁,c₂,c₃ for MAJ3 c₁,c₂,c₃;

end;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
canceled;
canceled;
func ADD2 c₃,c₄,c₁,c₂,c₅ -> set equals :: GATE_1:def 37
XOR3 a₃,a₄,(CARR1 a₁,a₂,a₅);
correctness ;

end;

:: deftheorem Def35 GATE_1:def 35 :

:: deftheorem Def36 GATE_1:def 36 :

:: deftheorem Def37 defines ADD2 GATE_1:def 37 :

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
func CARR2 c₃,c₄,c₁,c₂,c₅ -> set equals :: GATE_1:def 38
MAJ3 a₃,a₄,(CARR1 a₁,a₂,a₅);
correctness ;

end;

:: deftheorem Def38 defines CARR2 GATE_1:def 38 :

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
func ADD3 c₅,c₆,c₃,c₄,c₁,c₂,c₇ -> set equals :: GATE_1:def 39
XOR3 a₅,a₆,(CARR2 a₃,a₄,a₁,a₂,a₇);
correctness ;

end;

:: deftheorem Def39 defines ADD3 GATE_1:def 39 :

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
func CARR3 c₅,c₆,c₃,c₄,c₁,c₂,c₇ -> set equals :: GATE_1:def 40
MAJ3 a₅,a₆,(CARR2 a₃,a₄,a₁,a₂,a₇);
correctness ;

end;

:: deftheorem Def40 defines CARR3 GATE_1:def 40 :

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇, c₈, c₉ be set ;
func ADD4 c₇,c₈,c₅,c₆,c₃,c₄,c₁,c₂,c₉ -> set equals :: GATE_1:def 41
XOR3 a₇,a₈,(CARR3 a₅,a₆,a₃,a₄,a₁,a₂,a₉);
correctness ;

end;

:: deftheorem Def41 defines ADD4 GATE_1:def 41 :

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇, c₈, c₉ be set ;
func CARR4 c₇,c₈,c₅,c₆,c₃,c₄,c₁,c₂,c₉ -> set equals :: GATE_1:def 42
MAJ3 a₇,a₈,(CARR3 a₅,a₆,a₃,a₄,a₁,a₂,a₉);
correctness ;

end;

:: deftheorem Def42 defines CARR4 GATE_1:def 42 :

theorem Th44: :: GATE_1:44

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅, b₁₆, b₁₇, b₁₈, b₁₉, b₂₀, b₂₁, b₂₂, b₂₃, b₂₄, b₂₅, b₂₆, b₂₇, b₂₈, b₂₉, b₃₀, b₃₁, b₃₂, b₃₃, b₃₄, b₃₅, b₃₆, b₃₇, b₃₈, b₃₉, b₄₀, b₄₁ being set holds
not ( ( $ b₁₁ implies $ NOR2 b₂,b₃ ) & ( $ NOR2 b₂,b₃ implies $ b₁₁ ) & ( $ b₁₂ implies $ NAND2 b₂,b₃ ) & ( $ NAND2 b₂,b₃ implies $ b₁₂ ) & ( $ b₁₃ implies $ MODADD2 b₂,b₃ ) & ( $ MODADD2 b₂,b₃ implies $ b₁₃ ) & ( $ b₁₄ implies $ NOR2 b₄,b₅ ) & ( $ NOR2 b₄,b₅ implies $ b₁₄ ) & ( $ b₁₅ implies $ NAND2 b₄,b₅ ) & ( $ NAND2 b₄,b₅ implies $ b₁₅ ) & ( $ b₁₆ implies $ MODADD2 b₄,b₅ ) & ( $ MODADD2 b₄,b₅ implies $ b₁₆ ) & ( $ b₁₇ implies $ NOR2 b₆,b₇ ) & ( $ NOR2 b₆,b₇ implies $ b₁₇ ) & ( $ b₁₈ implies $ NAND2 b₆,b₇ ) & ( $ NAND2 b₆,b₇ implies $ b₁₈ ) & ( $ b₁₉ implies $ MODADD2 b₆,b₇ ) & ( $ MODADD2 b₆,b₇ implies $ b₁₉ ) & ( $ b₂₀ implies $ NOR2 b₈,b₉ ) & ( $ NOR2 b₈,b₉ implies $ b₂₀ ) & ( $ b₂₁ implies $ NAND2 b₈,b₉ ) & ( $ NAND2 b₈,b₉ implies $ b₂₁ ) & ( $ b₂₂ implies $ MODADD2 b₈,b₉ ) & ( $ MODADD2 b₈,b₉ implies $ b₂₂ ) & ( $ b₂₃ implies $ NOT1 b₁ ) & ( $ NOT1 b₁ implies $ b₂₃ ) & ( $ b₂₄ implies $ NOT1 b₂₃ ) & ( $ NOT1 b₂₃ implies $ b₂₄ ) & ( $ b₃₈ implies $ XOR2 b₂₄,b₁₃ ) & ( $ XOR2 b₂₄,b₁₃ implies $ b₃₈ ) & ( $ b₂₅ implies $ AND2 b₂₃,b₁₂ ) & ( $ AND2 b₂₃,b₁₂ implies $ b₂₅ ) & ( $ b₂₆ implies $ NOR2 b₂₅,b₁₁ ) & ( $ NOR2 b₂₅,b₁₁ implies $ b₂₆ ) & ( $ b₃₉ implies $ XOR2 b₂₆,b₁₆ ) & ( $ XOR2 b₂₆,b₁₆ implies $ b₃₉ ) & ( $ b₂₇ implies $ AND2 b₁₁,b₁₅ ) & ( $ AND2 b₁₁,b₁₅ implies $ b₂₇ ) & ( $ b₂₈ implies $ AND3 b₁₅,b₁₂,b₂₃ ) & ( $ AND3 b₁₅,b₁₂,b₂₃ implies $ b₂₈ ) & ( $ b₂₉ implies $ NOR3 b₂₇,b₂₈,b₁₄ ) & ( $ NOR3 b₂₇,b₂₈,b₁₄ implies $ b₂₉ ) & ( $ b₄₀ implies $ XOR2 b₂₉,b₁₉ ) & ( $ XOR2 b₂₉,b₁₉ implies $ b₄₀ ) & ( $ b₃₀ implies $ AND2 b₁₄,b₁₈ ) & ( $ AND2 b₁₄,b₁₈ implies $ b₃₀ ) & ( $ b₃₁ implies $ AND3 b₁₁,b₁₈,b₁₅ ) & ( $ AND3 b₁₁,b₁₈,b₁₅ implies $ b₃₁ ) & ( $ b₃₂ implies $ AND4 b₁₈,b₁₅,b₁₂,b₂₃ ) & ( $ AND4 b₁₈,b₁₅,b₁₂,b₂₃ implies $ b₃₂ ) & ( $ b₃₃ implies $ NOR4 b₃₀,b₃₁,b₃₂,b₁₇ ) & ( $ NOR4 b₃₀,b₃₁,b₃₂,b₁₇ implies $ b₃₃ ) & ( $ b₄₁ implies $ XOR2 b₃₃,b₂₂ ) & ( $ XOR2 b₃₃,b₂₂ implies $ b₄₁ ) & ( $ b₃₄ implies $ AND2 b₁₇,b₂₁ ) & ( $ AND2 b₁₇,b₂₁ implies $ b₃₄ ) & ( $ b₃₅ implies $ AND3 b₁₄,b₂₁,b₁₈ ) & ( $ AND3 b₁₄,b₂₁,b₁₈ implies $ b₃₅ ) & ( $ b₃₆ implies $ AND4 b₁₁,b₂₁,b₁₈,b₁₅ ) & ( $ AND4 b₁₁,b₂₁,b₁₈,b₁₅ implies $ b₃₆ ) & ( $ b₃₇ implies $ AND5 b₂₁,b₁₈,b₁₅,b₁₂,b₂₃ ) & ( $ AND5 b₂₁,b₁₈,b₁₅,b₁₂,b₂₃ implies $ b₃₇ ) & ( $ b₁₀ implies $ NOR5 b₂₀,b₃₄,b₃₅,b₃₆,b₃₇ ) & ( $ NOR5 b₂₀,b₃₄,b₃₅,b₃₆,b₃₇ implies $ b₁₀ ) & not ( ( $ b₃₈ implies $ ADD1 b₂,b₃,b₁ ) & ( $ ADD1 b₂,b₃,b₁ implies $ b₃₈ ) & ( $ b₃₉ implies $ ADD2 b₄,b₅,b₂,b₃,b₁ ) & ( $ ADD2 b₄,b₅,b₂,b₃,b₁ implies $ b₃₉ ) & ( $ b₄₀ implies $ ADD3 b₆,b₇,b₄,b₅,b₂,b₃,b₁ ) & ( $ ADD3 b₆,b₇,b₄,b₅,b₂,b₃,b₁ implies $ b₄₀ ) & ( $ b₄₁ implies $ ADD4 b₈,b₉,b₆,b₇,b₄,b₅,b₂,b₃,b₁ ) & ( $ ADD4 b₈,b₉,b₆,b₇,b₄,b₅,b₂,b₃,b₁ implies $ b₄₁ ) & ( $ b₁₀ implies $ CARR4 b₈,b₉,b₆,b₇,b₄,b₅,b₂,b₃,b₁ ) & ( $ CARR4 b₈,b₉,b₆,b₇,b₄,b₅,b₂,b₃,b₁ implies $ b₁₀ ) ) )

proof end;