:: BVFUNC26 semantic presentation

definition

let c₁, c₂ be boolean-valued Function;
func c₁ 'nand' c₂ -> Function means :Def1: :: BVFUNC26:def 1
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) 'nand' (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;
func c₁ 'nor' c₂ -> Function means :Def2: :: BVFUNC26:def 2
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) 'nor' (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

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

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

registration

let c₁, c₂ be boolean-valued Function;
cluster a₁ 'nand' a₂ -> boolean-valued ;
coherence

proof end;

cluster a₁ 'nor' a₂ -> boolean-valued ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of Funcs c₁,BOOLEAN ;
redefine func 'nand' as c₂ 'nand' c₃ -> Element of Funcs a₁,BOOLEAN means :Def3: :: BVFUNC26:def 3
for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) 'nand' (a₃ . b₁);
coherence

proof end;

compatibility

proof end;

redefine func 'nor' as c₂ 'nor' c₃ -> Element of Funcs a₁,BOOLEAN means :Def4: :: BVFUNC26:def 4
for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) 'nor' (a₃ . b₁);
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def3 defines 'nand' BVFUNC26:def 3 :

:: deftheorem Def4 defines 'nor' BVFUNC26:def 4 :

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of BVF c₁;
redefine func 'nand' as c₂ 'nand' c₃ -> Element of BVF a₁;
coherence

proof end;

redefine func 'nor' as c₂ 'nor' c₃ -> Element of BVF a₁;
coherence

proof end;

end;

theorem Th1: :: BVFUNC26:1

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' b₃ = 'not' (b₂ '&' b₃)

proof end;

theorem Th2: :: BVFUNC26:2

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' b₃ = 'not' (b₂ 'or' b₃)

proof end;

theorem Th3: :: BVFUNC26:3

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds (I_el b₁) 'nand' b₂ = 'not' b₂

proof end;

theorem Th4: :: BVFUNC26:4

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds (O_el b₁) 'nand' b₂ = I_el b₁

proof end;

theorem Th5: :: BVFUNC26:5

for b₁ being non empty set holds
( (O_el b₁) 'nand' (O_el b₁) = I_el b₁ & (O_el b₁) 'nand' (I_el b₁) = I_el b₁ & (I_el b₁) 'nand' (I_el b₁) = O_el b₁ )

proof end;

theorem Th6: :: BVFUNC26:6

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'nand' b₂ = 'not' b₂ & 'not' (b₂ 'nand' b₂) = b₂ )

proof end;

theorem Th7: :: BVFUNC26:7

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds 'not' (b₂ 'nand' b₃) = b₂ '&' b₃

proof end;

theorem Th8: :: BVFUNC26:8

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'nand' ('not' b₂) = I_el b₁ & 'not' (b₂ 'nand' ('not' b₂)) = O_el b₁ )

proof end;

theorem Th9: :: BVFUNC26:9

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₃ '&' b₄) = 'not' ((b₂ '&' b₃) '&' b₄)

proof end;

theorem Th10: :: BVFUNC26:10

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₃ '&' b₄) = (b₂ '&' b₃) 'nand' b₄

proof end;

theorem Th11: :: BVFUNC26:11

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₃ 'or' b₄) = ('not' (b₂ '&' b₃)) '&' ('not' (b₂ '&' b₄))

proof end;

theorem Th12: :: BVFUNC26:12

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₃ 'xor' b₄) = (b₂ '&' b₃) 'eqv' (b₂ '&' b₄)

proof end;

theorem Th13: :: BVFUNC26:13

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'nand' (b₃ 'nand' b₄) = ('not' b₂) 'or' (b₃ '&' b₄) & b₂ 'nand' (b₃ 'nand' b₄) = b₂ 'imp' (b₃ '&' b₄) )

proof end;

theorem Th14: :: BVFUNC26:14

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'nand' (b₃ 'nor' b₄) = (('not' b₂) 'or' b₃) 'or' b₄ & b₂ 'nand' (b₃ 'nor' b₄) = b₂ 'imp' (b₃ 'or' b₄) )

proof end;

theorem Th15: :: BVFUNC26:15

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₃ 'eqv' b₄) = b₂ 'imp' (b₃ 'xor' b₄)

proof end;

theorem Th16: :: BVFUNC26:16

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₂ '&' b₃) = b₂ 'nand' b₃

proof end;

theorem Th17: :: BVFUNC26:17

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₂ 'or' b₃) = ('not' b₂) '&' ('not' (b₂ '&' b₃))

proof end;

theorem Th18: :: BVFUNC26:18

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₂ 'eqv' b₃) = b₂ 'imp' (b₂ 'xor' b₃)

proof end;

theorem Th19: :: BVFUNC26:19

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'nand' (b₂ 'nand' b₃) = ('not' b₂) 'or' b₃ & b₂ 'nand' (b₂ 'nand' b₃) = b₂ 'imp' b₃ )

proof end;

theorem Th20: :: BVFUNC26:20

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₂ 'nor' b₃) = I_el b₁

proof end;

theorem Th21: :: BVFUNC26:21

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₂ 'eqv' b₃) = ('not' b₂) 'or' ('not' b₃)

proof end;

theorem Th22: :: BVFUNC26:22

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ '&' b₃ = (b₂ 'nand' b₃) 'nand' (b₂ 'nand' b₃)

proof end;

theorem Th23: :: BVFUNC26:23

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds (b₂ 'nand' b₃) 'nand' (b₂ 'nand' b₄) = b₂ '&' (b₃ 'or' b₄)

proof end;

theorem Th24: :: BVFUNC26:24

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₃ 'imp' b₄) = (('not' b₂) 'or' b₃) '&' ('not' (b₂ '&' b₄))

proof end;

theorem Th25: :: BVFUNC26:25

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₂ 'imp' b₃) = 'not' (b₂ '&' b₃)

proof end;

theorem Th26: :: BVFUNC26:26

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds (I_el b₁) 'nor' b₂ = O_el b₁

proof end;

theorem Th27: :: BVFUNC26:27

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds (O_el b₁) 'nor' b₂ = 'not' b₂

proof end;

theorem Th28: :: BVFUNC26:28

for b₁ being non empty set holds
( (O_el b₁) 'nor' (O_el b₁) = I_el b₁ & (O_el b₁) 'nor' (I_el b₁) = O_el b₁ & (I_el b₁) 'nor' (I_el b₁) = O_el b₁ )

proof end;

theorem Th29: :: BVFUNC26:29

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'nor' b₂ = 'not' b₂ & 'not' (b₂ 'nor' b₂) = b₂ )

proof end;

theorem Th30: :: BVFUNC26:30

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds 'not' (b₂ 'nor' b₃) = b₂ 'or' b₃

proof end;

theorem Th31: :: BVFUNC26:31

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'nor' ('not' b₂) = O_el b₁ & 'not' (b₂ 'nor' ('not' b₂)) = I_el b₁ )

proof end;

theorem Th32: :: BVFUNC26:32

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds ('not' b₂) '&' (b₂ 'xor' b₃) = ('not' b₂) '&' b₃

proof end;

theorem Th33: :: BVFUNC26:33

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₃ '&' b₄) = ('not' (b₂ 'or' b₃)) 'or' ('not' (b₂ 'or' b₄))

proof end;

theorem Th34: :: BVFUNC26:34

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₃ 'or' b₄) = 'not' ((b₂ 'or' b₃) 'or' b₄)

proof end;

theorem Th35: :: BVFUNC26:35

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₃ 'eqv' b₄) = ('not' b₂) '&' (b₃ 'xor' b₄)

proof end;

theorem Th36: :: BVFUNC26:36

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₃ 'imp' b₄) = (('not' b₂) '&' b₃) '&' ('not' b₄)

proof end;

theorem Th37: :: BVFUNC26:37

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₃ 'nand' b₄) = (('not' b₂) '&' b₃) '&' b₄

proof end;

theorem Th38: :: BVFUNC26:38

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₃ 'nor' b₄) = ('not' b₂) '&' (b₃ 'or' b₄)

proof end;

theorem Th39: :: BVFUNC26:39

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₂ '&' b₃) = 'not' (b₂ '&' (b₂ 'or' b₃))

proof end;

theorem Th40: :: BVFUNC26:40

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₂ 'or' b₃) = 'not' (b₂ 'or' b₃)

proof end;

theorem Th41: :: BVFUNC26:41

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₂ 'eqv' b₃) = ('not' b₂) '&' b₃

proof end;

theorem Th42: :: BVFUNC26:42

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₂ 'imp' b₃) = O_el b₁

proof end;

theorem Th43: :: BVFUNC26:43

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₂ 'nand' b₃) = O_el b₁

proof end;

theorem Th44: :: BVFUNC26:44

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₂ 'nor' b₃) = ('not' b₂) '&' b₃

proof end;

theorem Th45: :: BVFUNC26:45

for b₁ being non empty set holds (O_el b₁) 'eqv' (O_el b₁) = I_el b₁

proof end;

theorem Th46: :: BVFUNC26:46

for b₁ being non empty set holds (O_el b₁) 'eqv' (I_el b₁) = O_el b₁

proof end;

theorem Th47: :: BVFUNC26:47

for b₁ being non empty set holds (I_el b₁) 'eqv' (I_el b₁) = I_el b₁

proof end;

theorem Th48: :: BVFUNC26:48

for b₁ being non empty set
for b₂ being Element of Funcs b₁,BOOLEAN holds
( b₂ 'eqv' b₂ = I_el b₁ & 'not' (b₂ 'eqv' b₂) = O_el b₁ )

proof end;

theorem Th49: :: BVFUNC26:49

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'eqv' (b₂ 'or' b₃) = b₂ 'or' ('not' b₃)

proof end;

theorem Th50: :: BVFUNC26:50

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ '&' (b₃ 'nand' b₄) = (b₂ '&' ('not' b₃)) 'or' (b₂ '&' ('not' b₄))

proof end;

theorem Th51: :: BVFUNC26:51

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'or' (b₃ 'nand' b₄) = (b₂ 'or' ('not' b₃)) 'or' ('not' b₄)

proof end;

theorem Th52: :: BVFUNC26:52

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'xor' (b₃ 'nand' b₄) = (('not' b₂) '&' ('not' (b₃ '&' b₄))) 'or' ((b₂ '&' b₃) '&' b₄)

proof end;

theorem Th53: :: BVFUNC26:53

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'eqv' (b₃ 'nand' b₄) = (b₂ '&' ('not' (b₃ '&' b₄))) 'or' ((('not' b₂) '&' b₃) '&' b₄)

proof end;

theorem Th54: :: BVFUNC26:54

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'imp' (b₃ 'nand' b₄) = 'not' ((b₂ '&' b₃) '&' b₄)

proof end;

theorem Th55: :: BVFUNC26:55

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₃ 'nand' b₄) = 'not' ((b₂ 'or' ('not' b₃)) 'or' ('not' b₄))

proof end;

theorem Th56: :: BVFUNC26:56

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ '&' (b₂ 'nand' b₃) = b₂ '&' ('not' b₃)

proof end;

theorem Th57: :: BVFUNC26:57

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'or' (b₂ 'nand' b₃) = I_el b₁

proof end;

theorem Th58: :: BVFUNC26:58

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'xor' (b₂ 'nand' b₃) = ('not' b₂) 'or' b₃

proof end;

theorem Th59: :: BVFUNC26:59

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'eqv' (b₂ 'nand' b₃) = b₂ '&' ('not' b₃)

proof end;

theorem Th60: :: BVFUNC26:60

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'imp' (b₂ 'nand' b₃) = 'not' (b₂ '&' b₃)

proof end;

theorem Th61: :: BVFUNC26:61

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nor' (b₂ 'nand' b₃) = O_el b₁

proof end;

theorem Th62: :: BVFUNC26:62

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ '&' (b₃ 'nor' b₄) = (b₂ '&' ('not' b₃)) '&' ('not' b₄)

proof end;

theorem Th63: :: BVFUNC26:63

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'or' (b₃ 'nor' b₄) = (b₂ 'or' ('not' b₃)) '&' (b₂ 'or' ('not' b₄))

proof end;

theorem Th64: :: BVFUNC26:64

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'xor' (b₃ 'nor' b₄) = (b₂ 'or' ('not' (b₃ 'or' b₄))) '&' ((('not' b₂) 'or' b₃) 'or' b₄)

proof end;

theorem Th65: :: BVFUNC26:65

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'eqv' (b₃ 'nor' b₄) = ((b₂ 'or' b₃) 'or' b₄) '&' (('not' b₂) 'or' ('not' (b₃ 'or' b₄)))

proof end;

theorem Th66: :: BVFUNC26:66

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'imp' (b₃ 'nor' b₄) = 'not' (b₂ '&' (b₃ 'or' b₄))

proof end;

theorem Th67: :: BVFUNC26:67

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₃ 'nor' b₄) = (('not' b₂) 'or' b₃) 'or' b₄

proof end;

theorem Th68: :: BVFUNC26:68

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ '&' (b₂ 'nor' b₃) = O_el b₁

proof end;

theorem Th69: :: BVFUNC26:69

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'or' (b₂ 'nor' b₃) = b₂ 'or' ('not' b₃)

proof end;

theorem Th70: :: BVFUNC26:70

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'xor' (b₂ 'nor' b₃) = b₂ 'or' ('not' b₃)

proof end;

theorem Th71: :: BVFUNC26:71

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'eqv' (b₂ 'nor' b₃) = ('not' b₂) '&' b₃

proof end;

theorem Th72: :: BVFUNC26:72

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'imp' (b₂ 'nor' b₃) = 'not' (b₂ 'or' (b₂ '&' b₃))

proof end;

theorem Th73: :: BVFUNC26:73

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,BOOLEAN holds b₂ 'nand' (b₂ 'nor' b₃) = I_el b₁

proof end;