:: BINARI_5 semantic presentation

definition

let c₁, c₂ be boolean set ;
func c₁ 'nand' c₂ -> set equals :: BINARI_5:def 1
'not' (a₁ '&' a₂);
correctness ;
commutativity ;

end;

:: deftheorem Def1 defines 'nand' BINARI_5:def 1 :

registration

let c₁, c₂ be boolean set ;
cluster a₁ 'nand' a₂ -> boolean ;
correctness ;

end;

definition

let c₁, c₂ be Element of BOOLEAN ;
redefine func 'nand' as c₁ 'nand' c₂ -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;

end;

definition

let c₁, c₂ be boolean set ;
func c₁ 'nor' c₂ -> set equals :: BINARI_5:def 2
'not' (a₁ 'or' a₂);
correctness ;
commutativity ;

end;

:: deftheorem Def2 defines 'nor' BINARI_5:def 2 :

registration

let c₁, c₂ be boolean set ;
cluster a₁ 'nor' a₂ -> boolean ;
correctness ;

end;

definition

let c₁, c₂ be Element of BOOLEAN ;
redefine func 'nor' as c₁ 'nor' c₂ -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;

end;

definition

let c₁, c₂ be boolean set ;
func c₁ 'xnor' c₂ -> set equals :: BINARI_5:def 3
'not' (a₁ 'xor' a₂);
correctness ;
commutativity ;

end;

:: deftheorem Def3 defines 'xnor' BINARI_5:def 3 :

registration

let c₁, c₂ be boolean set ;
cluster a₁ 'xnor' a₂ -> boolean ;
correctness ;

end;

definition

let c₁, c₂ be Element of BOOLEAN ;
redefine func 'xnor' as c₁ 'xnor' c₂ -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;

end;

theorem Th1: :: BINARI_5:1

for b₁ being boolean set holds TRUE 'nand' b₁ = 'not' b₁ by MARGREL1:50;

theorem Th2: :: BINARI_5:2

for b₁ being boolean set holds FALSE 'nand' b₁ = TRUE

proof end;

theorem Th3: :: BINARI_5:3

for b₁ being boolean set holds
( b₁ 'nand' b₁ = 'not' b₁ & 'not' (b₁ 'nand' b₁) = b₁ )

proof end;

theorem Th4: :: BINARI_5:4

for b₁, b₂ being boolean set holds 'not' (b₁ 'nand' b₂) = b₁ '&' b₂ by MARGREL1:40;

theorem Th5: :: BINARI_5:5

for b₁ being boolean set holds
( b₁ 'nand' ('not' b₁) = TRUE & 'not' (b₁ 'nand' ('not' b₁)) = FALSE )

proof end;

theorem Th6: :: BINARI_5:6

for b₁, b₂, b₃ being boolean set holds b₁ 'nand' (b₂ '&' b₃) = 'not' ((b₁ '&' b₂) '&' b₃) by MARGREL1:52;

theorem Th7: :: BINARI_5:7

for b₁, b₂, b₃ being boolean set holds b₁ 'nand' (b₂ '&' b₃) = (b₁ '&' b₂) 'nand' b₃ by MARGREL1:52;

theorem Th8: :: BINARI_5:8

for b₁, b₂, b₃ being boolean set holds b₁ 'nand' (b₂ 'or' b₃) = ('not' (b₁ '&' b₂)) '&' ('not' (b₁ '&' b₃))

proof end;

theorem Th9: :: BINARI_5:9

for b₁, b₂, b₃ being boolean set holds b₁ 'nand' (b₂ 'xor' b₃) = (b₁ '&' b₂) 'eqv' (b₁ '&' b₃)

proof end;

theorem Th10: :: BINARI_5:10

for b₁ being boolean set holds TRUE 'nor' b₁ = FALSE

proof end;

theorem Th11: :: BINARI_5:11

for b₁ being boolean set holds FALSE 'nor' b₁ = 'not' b₁ by BINARITH:7;

theorem Th12: :: BINARI_5:12

for b₁ being boolean set holds
( b₁ 'nor' b₁ = 'not' b₁ & 'not' (b₁ 'nor' b₁) = b₁ )

proof end;

theorem Th13: :: BINARI_5:13

for b₁, b₂ being boolean set holds 'not' (b₁ 'nor' b₂) = b₁ 'or' b₂ by MARGREL1:40;

theorem Th14: :: BINARI_5:14

for b₁ being boolean set holds
( b₁ 'nor' ('not' b₁) = FALSE & 'not' (b₁ 'nor' ('not' b₁)) = TRUE )

proof end;

theorem Th15: :: BINARI_5:15

for b₁, b₂, b₃ being boolean set holds b₁ 'nor' (b₂ '&' b₃) = ('not' (b₁ 'or' b₂)) 'or' ('not' (b₁ 'or' b₃))

proof end;

theorem Th16: :: BINARI_5:16

for b₁, b₂, b₃ being boolean set holds b₁ 'nor' (b₂ 'or' b₃) = 'not' ((b₁ 'or' b₂) 'or' b₃) by BINARITH:20;

theorem Th17: :: BINARI_5:17

for b₁ being boolean set holds TRUE 'xnor' b₁ = b₁

proof end;

theorem Th18: :: BINARI_5:18

for b₁ being boolean set holds FALSE 'xnor' b₁ = 'not' b₁ by BINARITH:14;

theorem Th19: :: BINARI_5:19

for b₁ being boolean set holds
( b₁ 'xnor' b₁ = TRUE & 'not' (b₁ 'xnor' b₁) = FALSE )

proof end;

theorem Th20: :: BINARI_5:20

for b₁, b₂ being boolean set holds 'not' (b₁ 'xnor' b₂) = b₁ 'xor' b₂ by MARGREL1:40;

theorem Th21: :: BINARI_5:21

for b₁ being boolean set holds
( b₁ 'xnor' ('not' b₁) = FALSE & 'not' (b₁ 'xnor' ('not' b₁)) = TRUE )

proof end;

theorem Th22: :: BINARI_5:22

for b₁, b₂, b₃ being boolean set holds
( b₁ '<' b₂ 'imp' b₃ iff b₁ '&' b₂ '<' b₃ )

proof end;

theorem Th23: :: BINARI_5:23

for b₁, b₂ being boolean set holds b₁ 'eqv' b₂ = (b₁ 'imp' b₂) '&' (b₂ 'imp' b₁)

proof end;

theorem Th24: :: BINARI_5:24

for b₁, b₂ being boolean set holds
( b₁ 'eqv' b₂ = TRUE iff ( b₁ 'imp' b₂ = TRUE & b₂ 'imp' b₁ = TRUE ) )

proof end;

theorem Th25: :: BINARI_5:25

for b₁, b₂ being boolean set st b₁ 'imp' b₂ = TRUE & b₂ 'imp' b₁ = TRUE holds
b₁ = b₂

proof end;

theorem Th26: :: BINARI_5:26

for b₁, b₂, b₃ being boolean set st b₁ 'imp' b₂ = TRUE & b₂ 'imp' b₃ = TRUE holds
b₁ 'imp' b₃ = TRUE

proof end;

theorem Th27: :: BINARI_5:27

for b₁, b₂, b₃ being boolean set st b₁ 'eqv' b₂ = TRUE & b₂ 'eqv' b₃ = TRUE holds
b₁ 'eqv' b₃ = TRUE

proof end;

theorem Th28: :: BINARI_5:28

for b₁, b₂ being boolean set holds b₁ 'imp' b₂ = ('not' b₂) 'imp' ('not' b₁)

proof end;

theorem Th29: :: BINARI_5:29

for b₁, b₂ being boolean set holds b₁ 'eqv' b₂ = ('not' b₁) 'eqv' ('not' b₂)

proof end;

theorem Th30: :: BINARI_5:30

for b₁, b₂, b₃, b₄ being boolean set st b₁ 'eqv' b₂ = TRUE & b₃ 'eqv' b₄ = TRUE holds
(b₁ '&' b₃) 'eqv' (b₂ '&' b₄) = TRUE

proof end;

theorem Th31: :: BINARI_5:31

for b₁, b₂, b₃, b₄ being boolean set st b₁ 'eqv' b₂ = TRUE & b₃ 'eqv' b₄ = TRUE holds
(b₁ 'imp' b₃) 'eqv' (b₂ 'imp' b₄) = TRUE

proof end;

theorem Th32: :: BINARI_5:32

for b₁, b₂, b₃, b₄ being boolean set st b₁ 'eqv' b₂ = TRUE & b₃ 'eqv' b₄ = TRUE holds
(b₁ 'or' b₃) 'eqv' (b₂ 'or' b₄) = TRUE

proof end;

theorem Th33: :: BINARI_5:33

for b₁, b₂, b₃, b₄ being boolean set st b₁ 'eqv' b₂ = TRUE & b₃ 'eqv' b₄ = TRUE holds
(b₁ 'eqv' b₃) 'eqv' (b₂ 'eqv' b₄) = TRUE

proof end;

theorem Th34: :: BINARI_5:34

for b₁, b₂ being boolean set st b₁ = TRUE & b₁ 'imp' b₂ = TRUE holds
b₂ = TRUE

proof end;

theorem Th35: :: BINARI_5:35

for b₁, b₂ being boolean set st b₁ = TRUE holds
b₂ 'imp' b₁ = TRUE

proof end;

theorem Th36: :: BINARI_5:36

for b₁, b₂ being boolean set st 'not' b₁ = TRUE holds
b₁ 'imp' b₂ = TRUE

proof end;

theorem Th37: :: BINARI_5:37

for b₁ being boolean set holds b₁ 'imp' b₁ = TRUE

proof end;

theorem Th38: :: BINARI_5:38

for b₁, b₂ being boolean set st b₁ 'imp' b₂ = TRUE & b₁ 'imp' ('not' b₂) = TRUE holds
'not' b₁ = TRUE

proof end;

theorem Th39: :: BINARI_5:39

for b₁ being boolean set holds (('not' b₁) 'imp' b₁) 'imp' b₁ = TRUE

proof end;

theorem Th40: :: BINARI_5:40

for b₁, b₂, b₃ being boolean set holds (b₁ 'imp' b₂) 'imp' (('not' (b₂ '&' b₃)) 'imp' ('not' (b₁ '&' b₃))) = TRUE

proof end;

theorem Th41: :: BINARI_5:41

for b₁, b₂, b₃ being boolean set holds (b₁ 'imp' b₂) 'imp' ((b₂ 'imp' b₃) 'imp' (b₁ 'imp' b₃)) = TRUE

proof end;

theorem Th42: :: BINARI_5:42

for b₁, b₂, b₃ being boolean set st b₁ 'imp' b₂ = TRUE holds
(b₂ 'imp' b₃) 'imp' (b₁ 'imp' b₃) = TRUE

proof end;

theorem Th43: :: BINARI_5:43

for b₁, b₂ being boolean set holds b₁ 'imp' (b₂ 'imp' b₁) = TRUE

proof end;

theorem Th44: :: BINARI_5:44

for b₁, b₂, b₃ being boolean set holds ((b₁ 'imp' b₂) 'imp' b₃) 'imp' (b₂ 'imp' b₃) = TRUE

proof end;

theorem Th45: :: BINARI_5:45

for b₁, b₂ being boolean set holds b₁ 'imp' ((b₁ 'imp' b₂) 'imp' b₂) = TRUE

proof end;

theorem Th46: :: BINARI_5:46

for b₁, b₂, b₃ being boolean set holds (b₁ 'imp' (b₂ 'imp' b₃)) 'imp' (b₂ 'imp' (b₁ 'imp' b₃)) = TRUE

proof end;

theorem Th47: :: BINARI_5:47

for b₁, b₂, b₃ being boolean set holds (b₁ 'imp' b₂) 'imp' ((b₃ 'imp' b₁) 'imp' (b₃ 'imp' b₂)) = TRUE

proof end;

theorem Th48: :: BINARI_5:48

for b₁, b₂ being boolean set holds (b₁ 'imp' (b₁ 'imp' b₂)) 'imp' (b₁ 'imp' b₂) = TRUE

proof end;

theorem Th49: :: BINARI_5:49

for b₁, b₂, b₃ being boolean set holds (b₁ 'imp' (b₂ 'imp' b₃)) 'imp' ((b₁ 'imp' b₂) 'imp' (b₁ 'imp' b₃)) = TRUE

proof end;

theorem Th50: :: BINARI_5:50

for b₁, b₂ being boolean set st b₁ = TRUE holds
(b₁ 'imp' b₂) 'imp' b₂ = TRUE

proof end;

theorem Th51: :: BINARI_5:51

for b₁, b₂, b₃ being boolean set st b₁ 'imp' (b₂ 'imp' b₃) = TRUE holds
b₂ 'imp' (b₁ 'imp' b₃) = TRUE

proof end;

theorem Th52: :: BINARI_5:52

for b₁, b₂, b₃ being boolean set st b₁ 'imp' (b₂ 'imp' b₃) = TRUE & b₂ = TRUE holds
b₁ 'imp' b₃ = TRUE

proof end;

theorem Th53: :: BINARI_5:53

for b₁, b₂, b₃ being boolean set st b₁ 'imp' (b₂ 'imp' b₃) = TRUE & b₂ = TRUE & b₁ = TRUE holds
b₃ = TRUE

proof end;

theorem Th54: :: BINARI_5:54

for b₁, b₂ being boolean set st b₁ 'imp' (b₁ 'imp' b₂) = TRUE holds
b₁ 'imp' b₂ = TRUE

proof end;

theorem Th55: :: BINARI_5:55

for b₁, b₂, b₃ being boolean set st b₁ 'imp' (b₂ 'imp' b₃) = TRUE holds
(b₁ 'imp' b₂) 'imp' (b₁ 'imp' b₃) = TRUE

proof end;