:: On the Arithmetic of Boolean Values
:: by Library Committee
::
:: Received November 30, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users
begin
definition
func
FALSE
->
set
equals
:: XBOOLEAN:def 1
0
;
coherence
0
is
set
;
func
TRUE
->
set
equals
:: XBOOLEAN:def 2
1;
coherence
1 is
set
;
end;
::
deftheorem
defines
FALSE
XBOOLEAN:def 1 :
FALSE
=
0
;
::
deftheorem
defines
TRUE
XBOOLEAN:def 2 :
TRUE
=
1;
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 :
for
p
being
set
holds
(
p
is
boolean
iff (
p
=
FALSE
or
p
=
TRUE
) );
registration
cluster
FALSE
->
boolean
;
coherence
FALSE
is
boolean
by
Def3
;
cluster
TRUE
->
boolean
;
coherence
TRUE
is
boolean
by
Def3
;
cluster
boolean
for
set
;
existence
ex
b
1
being
number
st
b
1
is
boolean
by
Def3
;
cluster
boolean
->
natural
for
set
;
coherence
for
b
1
being
number
st
b
1
is
boolean
holds
b
1
is
natural
proof
end;
end;
definition
let
p
be
boolean
number
;
func
'not'
p
->
boolean
number
equals
:: XBOOLEAN:def 4
1
-
p
;
coherence
1
-
p
is
boolean
number
proof
end;
involutiveness
for
b
1
,
b
2
being
boolean
number
st
b
1
=
1
-
b
2
holds
b
2
=
1
-
b
1
;
let
q
be
boolean
number
;
func
p
'&'
q
->
set
equals
:: XBOOLEAN:def 5
p
*
q
;
correctness
coherence
p
*
q
is
set
;
;
commutativity
for
b
1
being
set
for
p
,
q
being
boolean
number
st
b
1
=
p
*
q
holds
b
1
=
q
*
p
;
idempotence
for
p
being
boolean
number
holds
p
=
p
*
p
proof
end;
end;
::
deftheorem
defines
'not'
XBOOLEAN:def 4 :
for
p
being
boolean
number
holds
'not'
p
=
1
-
p
;
::
deftheorem
defines
'&'
XBOOLEAN:def 5 :
for
p
,
q
being
boolean
number
holds
p
'&'
q
=
p
*
q
;
registration
let
p
,
q
be
boolean
number
;
cluster
p
'&'
q
->
boolean
;
coherence
p
'&'
q
is
boolean
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
'not'
(
(
'not'
p
)
'&'
(
'not'
q
)
)
is
set
;
commutativity
for
b
1
being
set
for
p
,
q
being
boolean
number
st
b
1
=
'not'
(
(
'not'
p
)
'&'
(
'not'
q
)
)
holds
b
1
=
'not'
(
(
'not'
q
)
'&'
(
'not'
p
)
)
;
idempotence
for
p
being
boolean
number
holds
p
=
'not'
(
(
'not'
p
)
'&'
(
'not'
p
)
)
;
end;
::
deftheorem
defines
'or'
XBOOLEAN:def 6 :
for
p
,
q
being
boolean
number
holds
p
'or'
q
=
'not'
(
(
'not'
p
)
'&'
(
'not'
q
)
)
;
definition
let
p
,
q
be
boolean
number
;
func
p
=>
q
->
set
equals
:: XBOOLEAN:def 7
(
'not'
p
)
'or'
q
;
coherence
(
'not'
p
)
'or'
q
is
set
;
end;
::
deftheorem
defines
=>
XBOOLEAN:def 7 :
for
p
,
q
being
boolean
number
holds
p
=>
q
=
(
'not'
p
)
'or'
q
;
registration
let
p
,
q
be
boolean
number
;
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
number
;
func
p
<=>
q
->
set
equals
:: XBOOLEAN:def 8
(
p
=>
q
)
'&'
(
q
=>
p
)
;
coherence
(
p
=>
q
)
'&'
(
q
=>
p
)
is
set
;
commutativity
for
b
1
being
set
for
p
,
q
being
boolean
number
st
b
1
=
(
p
=>
q
)
'&'
(
q
=>
p
)
holds
b
1
=
(
q
=>
p
)
'&'
(
p
=>
q
)
;
end;
::
deftheorem
defines
<=>
XBOOLEAN:def 8 :
for
p
,
q
being
boolean
number
holds
p
<=>
q
=
(
p
=>
q
)
'&'
(
q
=>
p
)
;
registration
let
p
,
q
be
boolean
number
;
cluster
p
<=>
q
->
boolean
;
coherence
p
<=>
q
is
boolean
;
end;
definition
let
p
,
q
be
boolean
number
;
func
p
'nand'
q
->
set
equals
:: XBOOLEAN:def 9
'not'
(
p
'&'
q
)
;
coherence
'not'
(
p
'&'
q
)
is
set
;
commutativity
for
b
1
being
set
for
p
,
q
being
boolean
number
st
b
1
=
'not'
(
p
'&'
q
)
holds
b
1
=
'not'
(
q
'&'
p
)
;
func
p
'nor'
q
->
set
equals
:: XBOOLEAN:def 10
'not'
(
p
'or'
q
)
;
coherence
'not'
(
p
'or'
q
)
is
set
;
commutativity
for
b
1
being
set
for
p
,
q
being
boolean
number
st
b
1
=
'not'
(
p
'or'
q
)
holds
b
1
=
'not'
(
q
'or'
p
)
;
func
p
'xor'
q
->
set
equals
:: XBOOLEAN:def 11
'not'
(
p
<=>
q
)
;
coherence
'not'
(
p
<=>
q
)
is
set
;
commutativity
for
b
1
being
set
for
p
,
q
being
boolean
number
st
b
1
=
'not'
(
p
<=>
q
)
holds
b
1
=
'not'
(
q
<=>
p
)
;
func
p
'\'
q
->
set
equals
:: XBOOLEAN:def 12
p
'&'
(
'not'
q
)
;
coherence
p
'&'
(
'not'
q
)
is
set
;
end;
::
deftheorem
defines
'nand'
XBOOLEAN:def 9 :
for
p
,
q
being
boolean
number
holds
p
'nand'
q
=
'not'
(
p
'&'
q
)
;
::
deftheorem
defines
'nor'
XBOOLEAN:def 10 :
for
p
,
q
being
boolean
number
holds
p
'nor'
q
=
'not'
(
p
'or'
q
)
;
::
deftheorem
defines
'xor'
XBOOLEAN:def 11 :
for
p
,
q
being
boolean
number
holds
p
'xor'
q
=
'not'
(
p
<=>
q
)
;
::
deftheorem
defines
'\'
XBOOLEAN:def 12 :
for
p
,
q
being
boolean
number
holds
p
'\'
q
=
p
'&'
(
'not'
q
)
;
registration
let
p
,
q
be
boolean
number
;
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;
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;
::p 'nand' q
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;
::q => p
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;