:: 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 b1 being object st b1 is boolean by Def3;
cluster boolean -> natural for object ;
coherence
for b1 being object st b1 is boolean holds
b1 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 b1, b2 being boolean object st b1 = 1 - b2 holds
b2 = 1 - b1 ;
let q be boolean object ;
func p '&' q -> object equals :: XBOOLEAN:def 5
p * q;
correctness
coherence
p * q is object ;
;
commutativity
for b1 being object
for p, q being boolean object st b1 = p * q holds
b1 = 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 b1 being object
for p, q being boolean object st b1 = 'not' (('not' p) '&' ('not' q)) holds
b1 = '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 b1 being object
for p, q being boolean object st b1 = (p => q) '&' (q => p) holds
b1 = (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 b1 being object
for p, q being boolean object st b1 = 'not' (p '&' q) holds
b1 = '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 b1 being object
for p, q being boolean object st b1 = 'not' (p 'or' q) holds
b1 = 'not' (q 'or' p) ;
func p 'xor' q -> object equals :: XBOOLEAN:def 11
 'not' (p <=> q);
coherence
'not' (p <=> q) is object ;
commutativity
for b1 being object
for p, q being boolean object st b1 = 'not' (p <=> q) holds
b1 = '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;