:: Propositional Calculus for Boolean Valued Functions, {VIII}
:: by Shunichi Kobayashi
::
:: Received September 25, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
begin
definition
let
p
,
q
be
boolean-valued
Function
;
func
p
'nand'
q
->
Function
means
:
Def1
:
:: BVFUNC26:def 1
(
dom
it
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
(
p
.
x
)
'nand'
(
q
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
p
.
x
)
'nand'
(
q
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
p
.
x
)
'nand'
(
q
.
x
)
) &
dom
b
2
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
p
.
x
)
'nand'
(
q
.
x
)
) holds
b
1
=
b
2
proof
end;
commutativity
for
b
1
being
Function
for
p
,
q
being
boolean-valued
Function
st
dom
b
1
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
p
.
x
)
'nand'
(
q
.
x
)
) holds
(
dom
b
1
=
(
dom
q
)
/\
(
dom
p
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
q
.
x
)
'nand'
(
p
.
x
)
) )
;
func
p
'nor'
q
->
Function
means
:
Def2
:
:: BVFUNC26:def 2
(
dom
it
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
(
p
.
x
)
'nor'
(
q
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
p
.
x
)
'nor'
(
q
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
p
.
x
)
'nor'
(
q
.
x
)
) &
dom
b
2
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
p
.
x
)
'nor'
(
q
.
x
)
) holds
b
1
=
b
2
proof
end;
commutativity
for
b
1
being
Function
for
p
,
q
being
boolean-valued
Function
st
dom
b
1
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
p
.
x
)
'nor'
(
q
.
x
)
) holds
(
dom
b
1
=
(
dom
q
)
/\
(
dom
p
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
q
.
x
)
'nor'
(
p
.
x
)
) )
;
end;
::
deftheorem
Def1
defines
'nand'
BVFUNC26:def 1 :
for
p
,
q
being
boolean-valued
Function
for
b
3
being
Function
holds
(
b
3
=
p
'nand'
q
iff (
dom
b
3
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
3
holds
b
3
.
x
=
(
p
.
x
)
'nand'
(
q
.
x
)
) ) );
::
deftheorem
Def2
defines
'nor'
BVFUNC26:def 2 :
for
p
,
q
being
boolean-valued
Function
for
b
3
being
Function
holds
(
b
3
=
p
'nor'
q
iff (
dom
b
3
=
(
dom
p
)
/\
(
dom
q
)
& ( for
x
being
set
st
x
in
dom
b
3
holds
b
3
.
x
=
(
p
.
x
)
'nor'
(
q
.
x
)
) ) );
registration
let
p
,
q
be
boolean-valued
Function
;
cluster
p
'nand'
q
->
boolean-valued
;
coherence
p
'nand'
q
is
boolean-valued
proof
end;
cluster
p
'nor'
q
->
boolean-valued
;
coherence
p
'nor'
q
is
boolean-valued
proof
end;
end;
definition
let
A
be non
empty
set
;
let
p
,
q
be
Function
of
A
,
BOOLEAN
;
:: original:
'nand'
redefine
func
p
'nand'
q
->
Function
of
A
,
BOOLEAN
means
:
Def3
:
:: BVFUNC26:def 3
for
x
being
Element
of
A
holds
it
.
x
=
(
p
.
x
)
'nand'
(
q
.
x
)
;
coherence
p
'nand'
q
is
Function
of
A
,
BOOLEAN
proof
end;
compatibility
for
b
1
being
Function
of
A
,
BOOLEAN
holds
(
b
1
=
p
'nand'
q
iff for
x
being
Element
of
A
holds
b
1
.
x
=
(
p
.
x
)
'nand'
(
q
.
x
)
)
proof
end;
:: original:
'nor'
redefine
func
p
'nor'
q
->
Function
of
A
,
BOOLEAN
means
:
Def4
:
:: BVFUNC26:def 4
for
x
being
Element
of
A
holds
it
.
x
=
(
p
.
x
)
'nor'
(
q
.
x
)
;
coherence
p
'nor'
q
is
Function
of
A
,
BOOLEAN
proof
end;
compatibility
for
b
1
being
Function
of
A
,
BOOLEAN
holds
(
b
1
=
p
'nor'
q
iff for
x
being
Element
of
A
holds
b
1
.
x
=
(
p
.
x
)
'nor'
(
q
.
x
)
)
proof
end;
end;
::
deftheorem
Def3
defines
'nand'
BVFUNC26:def 3 :
for
A
being non
empty
set
for
p
,
q
,
b
4
being
Function
of
A
,
BOOLEAN
holds
(
b
4
=
p
'nand'
q
iff for
x
being
Element
of
A
holds
b
4
.
x
=
(
p
.
x
)
'nand'
(
q
.
x
)
);
::
deftheorem
Def4
defines
'nor'
BVFUNC26:def 4 :
for
A
being non
empty
set
for
p
,
q
,
b
4
being
Function
of
A
,
BOOLEAN
holds
(
b
4
=
p
'nor'
q
iff for
x
being
Element
of
A
holds
b
4
.
x
=
(
p
.
x
)
'nor'
(
q
.
x
)
);
definition
let
Y
be non
empty
set
;
let
a
,
b
be
Function
of
Y
,
BOOLEAN
;
:: original:
'nand'
redefine
func
a
'nand'
b
->
Function
of
Y
,
BOOLEAN
;
coherence
a
'nand'
b
is
Function
of
Y
,
BOOLEAN
proof
end;
:: original:
'nor'
redefine
func
a
'nor'
b
->
Function
of
Y
,
BOOLEAN
;
coherence
a
'nor'
b
is
Function
of
Y
,
BOOLEAN
proof
end;
end;
theorem
Th1
:
:: BVFUNC26:1
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
b
=
'not'
(
a
'&'
b
)
proof
end;
theorem
Th2
:
:: BVFUNC26:2
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
b
=
'not'
(
a
'or'
b
)
proof
end;
theorem
Th3
:
:: BVFUNC26:3
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
I_el
Y
)
'nand'
a
=
'not'
a
proof
end;
theorem
Th4
:
:: BVFUNC26:4
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
O_el
Y
)
'nand'
a
=
I_el
Y
proof
end;
theorem
:: BVFUNC26:5
for
Y
being non
empty
set
holds
(
(
O_el
Y
)
'nand'
(
O_el
Y
)
=
I_el
Y
&
(
O_el
Y
)
'nand'
(
I_el
Y
)
=
I_el
Y
&
(
I_el
Y
)
'nand'
(
I_el
Y
)
=
O_el
Y
)
proof
end;
theorem
:: BVFUNC26:6
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
a
'nand'
a
=
'not'
a
&
'not'
(
a
'nand'
a
)
=
a
)
proof
end;
theorem
:: BVFUNC26:7
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
'not'
(
a
'nand'
b
)
=
a
'&'
b
proof
end;
theorem
:: BVFUNC26:8
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
a
'nand'
(
'not'
a
)
=
I_el
Y
&
'not'
(
a
'nand'
(
'not'
a
)
)
=
O_el
Y
)
proof
end;
theorem
Th9
:
:: BVFUNC26:9
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
b
'&'
c
)
=
'not'
(
(
a
'&'
b
)
'&'
c
)
proof
end;
theorem
Th10
:
:: BVFUNC26:10
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
b
'&'
c
)
=
(
a
'&'
b
)
'nand'
c
proof
end;
theorem
Th11
:
:: BVFUNC26:11
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
b
'or'
c
)
=
(
'not'
(
a
'&'
b
)
)
'&'
(
'not'
(
a
'&'
c
)
)
proof
end;
theorem
:: BVFUNC26:12
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
b
'xor'
c
)
=
(
a
'&'
b
)
'eqv'
(
a
'&'
c
)
proof
end;
theorem
:: BVFUNC26:13
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'nand'
(
b
'nand'
c
)
=
(
'not'
a
)
'or'
(
b
'&'
c
)
&
a
'nand'
(
b
'nand'
c
)
=
a
'imp'
(
b
'&'
c
)
)
proof
end;
theorem
:: BVFUNC26:14
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'nand'
(
b
'nor'
c
)
=
(
(
'not'
a
)
'or'
b
)
'or'
c
&
a
'nand'
(
b
'nor'
c
)
=
a
'imp'
(
b
'or'
c
)
)
proof
end;
theorem
:: BVFUNC26:15
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
b
'eqv'
c
)
=
a
'imp'
(
b
'xor'
c
)
proof
end;
theorem
:: BVFUNC26:16
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
a
'&'
b
)
=
a
'nand'
b
proof
end;
theorem
:: BVFUNC26:17
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
a
'or'
b
)
=
(
'not'
a
)
'&'
(
'not'
(
a
'&'
b
)
)
proof
end;
theorem
:: BVFUNC26:18
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
a
'eqv'
b
)
=
a
'imp'
(
a
'xor'
b
)
proof
end;
theorem
:: BVFUNC26:19
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'nand'
(
a
'nand'
b
)
=
(
'not'
a
)
'or'
b
&
a
'nand'
(
a
'nand'
b
)
=
a
'imp'
b
)
proof
end;
theorem
:: BVFUNC26:20
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
a
'nor'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC26:21
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
a
'eqv'
b
)
=
(
'not'
a
)
'or'
(
'not'
b
)
proof
end;
theorem
:: BVFUNC26:22
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'&'
b
=
(
a
'nand'
b
)
'nand'
(
a
'nand'
b
)
proof
end;
theorem
:: BVFUNC26:23
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'nand'
b
)
'nand'
(
a
'nand'
c
)
=
a
'&'
(
b
'or'
c
)
proof
end;
theorem
Th24
:
:: BVFUNC26:24
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
b
'imp'
c
)
=
(
(
'not'
a
)
'or'
b
)
'&'
(
'not'
(
a
'&'
c
)
)
proof
end;
theorem
:: BVFUNC26:25
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
a
'imp'
b
)
=
'not'
(
a
'&'
b
)
proof
end;
theorem
Th26
:
:: BVFUNC26:26
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
I_el
Y
)
'nor'
a
=
O_el
Y
proof
end;
theorem
Th27
:
:: BVFUNC26:27
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
O_el
Y
)
'nor'
a
=
'not'
a
proof
end;
theorem
:: BVFUNC26:28
for
Y
being non
empty
set
holds
(
(
O_el
Y
)
'nor'
(
O_el
Y
)
=
I_el
Y
&
(
O_el
Y
)
'nor'
(
I_el
Y
)
=
O_el
Y
&
(
I_el
Y
)
'nor'
(
I_el
Y
)
=
O_el
Y
)
proof
end;
theorem
:: BVFUNC26:29
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
a
'nor'
a
=
'not'
a
&
'not'
(
a
'nor'
a
)
=
a
)
proof
end;
theorem
:: BVFUNC26:30
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
'not'
(
a
'nor'
b
)
=
a
'or'
b
proof
end;
theorem
:: BVFUNC26:31
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
a
'nor'
(
'not'
a
)
=
O_el
Y
&
'not'
(
a
'nor'
(
'not'
a
)
)
=
I_el
Y
)
proof
end;
theorem
:: BVFUNC26:32
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
'not'
a
)
'&'
(
a
'xor'
b
)
=
(
'not'
a
)
'&'
b
proof
end;
theorem
Th33
:
:: BVFUNC26:33
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
b
'&'
c
)
=
(
'not'
(
a
'or'
b
)
)
'or'
(
'not'
(
a
'or'
c
)
)
proof
end;
theorem
Th34
:
:: BVFUNC26:34
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
b
'or'
c
)
=
'not'
(
(
a
'or'
b
)
'or'
c
)
proof
end;
theorem
Th35
:
:: BVFUNC26:35
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
b
'eqv'
c
)
=
(
'not'
a
)
'&'
(
b
'xor'
c
)
proof
end;
theorem
Th36
:
:: BVFUNC26:36
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
b
'imp'
c
)
=
(
(
'not'
a
)
'&'
b
)
'&'
(
'not'
c
)
proof
end;
theorem
Th37
:
:: BVFUNC26:37
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
b
'nand'
c
)
=
(
(
'not'
a
)
'&'
b
)
'&'
c
proof
end;
theorem
Th38
:
:: BVFUNC26:38
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
b
'nor'
c
)
=
(
'not'
a
)
'&'
(
b
'or'
c
)
proof
end;
theorem
:: BVFUNC26:39
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
a
'&'
b
)
=
'not'
(
a
'&'
(
a
'or'
b
)
)
proof
end;
theorem
:: BVFUNC26:40
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
a
'or'
b
)
=
'not'
(
a
'or'
b
)
proof
end;
theorem
:: BVFUNC26:41
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
a
'eqv'
b
)
=
(
'not'
a
)
'&'
b
proof
end;
theorem
:: BVFUNC26:42
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
a
'imp'
b
)
=
O_el
Y
proof
end;
theorem
:: BVFUNC26:43
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
a
'nand'
b
)
=
O_el
Y
proof
end;
theorem
:: BVFUNC26:44
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
a
'nor'
b
)
=
(
'not'
a
)
'&'
b
proof
end;
theorem
:: BVFUNC26:45
for
Y
being non
empty
set
holds
(
O_el
Y
)
'eqv'
(
O_el
Y
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC26:46
for
Y
being non
empty
set
holds
(
O_el
Y
)
'eqv'
(
I_el
Y
)
=
O_el
Y
proof
end;
theorem
:: BVFUNC26:47
for
Y
being non
empty
set
holds
(
I_el
Y
)
'eqv'
(
I_el
Y
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC26:48
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
a
'eqv'
a
=
I_el
Y
&
'not'
(
a
'eqv'
a
)
=
O_el
Y
)
proof
end;
theorem
:: BVFUNC26:49
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
(
a
'or'
b
)
=
a
'or'
(
'not'
b
)
proof
end;
theorem
Th50
:
:: BVFUNC26:50
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'&'
(
b
'nand'
c
)
=
(
a
'&'
(
'not'
b
)
)
'or'
(
a
'&'
(
'not'
c
)
)
proof
end;
theorem
Th51
:
:: BVFUNC26:51
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'or'
(
b
'nand'
c
)
=
(
a
'or'
(
'not'
b
)
)
'or'
(
'not'
c
)
proof
end;
theorem
Th52
:
:: BVFUNC26:52
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'xor'
(
b
'nand'
c
)
=
(
(
'not'
a
)
'&'
(
'not'
(
b
'&'
c
)
)
)
'or'
(
(
a
'&'
b
)
'&'
c
)
proof
end;
theorem
Th53
:
:: BVFUNC26:53
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
(
b
'nand'
c
)
=
(
a
'&'
(
'not'
(
b
'&'
c
)
)
)
'or'
(
(
(
'not'
a
)
'&'
b
)
'&'
c
)
proof
end;
theorem
Th54
:
:: BVFUNC26:54
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
b
'nand'
c
)
=
'not'
(
(
a
'&'
b
)
'&'
c
)
proof
end;
theorem
Th55
:
:: BVFUNC26:55
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
b
'nand'
c
)
=
'not'
(
(
a
'or'
(
'not'
b
)
)
'or'
(
'not'
c
)
)
proof
end;
theorem
:: BVFUNC26:56
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'&'
(
a
'nand'
b
)
=
a
'&'
(
'not'
b
)
proof
end;
theorem
:: BVFUNC26:57
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'or'
(
a
'nand'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC26:58
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'xor'
(
a
'nand'
b
)
=
(
'not'
a
)
'or'
b
proof
end;
theorem
:: BVFUNC26:59
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
(
a
'nand'
b
)
=
a
'&'
(
'not'
b
)
proof
end;
theorem
:: BVFUNC26:60
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
a
'nand'
b
)
=
'not'
(
a
'&'
b
)
proof
end;
theorem
:: BVFUNC26:61
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nor'
(
a
'nand'
b
)
=
O_el
Y
proof
end;
theorem
Th62
:
:: BVFUNC26:62
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'&'
(
b
'nor'
c
)
=
(
a
'&'
(
'not'
b
)
)
'&'
(
'not'
c
)
proof
end;
theorem
Th63
:
:: BVFUNC26:63
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'or'
(
b
'nor'
c
)
=
(
a
'or'
(
'not'
b
)
)
'&'
(
a
'or'
(
'not'
c
)
)
proof
end;
theorem
Th64
:
:: BVFUNC26:64
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'xor'
(
b
'nor'
c
)
=
(
a
'or'
(
'not'
(
b
'or'
c
)
)
)
'&'
(
(
(
'not'
a
)
'or'
b
)
'or'
c
)
proof
end;
theorem
Th65
:
:: BVFUNC26:65
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
(
b
'nor'
c
)
=
(
(
a
'or'
b
)
'or'
c
)
'&'
(
(
'not'
a
)
'or'
(
'not'
(
b
'or'
c
)
)
)
proof
end;
theorem
Th66
:
:: BVFUNC26:66
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
b
'nor'
c
)
=
'not'
(
a
'&'
(
b
'or'
c
)
)
proof
end;
theorem
Th67
:
:: BVFUNC26:67
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
b
'nor'
c
)
=
(
(
'not'
a
)
'or'
b
)
'or'
c
proof
end;
theorem
:: BVFUNC26:68
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'&'
(
a
'nor'
b
)
=
O_el
Y
proof
end;
theorem
:: BVFUNC26:69
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'or'
(
a
'nor'
b
)
=
a
'or'
(
'not'
b
)
proof
end;
theorem
:: BVFUNC26:70
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'xor'
(
a
'nor'
b
)
=
a
'or'
(
'not'
b
)
proof
end;
theorem
:: BVFUNC26:71
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
(
a
'nor'
b
)
=
(
'not'
a
)
'&'
b
proof
end;
theorem
:: BVFUNC26:72
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
a
'nor'
b
)
=
'not'
(
a
'or'
(
a
'&'
b
)
)
proof
end;
theorem
:: BVFUNC26:73
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'nand'
(
a
'nor'
b
)
=
I_el
Y
proof
end;