:: BINARI_6 semantic presentation

theorem Th1: :: BINARI_6:1

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

proof end;

theorem Th3: :: BINARI_6:2

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

proof end;

theorem Th8: :: BINARI_6:3

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

proof end;

theorem :: BINARI_6:4

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

proof end;

theorem Th9: :: BINARI_6:5

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

proof end;

theorem Th10: :: BINARI_6:6

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

proof end;

theorem :: BINARI_6:7

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

proof end;

theorem :: BINARI_6:8

for x being boolean set holds FALSE 'eqv' x = 'not' x

proof end;

theorem :: BINARI_6:9

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

proof end;

theorem :: BINARI_6:10

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

proof end;

theorem :: BINARI_6:11

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

proof end;

theorem Th11: :: BINARI_6:12

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

proof end;

theorem Th12: :: BINARI_6:13

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

proof end;

theorem :: BINARI_6:14

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

proof end;

theorem :: BINARI_6:15

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

proof end;

theorem :: BINARI_6:16

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

proof end;

theorem :: BINARI_6:17

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

proof end;

theorem Th55: :: BINARI_6:18

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

proof end;

theorem :: BINARI_6:19

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

proof end;

theorem :: BINARI_6:20

for x, y being boolean set holds x '&' (x 'nor' y) = FALSE

proof end;

theorem :: BINARI_6:21

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

proof end;

theorem Th17: :: BINARI_6:22

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

proof end;

theorem Th15: :: BINARI_6:23

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

proof end;

theorem Th16: :: BINARI_6:24

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

proof end;

theorem :: BINARI_6:25

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

proof end;

theorem :: BINARI_6:26

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

proof end;

theorem :: BINARI_6:27

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

proof end;

theorem :: BINARI_6:28

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

proof end;

theorem :: BINARI_6:29

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

proof end;

theorem Th20: :: BINARI_6:30

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

proof end;

theorem Th22: :: BINARI_6:31

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

proof end;

theorem Th23: :: BINARI_6:32

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

proof end;

theorem Th24: :: BINARI_6:33

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

proof end;

theorem Th31: :: BINARI_6:34

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

proof end;

theorem :: BINARI_6:35

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

proof end;

theorem :: BINARI_6:36

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

proof end;

theorem Th25: :: BINARI_6:37

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

proof end;

theorem :: BINARI_6:38

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

proof end;

theorem :: BINARI_6:39

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

proof end;

theorem :: BINARI_6:40

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

proof end;

theorem Th27: :: BINARI_6:41

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

proof end;

theorem Th28: :: BINARI_6:42

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

proof end;

theorem Th29: :: BINARI_6:43

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

proof end;

theorem Th30: :: BINARI_6:44

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

proof end;

theorem :: BINARI_6:45

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

proof end;

theorem :: BINARI_6:46

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

proof end;

theorem :: BINARI_6:47

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

proof end;

theorem :: BINARI_6:48

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

proof end;

theorem :: BINARI_6:49

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

proof end;

theorem :: BINARI_6:50

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

proof end;

theorem Th32: :: BINARI_6:51

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

proof end;

theorem Th34: :: BINARI_6:52

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

proof end;

theorem Th35: :: BINARI_6:53

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

proof end;

theorem Th36: :: BINARI_6:54

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

proof end;

theorem :: BINARI_6:55

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

proof end;

theorem :: BINARI_6:56

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

proof end;

theorem :: BINARI_6:57

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

proof end;

theorem :: BINARI_6:58

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

proof end;

theorem :: BINARI_6:59

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

proof end;

theorem :: BINARI_6:60

for x, y being boolean set holds x 'nor' (x 'nand' y) = FALSE

proof end;

theorem :: BINARI_6:61

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

proof end;

theorem Th37: :: BINARI_6:62

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

proof end;

theorem :: BINARI_6:63

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

proof end;

theorem :: BINARI_6:64

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

proof end;

theorem Th38: :: BINARI_6:65

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

proof end;

theorem Th39: :: BINARI_6:66

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

proof end;

theorem :: BINARI_6:67

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

proof end;

theorem Th41: :: BINARI_6:68

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

proof end;

theorem :: BINARI_6:69

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

proof end;

theorem Th42: :: BINARI_6:70

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

proof end;

theorem Th43: :: BINARI_6:71

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

proof end;

theorem :: BINARI_6:72

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

proof end;

theorem :: BINARI_6:73

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

proof end;

theorem :: BINARI_6:74

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

proof end;

theorem :: BINARI_6:75

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

proof end;

theorem Th51: :: BINARI_6:76

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

proof end;

theorem :: BINARI_6:77

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

proof end;

theorem :: BINARI_6:78

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

proof end;

theorem :: BINARI_6:79

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

proof end;

theorem :: BINARI_6:80

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

proof end;

theorem :: BINARI_6:81

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

proof end;

theorem :: BINARI_6:82

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

proof end;

theorem :: BINARI_6:83

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

proof end;

theorem :: BINARI_6:84

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

proof end;

theorem Th57: :: BINARI_6:85

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

proof end;

theorem Th56: :: BINARI_6:86

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

proof end;

theorem :: BINARI_6:87

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

proof end;