:: BINARI_5 semantic presentation

definition

let x, y be boolean set ;
func x 'nand' y -> set equals :: BINARI_5:def 1
'not' (x '&' y);
correctness ;
commutativity ;

end;

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

registration

let x, y be boolean set ;
cluster x 'nand' y -> boolean ;
correctness ;

end;

definition

let x, y be Element of BOOLEAN ;
:: original: 'nand'
redefine func x 'nand' y -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;

end;

definition

let x, y be boolean set ;
func x 'nor' y -> set equals :: BINARI_5:def 2
'not' (x 'or' y);
correctness ;
commutativity ;

end;

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

registration

let x, y be boolean set ;
cluster x 'nor' y -> boolean ;
correctness ;

end;

definition

let x, y be Element of BOOLEAN ;
:: original: 'nor'
redefine func x 'nor' y -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;

end;

definition

let x, y be boolean set ;
func x 'xnor' y -> set equals :: BINARI_5:def 3
'not' (x 'xor' y);
correctness ;
commutativity ;

end;

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

registration

let x, y be boolean set ;
cluster x 'xnor' y -> boolean ;
correctness ;

end;

definition

let x, y be Element of BOOLEAN ;
:: original: 'xnor'
redefine func x 'xnor' y -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;

end;

theorem :: BINARI_5:1

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

theorem :: BINARI_5:2

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

proof end;

theorem :: BINARI_5:3

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

proof end;

theorem :: BINARI_5:4

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

theorem :: BINARI_5:5

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

proof end;

theorem :: BINARI_5:6

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

theorem :: BINARI_5:7

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

theorem :: BINARI_5:8

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

proof end;

theorem :: BINARI_5:9

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

proof end;

theorem :: BINARI_5:10

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

proof end;

theorem :: BINARI_5:11

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

theorem :: BINARI_5:12

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

proof end;

theorem :: BINARI_5:13

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

theorem :: BINARI_5:14

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

proof end;

theorem :: BINARI_5:15

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

proof end;

theorem :: BINARI_5:16

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

theorem :: BINARI_5:17

for x being boolean set holds TRUE 'xnor' x = x

proof end;

theorem :: BINARI_5:18

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

theorem :: BINARI_5:19

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

proof end;

theorem :: BINARI_5:20

for x, y being boolean set holds 'not' (x 'xnor' y) = x 'xor' y by MARGREL1:40;

theorem :: BINARI_5:21

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

proof end;

theorem :: BINARI_5:22

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

proof end;

theorem Th23: :: BINARI_5:23

for x, y being boolean set holds x 'eqv' y = (x 'imp' y) '&' (y 'imp' x)

proof end;

theorem Th24: :: BINARI_5:24

for x, y being boolean set holds
( x 'eqv' y = TRUE iff ( x 'imp' y = TRUE & y 'imp' x = TRUE ) )

proof end;

theorem Th25: :: BINARI_5:25

for x, y being boolean set st x 'imp' y = TRUE & y 'imp' x = TRUE holds
x = y

proof end;

theorem Th26: :: BINARI_5:26

for x, y, z being boolean set st x 'imp' y = TRUE & y 'imp' z = TRUE holds
x 'imp' z = TRUE

proof end;

theorem :: BINARI_5:27

for x, y, z being boolean set st x 'eqv' y = TRUE & y 'eqv' z = TRUE holds
x 'eqv' z = TRUE

proof end;

theorem Th28: :: BINARI_5:28

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

proof end;

theorem :: BINARI_5:29

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

proof end;

theorem :: BINARI_5:30

for x, y, z, w being boolean set st x 'eqv' y = TRUE & z 'eqv' w = TRUE holds
(x '&' z) 'eqv' (y '&' w) = TRUE

proof end;

theorem :: BINARI_5:31

for x, y, z, w being boolean set st x 'eqv' y = TRUE & z 'eqv' w = TRUE holds
(x 'imp' z) 'eqv' (y 'imp' w) = TRUE

proof end;

theorem :: BINARI_5:32

for x, y, z, w being boolean set st x 'eqv' y = TRUE & z 'eqv' w = TRUE holds
(x 'or' z) 'eqv' (y 'or' w) = TRUE

proof end;

theorem :: BINARI_5:33

for x, y, z, w being boolean set st x 'eqv' y = TRUE & z 'eqv' w = TRUE holds
(x 'eqv' z) 'eqv' (y 'eqv' w) = TRUE

proof end;

theorem :: BINARI_5:34

for x, y being boolean set st x = TRUE & x 'imp' y = TRUE holds
y = TRUE

proof end;

theorem :: BINARI_5:35

for y, x being boolean set st y = TRUE holds
x 'imp' y = TRUE

proof end;

theorem :: BINARI_5:36

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

proof end;

theorem :: BINARI_5:37

for x being boolean set holds x 'imp' x = TRUE

proof end;

theorem :: BINARI_5:38

for x, y being boolean set st x 'imp' y = TRUE & x 'imp' ('not' y) = TRUE holds
'not' x = TRUE

proof end;

theorem :: BINARI_5:39

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

proof end;

theorem :: BINARI_5:40

for x, y, z being boolean set holds (x 'imp' y) 'imp' (('not' (y '&' z)) 'imp' ('not' (x '&' z))) = TRUE

proof end;

theorem :: BINARI_5:41

for x, y, z being boolean set holds (x 'imp' y) 'imp' ((y 'imp' z) 'imp' (x 'imp' z)) = TRUE

proof end;

theorem :: BINARI_5:42

for x, y, z being boolean set st x 'imp' y = TRUE holds
(y 'imp' z) 'imp' (x 'imp' z) = TRUE

proof end;

theorem :: BINARI_5:43

for y, x being boolean set holds y 'imp' (x 'imp' y) = TRUE

proof end;

theorem :: BINARI_5:44

for x, y, z being boolean set holds ((x 'imp' y) 'imp' z) 'imp' (y 'imp' z) = TRUE

proof end;

theorem :: BINARI_5:45

for y, x being boolean set holds y 'imp' ((y 'imp' x) 'imp' x) = TRUE

proof end;

theorem :: BINARI_5:46

for z, y, x being boolean set holds (z 'imp' (y 'imp' x)) 'imp' (y 'imp' (z 'imp' x)) = TRUE

proof end;

theorem :: BINARI_5:47

for y, z, x being boolean set holds (y 'imp' z) 'imp' ((x 'imp' y) 'imp' (x 'imp' z)) = TRUE

proof end;

theorem :: BINARI_5:48

for y, z being boolean set holds (y 'imp' (y 'imp' z)) 'imp' (y 'imp' z) = TRUE

proof end;

theorem :: BINARI_5:49

for x, y, z being boolean set holds (x 'imp' (y 'imp' z)) 'imp' ((x 'imp' y) 'imp' (x 'imp' z)) = TRUE

proof end;

theorem :: BINARI_5:50

for x, y being boolean set st x = TRUE holds
(x 'imp' y) 'imp' y = TRUE

proof end;

theorem :: BINARI_5:51

for z, y, x being boolean set st z 'imp' (y 'imp' x) = TRUE holds
y 'imp' (z 'imp' x) = TRUE

proof end;

theorem :: BINARI_5:52

for z, y, x being boolean set st z 'imp' (y 'imp' x) = TRUE & y = TRUE holds
z 'imp' x = TRUE

proof end;

theorem :: BINARI_5:53

for z, y, x being boolean set st z 'imp' (y 'imp' x) = TRUE & y = TRUE & z = TRUE holds
x = TRUE

proof end;

theorem :: BINARI_5:54

for y, z being boolean set st y 'imp' (y 'imp' z) = TRUE holds
y 'imp' z = TRUE

proof end;

theorem :: BINARI_5:55

for x, y, z being boolean set st x 'imp' (y 'imp' z) = TRUE holds
(x 'imp' y) 'imp' (x 'imp' z) = TRUE

proof end;