:: On the Calculus of Binary Arithmetics
:: by Shunichi Kobayashi
::
:: Received August 23, 2003
:: Copyright (c) 2003 Association of Mizar Users

begin

definition

let x, y be Element of BOOLEAN ;
:: original: 'nand'
redefine func x 'nand' y -> Element of BOOLEAN ;
correctness
coherence
x 'nand' y is Element of BOOLEAN ;

proof end;

end;

definition

let x, y be Element of BOOLEAN ;
:: original: 'nor'
redefine func x 'nor' y -> Element of BOOLEAN ;
correctness
coherence
x 'nor' y is Element of BOOLEAN ;

proof end;

end;

definition

let x, y be boolean set ;
canceled;
canceled;
redefine func x <=> y equals :: BINARI_5:def 3
'not' (x 'xor' y);
correctness
compatibility
for b₁ being set holds
( b₁ = x <=> y iff b₁ = 'not' (x 'xor' y) );
;

end;

:: deftheorem BINARI_5:def 1 :

canceled;

:: deftheorem BINARI_5:def 2 :

canceled;

:: deftheorem defines <=> BINARI_5:def 3 :

for x, y being boolean set holds x <=> y = 'not' (x 'xor' y);

definition

let x, y be Element of BOOLEAN ;
:: original: <=>
redefine func x <=> y -> Element of BOOLEAN ;
correctness
coherence
x <=> y is Element of BOOLEAN ;

proof end;

end;

theorem :: BINARI_5:1

for x being boolean set holds TRUE 'nand' x = 'not' x ;

theorem :: BINARI_5:2

for x being boolean set holds FALSE 'nand' x = TRUE ;

theorem :: BINARI_5:3

for x being boolean set holds
( x 'nand' x = 'not' x & 'not' (x 'nand' x) = x ) ;

theorem :: BINARI_5:4

for x, y being boolean set holds 'not' (x 'nand' y) = x '&' y ;

theorem :: BINARI_5:5

for x being boolean set holds
( x 'nand' ('not' x) = TRUE & 'not' (x 'nand' ('not' x)) = FALSE ) by XBOOLEAN:135, XBOOLEAN:138;

theorem :: BINARI_5:6

for x, y, z being boolean set holds x 'nand' (y '&' z) = 'not' ((x '&' y) '&' z) ;

theorem :: BINARI_5:7

for x, y, z being boolean set holds x 'nand' (y '&' z) = (x '&' y) 'nand' z ;

theorem :: BINARI_5:8

canceled;

theorem :: BINARI_5:9

canceled;

theorem :: BINARI_5:10

for x being boolean set holds TRUE 'nor' x = FALSE ;

theorem :: BINARI_5:11

for x being boolean set holds FALSE 'nor' x = 'not' x ;

theorem :: BINARI_5:12

for x being boolean set holds
( x 'nor' x = 'not' x & 'not' (x 'nor' x) = x ) ;

theorem :: BINARI_5:13

for x, y being boolean set holds 'not' (x 'nor' y) = x 'or' y ;

theorem :: BINARI_5:14

for x being boolean set holds
( x 'nor' ('not' x) = FALSE & 'not' (x 'nor' ('not' x)) = TRUE ) by XBOOLEAN:134, XBOOLEAN:138;

theorem :: BINARI_5:15

canceled;

theorem :: BINARI_5:16

for x, y, z being boolean set holds x 'nor' (y 'or' z) = 'not' ((x 'or' y) 'or' z) ;

theorem :: BINARI_5:17

for x being boolean set holds TRUE <=> x = x ;

theorem :: BINARI_5:18

for x being boolean set holds FALSE <=> x = 'not' x ;

theorem :: BINARI_5:19

for x being boolean set holds
( x <=> x = TRUE & 'not' (x <=> x) = FALSE ) by XBOOLEAN:125, XBOOLEAN:143;

theorem :: BINARI_5:20

for x, y being boolean set holds 'not' (x <=> y) = x 'xor' y ;

theorem :: BINARI_5:21

for x being boolean set holds
( x <=> ('not' x) = FALSE & 'not' (x <=> ('not' x)) = TRUE ) by XBOOLEAN:129, XBOOLEAN:142;

theorem :: BINARI_5:22

for x, y, z being boolean set holds
( x <= y => z iff x '&' y <= z )

proof end;

theorem :: BINARI_5:23

for x, y being boolean set holds x <=> y = (x => y) '&' (y => x) ;

theorem :: BINARI_5:24

canceled;

theorem :: BINARI_5:25

canceled;

theorem :: BINARI_5:26

canceled;

theorem :: BINARI_5:27

canceled;

theorem :: BINARI_5:28

for x, y being boolean set holds x => y = ('not' y) => ('not' x) ;

theorem :: BINARI_5:29

for x, y being boolean set holds x <=> y = ('not' x) <=> ('not' y) ;

theorem :: BINARI_5:30

canceled;

theorem :: BINARI_5:31

canceled;

theorem :: BINARI_5:32

canceled;

theorem :: BINARI_5:33

canceled;

theorem :: BINARI_5:34

for x, y being boolean set st x = TRUE & x => y = TRUE holds
y = TRUE ;

theorem :: BINARI_5:35

for y, x being boolean set st y = TRUE holds
x => y = TRUE ;

theorem :: BINARI_5:36

for x, y being boolean set st 'not' x = TRUE holds
x => y = TRUE ;

theorem :: BINARI_5:37

canceled;

theorem :: BINARI_5:38

canceled;

theorem :: BINARI_5:39

canceled;

theorem :: BINARI_5:40

canceled;

theorem :: BINARI_5:41

canceled;

theorem :: BINARI_5:42

canceled;

theorem :: BINARI_5:43

canceled;

theorem :: BINARI_5:44

canceled;

theorem :: BINARI_5:45

canceled;

theorem :: BINARI_5:46

canceled;

theorem :: BINARI_5:47

canceled;

theorem :: BINARI_5:48

canceled;

theorem :: BINARI_5:49

canceled;

theorem :: BINARI_5:50

canceled;

theorem :: BINARI_5:51

for z, y, x being boolean set st z => (y => x) = TRUE holds
y => (z => x) = TRUE ;

theorem :: BINARI_5:52

for z, y, x being boolean set st z => (y => x) = TRUE & y = TRUE holds
z => x = TRUE ;

theorem :: BINARI_5:53

for z, y, x being boolean set st z => (y => x) = TRUE & y = TRUE & z = TRUE holds
x = TRUE ;