XBOOLEAN: On the Arithmetic of Boolean Values

:: On the Arithmetic of Boolean Values
:: by Library Committee
::
:: Received November 30, 2006
:: Copyright (c) 2006 Association of Mizar Users

begin

definition

func FALSE -> set equals :: XBOOLEAN:def 1
0 ;
coherence ;
func TRUE -> set equals :: XBOOLEAN:def 2
1;
coherence ;

end;

:: deftheorem defines FALSE XBOOLEAN:def 1 :

:: deftheorem defines TRUE XBOOLEAN:def 2 :

definition

let p be set ;
attr p is boolean means :Def3: :: XBOOLEAN:def 3
( p = FALSE or p = TRUE );

end;

:: deftheorem Def3 defines boolean XBOOLEAN:def 3 :

registration

cluster FALSE -> boolean ;
coherence by Def3;
cluster TRUE -> boolean ;
coherence by Def3;
cluster boolean set ;
existence by Def3;
cluster boolean -> natural set ;
coherence

proof end;

end;

definition

let p be boolean number ;
func 'not' p -> boolean number equals :: XBOOLEAN:def 4
1 - p;
coherence

proof end;

involutiveness ;
let q be boolean number ;
func p '&' q -> set equals :: XBOOLEAN:def 5
p * q;
correctness ;
commutativity ;
idempotence

proof end;

end;

:: deftheorem defines 'not' XBOOLEAN:def 4 :

:: deftheorem defines '&' XBOOLEAN:def 5 :

registration

let p, q be boolean number ;
cluster p '&' q -> boolean ;
coherence

proof end;

end;

definition

let p, q be boolean number ;
func p 'or' q -> set equals :: XBOOLEAN:def 6
'not' (('not' p) '&' ('not' q));
coherence ;
commutativity ;
idempotence ;

end;

:: deftheorem defines 'or' XBOOLEAN:def 6 :

definition

let p, q be boolean number ;
func p => q -> set equals :: XBOOLEAN:def 7
('not' p) 'or' q;
coherence ;

end;

:: deftheorem defines => XBOOLEAN:def 7 :

registration

let p, q be boolean number ;
cluster p 'or' q -> boolean ;
coherence ;
cluster p => q -> boolean ;
coherence ;

end;

definition

let p, q be boolean number ;
func p <=> q -> set equals :: XBOOLEAN:def 8
(p => q) '&' (q => p);
coherence ;
commutativity ;

end;

:: deftheorem defines <=> XBOOLEAN:def 8 :

registration

let p, q be boolean number ;
cluster p <=> q -> boolean ;
coherence ;

end;

definition

let p, q be boolean number ;
func p 'nand' q -> set equals :: XBOOLEAN:def 9
'not' (p '&' q);
coherence ;
commutativity ;
func p 'nor' q -> set equals :: XBOOLEAN:def 10
'not' (p 'or' q);
coherence ;
commutativity ;
func p 'xor' q -> set equals :: XBOOLEAN:def 11
'not' (p <=> q);
coherence ;
commutativity ;
func p '\' q -> set equals :: XBOOLEAN:def 12
p '&' ('not' q);
coherence ;

end;

:: deftheorem defines 'nand' XBOOLEAN:def 9 :

:: deftheorem defines 'nor' XBOOLEAN:def 10 :

:: deftheorem defines 'xor' XBOOLEAN:def 11 :

:: deftheorem defines '\' XBOOLEAN:def 12 :

registration

let p, q be boolean number ;
cluster p 'nand' q -> boolean ;
coherence ;
cluster p 'nor' q -> boolean ;
coherence ;
cluster p 'xor' q -> boolean ;
coherence ;
cluster p '\' q -> boolean ;
coherence ;

end;

begin

theorem :: XBOOLEAN:1

for p being boolean number holds p '&' p = p ;

theorem :: XBOOLEAN:2

for p, q being boolean number holds p '&' (p '&' q) = p '&' q

proof end;

theorem :: XBOOLEAN:3

for p being boolean number holds p 'or' p = p ;

theorem :: XBOOLEAN:4

for p, q being boolean number holds p 'or' (p 'or' q) = p 'or' q

proof end;

theorem :: XBOOLEAN:5

for p, q being boolean number holds p 'or' (p '&' q) = p

proof end;

theorem :: XBOOLEAN:6

for p, q being boolean number holds p '&' (p 'or' q) = p

proof end;

theorem :: XBOOLEAN:7

for p, q being boolean number holds p '&' (p 'or' q) = p 'or' (p '&' q)

proof end;

theorem :: XBOOLEAN:8

for p, q, r being boolean number holds p '&' (q 'or' r) = (p '&' q) 'or' (p '&' r)

proof end;

theorem :: XBOOLEAN:9

for p, q, r being boolean number holds p 'or' (q '&' r) = (p 'or' q) '&' (p 'or' r)

proof end;

theorem :: XBOOLEAN:10

for p, q, r being boolean number holds ((p '&' q) 'or' (q '&' r)) 'or' (r '&' p) = ((p 'or' q) '&' (q 'or' r)) '&' (r 'or' p)

proof end;

theorem :: XBOOLEAN:11

for p, q being boolean number holds p '&' (('not' p) 'or' q) = p '&' q

proof end;

theorem :: XBOOLEAN:12

for p, q being boolean number holds p 'or' (('not' p) '&' q) = p 'or' q

proof end;

theorem :: XBOOLEAN:13

for p, q being boolean number holds p => (p => q) = p => q

proof end;

theorem :: XBOOLEAN:14

for p, q being boolean number holds p '&' (p => q) = p '&' q

proof end;

theorem :: XBOOLEAN:15

for p, q being boolean number holds p => (p '&' q) = p => q

proof end;

theorem :: XBOOLEAN:16

for p, q being boolean number holds p '&' ('not' (p => q)) = p '&' ('not' q)

proof end;

theorem :: XBOOLEAN:17

for p, q being boolean number holds ('not' p) 'or' (p => q) = p => q

proof end;

theorem :: XBOOLEAN:18

for p, q being boolean number holds ('not' p) '&' (p => q) = ('not' p) 'or' (('not' p) '&' q)

proof end;

theorem :: XBOOLEAN:19

for p, q, r being boolean number holds (p <=> q) <=> r = p <=> (q <=> r)

proof end;

theorem :: XBOOLEAN:20

for p, q being boolean number holds p '&' (p <=> q) = p '&' q

proof end;

theorem :: XBOOLEAN:21

for p, q being boolean number holds ('not' p) '&' (p <=> q) = ('not' p) '&' ('not' q)

proof end;

theorem :: XBOOLEAN:22

for p, q, r being boolean number holds p '&' (q <=> r) = (p '&' (('not' q) 'or' r)) '&' (('not' r) 'or' q) ;

theorem :: XBOOLEAN:23

for p, q, r being boolean number holds p 'or' (q <=> r) = ((p 'or' ('not' q)) 'or' r) '&' ((p 'or' ('not' r)) 'or' q)

proof end;

theorem :: XBOOLEAN:24

for p, q being boolean number holds ('not' p) '&' (p <=> q) = (('not' p) '&' ('not' q)) '&' (('not' p) 'or' q)

proof end;

theorem :: XBOOLEAN:25

for p, q, r being boolean number holds ('not' p) '&' (q <=> r) = (('not' p) '&' (('not' q) 'or' r)) '&' (('not' r) 'or' q) ;

theorem :: XBOOLEAN:26

for p, q being boolean number holds p => (p <=> q) = p => q

proof end;

theorem :: XBOOLEAN:27

for p, q being boolean number holds p => (p <=> q) = p => (p => q)

proof end;

theorem :: XBOOLEAN:28

for p, q being boolean number holds p 'or' (p <=> q) = q => p

proof end;

theorem :: XBOOLEAN:29

for p, q being boolean number holds ('not' p) 'or' (p <=> q) = p => q

proof end;

theorem :: XBOOLEAN:30

for p, q, r being boolean number holds p => (q <=> r) = ((('not' p) 'or' ('not' q)) 'or' r) '&' ((('not' p) 'or' q) 'or' ('not' r))

proof end;

theorem :: XBOOLEAN:31

for p being boolean number holds p 'nor' p = 'not' p ;

theorem :: XBOOLEAN:32

for p, q being boolean number holds p 'nor' (p '&' q) = 'not' p

proof end;

theorem :: XBOOLEAN:33

for p, q being boolean number holds p 'nor' (p 'or' q) = ('not' p) '&' ('not' q)

proof end;

theorem :: XBOOLEAN:34

for p, q being boolean number holds p 'nor' (p 'nor' q) = ('not' p) '&' q

proof end;

theorem :: XBOOLEAN:35

for p, q being boolean number holds p 'nor' (p '&' q) = 'not' p

proof end;

theorem :: XBOOLEAN:36

for p, q being boolean number holds p 'nor' (p 'or' q) = p 'nor' q

proof end;

theorem :: XBOOLEAN:37

for p, q being boolean number holds ('not' p) '&' (p 'nor' q) = p 'nor' q

proof end;

theorem :: XBOOLEAN:38

for p, q, r being boolean number holds p 'or' (q 'nor' r) = (p 'or' ('not' q)) '&' (p 'or' ('not' r))

proof end;

theorem :: XBOOLEAN:39

for p, q, r being boolean number holds p 'nor' (q 'nor' r) = (('not' p) '&' q) 'or' (('not' p) '&' r)

proof end;

theorem :: XBOOLEAN:40

for p, q, r being boolean number holds p 'nor' (q '&' r) = ('not' (p 'or' q)) 'or' ('not' (p 'or' r))

proof end;

theorem :: XBOOLEAN:41

for p, q, r being boolean number holds p '&' (q 'nor' r) = (p '&' ('not' q)) '&' ('not' r)

proof end;

theorem :: XBOOLEAN:42

for p, q being boolean number holds p => (p 'nor' q) = 'not' p

proof end;

theorem :: XBOOLEAN:43

for p, q, r being boolean number holds p => (q 'nor' r) = (p => ('not' q)) '&' (p => ('not' r))

proof end;

theorem :: XBOOLEAN:44

for p, q being boolean number holds p 'or' (p 'nor' q) = q => p

proof end;

theorem :: XBOOLEAN:45

for p, q, r being boolean number holds p 'or' (q 'nor' r) = (q => p) '&' (r => p)

proof end;

theorem :: XBOOLEAN:46

for p, q, r being boolean number holds p => (q 'nor' r) = (('not' p) 'or' ('not' q)) '&' (('not' p) 'or' ('not' r))

proof end;

theorem :: XBOOLEAN:47

for p, q being boolean number holds p 'nor' (p <=> q) = ('not' p) '&' q

proof end;

theorem :: XBOOLEAN:48

for p, q being boolean number holds ('not' p) '&' (p <=> q) = p 'nor' q

proof end;

theorem :: XBOOLEAN:49

for p, q, r being boolean number holds p 'nor' (q <=> r) = 'not' (((p 'or' ('not' q)) 'or' r) '&' ((p 'or' ('not' r)) 'or' q))

proof end;

theorem :: XBOOLEAN:50

for p, q being boolean number holds p <=> q = (p '&' q) 'or' (p 'nor' q)

proof end;

theorem :: XBOOLEAN:51

for p being boolean number holds p 'nand' p = 'not' p ;

theorem :: XBOOLEAN:52

for p, q being boolean number holds p '&' (p 'nand' q) = p '&' ('not' q)

proof end;

theorem :: XBOOLEAN:53

for p, q being boolean number holds p 'nand' (p '&' q) = 'not' (p '&' q)

proof end;

theorem :: XBOOLEAN:54

for p, q, r being boolean number holds p 'nand' (q 'nand' r) = (('not' p) 'or' q) '&' (('not' p) 'or' r)

proof end;

theorem :: XBOOLEAN:55

for p, q, r being boolean number holds p 'nand' (q 'or' r) = ('not' (p '&' q)) '&' ('not' (p '&' r))

proof end;

theorem :: XBOOLEAN:56

for p, q being boolean number holds p => (p 'nand' q) = p 'nand' q

proof end;

theorem :: XBOOLEAN:57

for p, q being boolean number holds p 'nand' (p 'nand' q) = p => q

proof end;

theorem :: XBOOLEAN:58

for p, q, r being boolean number holds p 'nand' (q 'nand' r) = (p => q) '&' (p => r)

proof end;

theorem :: XBOOLEAN:59

for p, q being boolean number holds p 'nand' (p => q) = 'not' (p '&' q)

proof end;

theorem :: XBOOLEAN:60

for p, q, r being boolean number holds p 'nand' (q => r) = (p => q) '&' (p => ('not' r))

proof end;

theorem :: XBOOLEAN:61

for p, q being boolean number holds ('not' p) 'or' (p 'nand' q) = p 'nand' q

proof end;

theorem :: XBOOLEAN:62

for p, q, r being boolean number holds p 'nand' (q => r) = (('not' p) 'or' q) '&' (('not' p) 'or' ('not' r))

proof end;

theorem :: XBOOLEAN:63

for p, q being boolean number holds ('not' p) '&' (p 'nand' q) = ('not' p) 'or' (('not' p) '&' ('not' q))

proof end;

theorem :: XBOOLEAN:64

for p, q, r being boolean number holds p '&' (q 'nand' r) = (p '&' ('not' q)) 'or' (p '&' ('not' r))

proof end;

theorem :: XBOOLEAN:65

for p, q being boolean number holds p 'nand' (p <=> q) = 'not' (p '&' q)

proof end;

theorem :: XBOOLEAN:66

for p, q, r being boolean number holds p 'nand' (q <=> r) = 'not' ((p '&' (('not' q) 'or' r)) '&' (('not' r) 'or' q)) ;

theorem :: XBOOLEAN:67

for p, q, r being boolean number holds p 'nand' (q 'nor' r) = (('not' p) 'or' q) 'or' r

proof end;

theorem :: XBOOLEAN:68

for p, q being boolean number holds (p '\' q) '\' q = p '\' q

proof end;

theorem :: XBOOLEAN:69

for p, q being boolean number holds p '&' (p '\' q) = p '\' q

proof end;

theorem :: XBOOLEAN:70

for p, q being boolean number holds p 'nor' (p <=> q) = q '\' p

proof end;

theorem :: XBOOLEAN:71

for p, q being boolean number holds p 'nor' (p 'nor' q) = q '\' p

proof end;

theorem :: XBOOLEAN:72

for p, q being boolean number holds p 'xor' (p 'xor' q) = q

proof end;

theorem :: XBOOLEAN:73

for p, q, r being boolean number holds (p 'xor' q) 'xor' r = p 'xor' (q 'xor' r)

proof end;

theorem :: XBOOLEAN:74

for p, q being boolean number holds 'not' (p 'xor' q) = ('not' p) 'xor' q

proof end;

theorem :: XBOOLEAN:75

for p, q, r being boolean number holds p '&' (q 'xor' r) = (p '&' q) 'xor' (p '&' r)

proof end;

theorem :: XBOOLEAN:76

for p, q being boolean number holds p '&' (p 'xor' q) = p '&' ('not' q)

proof end;

theorem :: XBOOLEAN:77

for p, q being boolean number holds p 'xor' (p '&' q) = p '&' ('not' q)

proof end;

theorem :: XBOOLEAN:78

for p, q being boolean number holds ('not' p) '&' (p 'xor' q) = ('not' p) '&' q

proof end;

theorem :: XBOOLEAN:79

for p, q being boolean number holds p 'or' (p 'xor' q) = p 'or' q

proof end;

theorem :: XBOOLEAN:80

for p, q being boolean number holds p 'or' (('not' p) 'xor' q) = p 'or' ('not' q)

proof end;

theorem :: XBOOLEAN:81

for p, q being boolean number holds p 'xor' (('not' p) '&' q) = p 'or' q

proof end;

theorem :: XBOOLEAN:82

for p, q being boolean number holds p 'xor' (p 'or' q) = ('not' p) '&' q

proof end;

theorem :: XBOOLEAN:83

for p, q, r being boolean number holds p 'xor' (q '&' r) = (p 'or' (q '&' r)) '&' (('not' p) 'or' ('not' (q '&' r)))

proof end;

theorem :: XBOOLEAN:84

for p, q being boolean number holds ('not' p) 'xor' (p => q) = p '&' q

proof end;

theorem :: XBOOLEAN:85

for p, q being boolean number holds p => (p 'xor' q) = ('not' p) 'or' ('not' q)

proof end;

theorem :: XBOOLEAN:86

for p, q being boolean number holds p 'xor' (p => q) = ('not' p) 'or' ('not' q)

proof end;

theorem :: XBOOLEAN:87

for p, q being boolean number holds ('not' p) 'xor' (q => p) = (p '&' (p 'or' ('not' q))) 'or' (('not' p) '&' q)

proof end;

theorem :: XBOOLEAN:88

for p, q being boolean number holds p 'xor' (p <=> q) = 'not' q

proof end;

theorem :: XBOOLEAN:89

for p, q being boolean number holds ('not' p) 'xor' (p <=> q) = q

proof end;

theorem :: XBOOLEAN:90

for p, q being boolean number holds p 'nor' (p 'xor' q) = ('not' p) '&' ('not' q)

proof end;

theorem :: XBOOLEAN:91

for p, q being boolean number holds p 'nor' (p 'xor' q) = p 'nor' q

proof end;

theorem :: XBOOLEAN:92

for p, q being boolean number holds p 'xor' (p 'nor' q) = q => p

proof end;

theorem :: XBOOLEAN:93

for p, q being boolean number holds p 'nand' (p 'xor' q) = p => q

proof end;

theorem :: XBOOLEAN:94

for p, q being boolean number holds p 'xor' (p 'nand' q) = p => q

proof end;

theorem :: XBOOLEAN:95

for p, q being boolean number holds p 'xor' (p => q) = p 'nand' q

proof end;

theorem :: XBOOLEAN:96

for p, q, r being boolean number holds p 'nand' (q 'xor' r) = (p '&' q) <=> (p '&' r)

proof end;

theorem :: XBOOLEAN:97

for p, q being boolean number holds p 'xor' (p '&' q) = p '\' q

proof end;

theorem :: XBOOLEAN:98

for p, q being boolean number holds p '&' (p 'xor' q) = p '\' q

proof end;

theorem :: XBOOLEAN:99

for p, q being boolean number holds ('not' p) '&' (p 'xor' q) = q '\' p

proof end;

theorem :: XBOOLEAN:100

for p, q being boolean number holds p 'xor' (p 'or' q) = q '\' p

proof end;

begin

theorem :: XBOOLEAN:101

for p, q being boolean number st p '&' q = TRUE holds
( p = TRUE & q = TRUE )

proof end;

theorem :: XBOOLEAN:102

for p being boolean number holds 'not' (p '&' ('not' p)) = TRUE

proof end;

theorem :: XBOOLEAN:103

for p being boolean number holds p => p = TRUE

proof end;

theorem :: XBOOLEAN:104

for p, q being boolean number holds p => (q => p) = TRUE

proof end;

theorem :: XBOOLEAN:105

for p, q being boolean number holds p => ((p => q) => q) = TRUE

proof end;

theorem :: XBOOLEAN:106

for p, q, r being boolean number holds (p => q) => ((q => r) => (p => r)) = TRUE

proof end;

theorem :: XBOOLEAN:107

for p, q, r being boolean number holds (p => q) => ((r => p) => (r => q)) = TRUE

proof end;

theorem :: XBOOLEAN:108

for p, q being boolean number holds (p => (p => q)) => (p => q) = TRUE

proof end;

theorem :: XBOOLEAN:109

for p, q, r being boolean number holds (p => (q => r)) => ((p => q) => (p => r)) = TRUE

proof end;

theorem :: XBOOLEAN:110

for p, q, r being boolean number holds (p => (q => r)) => (q => (p => r)) = TRUE

proof end;

theorem :: XBOOLEAN:111

for p, q, r being boolean number holds ((p => q) => r) => (q => r) = TRUE

proof end;

theorem :: XBOOLEAN:112

for p being boolean number holds (TRUE => p) => p = TRUE

proof end;

theorem :: XBOOLEAN:113

for p, q, r being boolean number st p => q = TRUE holds
(q => r) => (p => r) = TRUE

proof end;

theorem :: XBOOLEAN:114

for p, q being boolean number st p => (p => q) = TRUE holds
p => q = TRUE

proof end;

theorem :: XBOOLEAN:115

for p, q, r being boolean number st p => (q => r) = TRUE holds
(p => q) => (p => r) = TRUE

proof end;

theorem :: XBOOLEAN:116

for p, q being boolean number st p => q = TRUE & q => p = TRUE holds
p = q

proof end;

theorem :: XBOOLEAN:117

for p, q, r being boolean number st p => q = TRUE & q => r = TRUE holds
p => r = TRUE

proof end;

theorem :: XBOOLEAN:118

for p being boolean number holds (('not' p) => p) => p = TRUE

proof end;

theorem :: XBOOLEAN:119

for p, q being boolean number st 'not' p = TRUE holds
p => q = TRUE ;

theorem :: XBOOLEAN:120

for p, q being boolean number st p => q = TRUE & p => ('not' q) = TRUE holds
'not' p = TRUE

proof end;

theorem :: XBOOLEAN:121

for p, q, r being boolean number holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) = TRUE

proof end;

theorem :: XBOOLEAN:122

for p, q being boolean number holds p 'or' (p => q) = TRUE

proof end;

theorem :: XBOOLEAN:123

for p, q being boolean number holds p => (p 'or' q) = TRUE

proof end;

theorem :: XBOOLEAN:124

for q, p being boolean number holds ('not' q) 'or' ((q => p) => p) = TRUE

proof end;

theorem :: XBOOLEAN:125

for p being boolean number holds p <=> p = TRUE

proof end;

theorem :: XBOOLEAN:126

for p, q, r being boolean number holds (((p <=> q) <=> r) <=> p) <=> (q <=> r) = TRUE

proof end;

theorem :: XBOOLEAN:127

for p, q, r being boolean number st p <=> q = TRUE & q <=> r = TRUE holds
p <=> r = TRUE

proof end;

theorem :: XBOOLEAN:128

for p, q, r, s being boolean number st p <=> q = TRUE & r <=> s = TRUE holds
(p <=> r) <=> (q <=> s) = TRUE

proof end;

theorem :: XBOOLEAN:129

for p being boolean number holds 'not' (p <=> ('not' p)) = TRUE

proof end;

theorem :: XBOOLEAN:130

for p, q, r, s being boolean number st p <=> q = TRUE & r <=> s = TRUE holds
(p '&' r) <=> (q '&' s) = TRUE

proof end;

theorem :: XBOOLEAN:131

for p, q, r, s being boolean number st p <=> q = TRUE & r <=> s = TRUE holds
(p 'or' r) <=> (q 'or' s) = TRUE

proof end;

theorem :: XBOOLEAN:132

for p, q being boolean number holds
( p <=> q = TRUE iff ( p => q = TRUE & q => p = TRUE ) )

proof end;

theorem :: XBOOLEAN:133

for p, q, r, s being boolean number st p <=> q = TRUE & r <=> s = TRUE holds
(p => r) <=> (q => s) = TRUE

proof end;

theorem :: XBOOLEAN:134

for p being boolean number holds 'not' (p 'nor' ('not' p)) = TRUE

proof end;

theorem :: XBOOLEAN:135

for p being boolean number holds p 'nand' ('not' p) = TRUE

proof end;

theorem :: XBOOLEAN:136

for p, q being boolean number holds p 'or' (p 'nand' q) = TRUE

proof end;

theorem :: XBOOLEAN:137

for p, q being boolean number holds p 'nand' (p 'nor' q) = TRUE

proof end;

theorem :: XBOOLEAN:138

for p being boolean number holds p '&' ('not' p) = FALSE

proof end;

theorem :: XBOOLEAN:139

for p being boolean number st p '&' p = FALSE holds
p = FALSE ;

theorem :: XBOOLEAN:140

for p, q being boolean number holds
( not p '&' q = FALSE or p = FALSE or q = FALSE )

proof end;

theorem :: XBOOLEAN:141

for p being boolean number holds 'not' (p => p) = FALSE

proof end;

theorem :: XBOOLEAN:142

for p being boolean number holds p <=> ('not' p) = FALSE

proof end;

theorem :: XBOOLEAN:143

for p being boolean number holds 'not' (p <=> p) = FALSE

proof end;

theorem :: XBOOLEAN:144

for p, q being boolean number holds p '&' (p 'nor' q) = FALSE

proof end;

theorem :: XBOOLEAN:145

for p, q being boolean number holds p 'nor' (p => q) = FALSE

proof end;

theorem :: XBOOLEAN:146

for p, q being boolean number holds p 'nor' (p 'nand' q) = FALSE

proof end;

theorem :: XBOOLEAN:147

for p being boolean number holds p 'xor' p = FALSE

proof end;