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

definition

func FALSE -> object equals :: XBOOLEAN:def 1
0 ;

coherence
0 is object ;

func TRUE -> object equals :: XBOOLEAN:def 2
1;

coherence
1 is object ;

end;

:: deftheorem defines FALSE XBOOLEAN:def 1 :
FALSE = 0 ;

:: deftheorem defines TRUE XBOOLEAN:def 2 :
TRUE = 1;

definition

let p be object ;

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

end;

:: deftheorem Def3 defines boolean XBOOLEAN:def 3 :
for p being object holds
( p is boolean iff ( p = FALSE or p = TRUE ) );

registration

cluster FALSE -> boolean ;

coherence
FALSE is boolean ;

cluster TRUE -> boolean ;

coherence
TRUE is boolean ;

cluster boolean for object ;

existence
ex b₁ being object st b₁ is boolean by Def3;

cluster boolean -> natural for object ;

coherence
for b₁ being object st b₁ is boolean holds
b₁ is natural ;

end;

definition

let p be boolean object ;

func 'not' p -> boolean object equals :: XBOOLEAN:def 4
1 - p;

coherence
1 - p is boolean object

proof end;

involutiveness
for b₁, b₂ being boolean object st b₁ = 1 - b₂ holds
b₂ = 1 - b₁ ;
let q be boolean object ;

func p '&' q -> object equals :: XBOOLEAN:def 5
p * q;

correctness
coherence
p * q is object ;
;
commutativity
for b₁ being object
for p, q being boolean object st b₁ = p * q holds
b₁ = q * p ;
idempotence
for p being boolean object holds p = p * p

proof end;

end;

:: deftheorem defines 'not' XBOOLEAN:def 4 :
for p being boolean object holds 'not' p = 1 - p;

:: deftheorem defines '&' XBOOLEAN:def 5 :
for p, q being boolean object holds p '&' q = p * q;

registration

let p, q be boolean object ;

cluster p '&' q -> boolean ;

coherence
p '&' q is boolean

proof end;

end;

definition

let p, q be boolean object ;

func p 'or' q -> object equals :: XBOOLEAN:def 6
'not' (('not' p) '&' ('not' q));

coherence
'not' (('not' p) '&' ('not' q)) is object ;
commutativity
for b₁ being object
for p, q being boolean object st b₁ = 'not' (('not' p) '&' ('not' q)) holds
b₁ = 'not' (('not' q) '&' ('not' p)) ;
idempotence
for p being boolean object holds p = 'not' (('not' p) '&' ('not' p)) ;

end;

:: deftheorem defines 'or' XBOOLEAN:def 6 :
for p, q being boolean object holds p 'or' q = 'not' (('not' p) '&' ('not' q));

definition

let p, q be boolean object ;

func p => q -> object equals :: XBOOLEAN:def 7
('not' p) 'or' q;

coherence
('not' p) 'or' q is object ;

end;

:: deftheorem defines => XBOOLEAN:def 7 :
for p, q being boolean object holds p => q = ('not' p) 'or' q;

registration

let p, q be boolean object ;

cluster p 'or' q -> boolean ;

coherence
p 'or' q is boolean ;

cluster p => q -> boolean ;

coherence
p => q is boolean ;

end;

definition

let p, q be boolean object ;

func p <=> q -> object equals :: XBOOLEAN:def 8
(p => q) '&' (q => p);

coherence
(p => q) '&' (q => p) is object ;
commutativity
for b₁ being object
for p, q being boolean object st b₁ = (p => q) '&' (q => p) holds
b₁ = (q => p) '&' (p => q) ;

end;

:: deftheorem defines <=> XBOOLEAN:def 8 :
for p, q being boolean object holds p <=> q = (p => q) '&' (q => p);

registration

let p, q be boolean object ;

cluster p <=> q -> boolean ;

coherence
p <=> q is boolean ;

end;

definition

let p, q be boolean object ;

func p 'nand' q -> object equals :: XBOOLEAN:def 9
'not' (p '&' q);

coherence
'not' (p '&' q) is object ;
commutativity
for b₁ being object
for p, q being boolean object st b₁ = 'not' (p '&' q) holds
b₁ = 'not' (q '&' p) ;

func p 'nor' q -> object equals :: XBOOLEAN:def 10
'not' (p 'or' q);

coherence
'not' (p 'or' q) is object ;
commutativity
for b₁ being object
for p, q being boolean object st b₁ = 'not' (p 'or' q) holds
b₁ = 'not' (q 'or' p) ;

func p 'xor' q -> object equals :: XBOOLEAN:def 11
'not' (p <=> q);

coherence
'not' (p <=> q) is object ;
commutativity
for b₁ being object
for p, q being boolean object st b₁ = 'not' (p <=> q) holds
b₁ = 'not' (q <=> p) ;

func p '\' q -> object equals :: XBOOLEAN:def 12
p '&' ('not' q);

coherence
p '&' ('not' q) is object ;

end;

:: deftheorem defines 'nand' XBOOLEAN:def 9 :
for p, q being boolean object holds p 'nand' q = 'not' (p '&' q);

:: deftheorem defines 'nor' XBOOLEAN:def 10 :
for p, q being boolean object holds p 'nor' q = 'not' (p 'or' q);

:: deftheorem defines 'xor' XBOOLEAN:def 11 :
for p, q being boolean object holds p 'xor' q = 'not' (p <=> q);

:: deftheorem defines '\' XBOOLEAN:def 12 :
for p, q being boolean object holds p '\' q = p '&' ('not' q);

registration

let p, q be boolean object ;

cluster p 'nand' q -> boolean ;

coherence
p 'nand' q is boolean ;

cluster p 'nor' q -> boolean ;

coherence
p 'nor' q is boolean ;

cluster p 'xor' q -> boolean ;

coherence
p 'xor' q is boolean ;

cluster p '\' q -> boolean ;

coherence
p '\' q is boolean ;

end;

theorem :: XBOOLEAN:1

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

theorem :: XBOOLEAN:2

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

proof end;

theorem :: XBOOLEAN:3

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

theorem :: XBOOLEAN:4

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

proof end;

theorem :: XBOOLEAN:5

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

proof end;

theorem :: XBOOLEAN:6

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

proof end;

theorem :: XBOOLEAN:7

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

proof end;

theorem :: XBOOLEAN:8

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

proof end;

theorem :: XBOOLEAN:9

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

proof end;

theorem :: XBOOLEAN:10

for p, q, r being boolean object 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 object holds p '&' (('not' p) 'or' q) = p '&' q

proof end;

theorem :: XBOOLEAN:12

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

proof end;

theorem :: XBOOLEAN:13

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

proof end;

theorem :: XBOOLEAN:14

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

proof end;

theorem :: XBOOLEAN:15

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

proof end;

theorem :: XBOOLEAN:16

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

proof end;

theorem :: XBOOLEAN:17

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

proof end;

theorem :: XBOOLEAN:18

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

proof end;

theorem :: XBOOLEAN:19

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

proof end;

theorem :: XBOOLEAN:20

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

proof end;

theorem :: XBOOLEAN:21

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

proof end;

theorem :: XBOOLEAN:22

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

theorem :: XBOOLEAN:23

for p, q, r being boolean object 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 object holds ('not' p) '&' (p <=> q) = (('not' p) '&' ('not' q)) '&' (('not' p) 'or' q)

proof end;

theorem :: XBOOLEAN:25

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

theorem :: XBOOLEAN:26

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

proof end;

theorem :: XBOOLEAN:27

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

proof end;

theorem :: XBOOLEAN:28

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

proof end;

theorem :: XBOOLEAN:29

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

proof end;

theorem :: XBOOLEAN:30

for p, q, r being boolean object 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 object holds p 'nor' p = 'not' p ;

theorem :: XBOOLEAN:32

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

proof end;

theorem :: XBOOLEAN:33

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

proof end;

theorem :: XBOOLEAN:34

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

proof end;

theorem :: XBOOLEAN:35

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

proof end;

theorem :: XBOOLEAN:36

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

proof end;

theorem :: XBOOLEAN:37

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

proof end;

theorem :: XBOOLEAN:38

for p, q, r being boolean object 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 object holds p 'nor' (q 'nor' r) = (('not' p) '&' q) 'or' (('not' p) '&' r)

proof end;

theorem :: XBOOLEAN:40

for p, q, r being boolean object 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 object holds p '&' (q 'nor' r) = (p '&' ('not' q)) '&' ('not' r)

proof end;

theorem :: XBOOLEAN:42

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

proof end;

theorem :: XBOOLEAN:43

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

proof end;

theorem :: XBOOLEAN:44

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

proof end;

theorem :: XBOOLEAN:45

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

proof end;

theorem :: XBOOLEAN:46

for p, q, r being boolean object 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 object holds p 'nor' (p <=> q) = ('not' p) '&' q

proof end;

theorem :: XBOOLEAN:48

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

proof end;

theorem :: XBOOLEAN:49

for p, q, r being boolean object 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 object holds p <=> q = (p '&' q) 'or' (p 'nor' q)

proof end;

theorem :: XBOOLEAN:51

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

theorem :: XBOOLEAN:52

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

proof end;

theorem :: XBOOLEAN:53

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

proof end;

theorem :: XBOOLEAN:54

for p, q, r being boolean object 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 object holds p 'nand' (q 'or' r) = ('not' (p '&' q)) '&' ('not' (p '&' r))

proof end;

theorem :: XBOOLEAN:56

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

proof end;

theorem :: XBOOLEAN:57

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

proof end;

theorem :: XBOOLEAN:58

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

proof end;

theorem :: XBOOLEAN:59

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

proof end;

theorem :: XBOOLEAN:60

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

proof end;

theorem :: XBOOLEAN:61

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

proof end;

theorem :: XBOOLEAN:62

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

proof end;

theorem :: XBOOLEAN:63

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

proof end;

theorem :: XBOOLEAN:64

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

proof end;

theorem :: XBOOLEAN:65

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

proof end;

::p 'nand' q

theorem :: XBOOLEAN:66

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

theorem :: XBOOLEAN:67

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

proof end;

theorem :: XBOOLEAN:68

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

proof end;

theorem :: XBOOLEAN:69

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

proof end;

theorem :: XBOOLEAN:70

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

proof end;

theorem :: XBOOLEAN:71

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

proof end;

theorem :: XBOOLEAN:72

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

proof end;

theorem :: XBOOLEAN:73

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

proof end;

theorem :: XBOOLEAN:74

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

proof end;

theorem :: XBOOLEAN:75

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

proof end;

theorem :: XBOOLEAN:76

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

proof end;

theorem :: XBOOLEAN:77

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

proof end;

theorem :: XBOOLEAN:78

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

proof end;

theorem :: XBOOLEAN:79

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

proof end;

theorem :: XBOOLEAN:80

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

proof end;

::q => p

theorem :: XBOOLEAN:81

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

proof end;

theorem :: XBOOLEAN:82

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

proof end;

theorem :: XBOOLEAN:83

for p, q, r being boolean object 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 object holds ('not' p) 'xor' (p => q) = p '&' q

proof end;

theorem :: XBOOLEAN:85

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

proof end;

theorem :: XBOOLEAN:86

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

proof end;

theorem :: XBOOLEAN:87

for p, q being boolean object 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 object holds p 'xor' (p <=> q) = 'not' q

proof end;

theorem :: XBOOLEAN:89

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

proof end;

theorem :: XBOOLEAN:90

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

proof end;

theorem :: XBOOLEAN:91

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

proof end;

theorem :: XBOOLEAN:92

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

proof end;

theorem :: XBOOLEAN:93

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

proof end;

theorem :: XBOOLEAN:94

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

proof end;

theorem :: XBOOLEAN:95

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

proof end;

theorem :: XBOOLEAN:96

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

proof end;

theorem :: XBOOLEAN:97

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

proof end;

theorem :: XBOOLEAN:98

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

proof end;

theorem :: XBOOLEAN:99

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

proof end;

theorem :: XBOOLEAN:100

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

proof end;

theorem :: XBOOLEAN:101

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

proof end;

theorem :: XBOOLEAN:102

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

proof end;

theorem :: XBOOLEAN:103

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

proof end;

theorem :: XBOOLEAN:104

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

proof end;

theorem :: XBOOLEAN:105

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

proof end;

theorem :: XBOOLEAN:106

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

proof end;

theorem :: XBOOLEAN:107

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

proof end;

theorem :: XBOOLEAN:108

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

proof end;

theorem :: XBOOLEAN:109

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

proof end;

theorem :: XBOOLEAN:110

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

proof end;

theorem :: XBOOLEAN:111

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

proof end;

theorem :: XBOOLEAN:112

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

proof end;

theorem :: XBOOLEAN:113

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

proof end;

theorem :: XBOOLEAN:114

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

proof end;

theorem :: XBOOLEAN:115

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

proof end;

theorem :: XBOOLEAN:116

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

proof end;

theorem :: XBOOLEAN:117

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

proof end;

theorem :: XBOOLEAN:118

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

proof end;

theorem :: XBOOLEAN:119

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

theorem :: XBOOLEAN:120

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

proof end;

theorem :: XBOOLEAN:121

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

proof end;

theorem :: XBOOLEAN:122

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

proof end;

theorem :: XBOOLEAN:123

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

proof end;

theorem :: XBOOLEAN:124

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

proof end;

theorem :: XBOOLEAN:125

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

proof end;

theorem :: XBOOLEAN:126

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

proof end;

theorem :: XBOOLEAN:127

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

proof end;

theorem :: XBOOLEAN:128

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

proof end;

theorem :: XBOOLEAN:129

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

proof end;

theorem :: XBOOLEAN:130

for p, q, r, s being boolean object 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 object 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 object holds
( p <=> q = TRUE iff ( p => q = TRUE & q => p = TRUE ) )

proof end;

theorem :: XBOOLEAN:133

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

proof end;

theorem :: XBOOLEAN:134

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

proof end;

theorem :: XBOOLEAN:135

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

proof end;

theorem :: XBOOLEAN:136

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

proof end;

theorem :: XBOOLEAN:137

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

proof end;

theorem :: XBOOLEAN:138

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

proof end;

theorem :: XBOOLEAN:139

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

theorem :: XBOOLEAN:140

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

theorem :: XBOOLEAN:141

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

proof end;

theorem :: XBOOLEAN:142

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

proof end;

theorem :: XBOOLEAN:143

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

proof end;

theorem :: XBOOLEAN:144

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

proof end;

theorem :: XBOOLEAN:145

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

proof end;

theorem :: XBOOLEAN:146

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

proof end;

theorem :: XBOOLEAN:147

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

proof end;