:: Propositional Calculus for Boolean Valued Functions, II
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users
begin
theorem
:: BVFUNC_6:1
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
b
'imp'
(
a
'&'
b
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:2
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
b
)
'imp'
(
(
b
'imp'
a
)
'imp'
(
a
'eqv'
b
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:3
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'or'
b
)
'eqv'
(
b
'or'
a
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:4
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'&'
b
)
'imp'
c
)
'imp'
(
a
'imp'
(
b
'imp'
c
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:5
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
(
b
'imp'
c
)
)
'imp'
(
(
a
'&'
b
)
'imp'
c
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:6
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
c
'imp'
a
)
'imp'
(
(
c
'imp'
b
)
'imp'
(
c
'imp'
(
a
'&'
b
)
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:7
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'or'
b
)
'imp'
c
)
'imp'
(
(
a
'imp'
c
)
'or'
(
b
'imp'
c
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:8
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
c
)
'imp'
(
(
b
'imp'
c
)
'imp'
(
(
a
'or'
b
)
'imp'
c
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:9
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'imp'
c
)
'&'
(
b
'imp'
c
)
)
'imp'
(
(
a
'or'
b
)
'imp'
c
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:10
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
(
b
'&'
(
'not'
b
)
)
)
'imp'
(
'not'
a
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:11
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'or'
b
)
'&'
(
a
'or'
c
)
)
'imp'
(
a
'or'
(
b
'&'
c
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:12
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'&'
(
b
'or'
c
)
)
'imp'
(
(
a
'&'
b
)
'or'
(
a
'&'
c
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:13
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'or'
c
)
'&'
(
b
'or'
c
)
)
'imp'
(
(
a
'&'
b
)
'or'
c
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:14
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'or'
b
)
'&'
c
)
'imp'
(
(
a
'&'
c
)
'or'
(
b
'&'
c
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:15
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
st
a
'&'
b
=
I_el
Y
holds
a
'or'
b
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:16
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
st
a
'imp'
b
=
I_el
Y
holds
(
a
'or'
c
)
'imp'
(
b
'or'
c
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:17
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
st
a
'imp'
b
=
I_el
Y
holds
(
a
'&'
c
)
'imp'
(
b
'&'
c
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:18
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
st
c
'imp'
a
=
I_el
Y
&
c
'imp'
b
=
I_el
Y
holds
c
'imp'
(
a
'&'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:19
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
st
a
'imp'
c
=
I_el
Y
&
b
'imp'
c
=
I_el
Y
holds
(
a
'or'
b
)
'imp'
c
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:20
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
st
a
'or'
b
=
I_el
Y
&
'not'
a
=
I_el
Y
holds
b
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:21
for
Y
being non
empty
set
for
a
,
b
,
c
,
d
being
Function
of
Y
,
BOOLEAN
st
a
'imp'
b
=
I_el
Y
&
c
'imp'
d
=
I_el
Y
holds
(
a
'&'
c
)
'imp'
(
b
'&'
d
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:22
for
Y
being non
empty
set
for
a
,
b
,
c
,
d
being
Function
of
Y
,
BOOLEAN
st
a
'imp'
b
=
I_el
Y
&
c
'imp'
d
=
I_el
Y
holds
(
a
'or'
c
)
'imp'
(
b
'or'
d
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:23
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
st
(
a
'&'
(
'not'
b
)
)
'imp'
(
'not'
a
)
=
I_el
Y
holds
a
'imp'
b
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:24
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
st
a
'imp'
(
'not'
b
)
=
I_el
Y
holds
b
'imp'
(
'not'
a
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:25
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
st
(
'not'
a
)
'imp'
b
=
I_el
Y
holds
(
'not'
b
)
'imp'
a
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:26
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
a
'or'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:27
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'or'
b
)
'imp'
(
(
'not'
a
)
'imp'
b
)
=
I_el
Y
proof
end;
theorem
Th28
:
:: BVFUNC_6:28
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
'not'
(
a
'or'
b
)
)
'imp'
(
(
'not'
a
)
'&'
(
'not'
b
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:29
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
(
'not'
a
)
'&'
(
'not'
b
)
)
'imp'
(
'not'
(
a
'or'
b
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:30
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
'not'
(
a
'or'
b
)
)
'imp'
(
'not'
a
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:31
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
a
'or'
a
)
'imp'
a
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:32
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'&'
(
'not'
a
)
)
'imp'
b
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:33
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
b
)
'imp'
(
(
'not'
a
)
'or'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:34
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'&'
b
)
'imp'
(
'not'
(
a
'imp'
(
'not'
b
)
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:35
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
'not'
(
a
'imp'
(
'not'
b
)
)
)
'imp'
(
a
'&'
b
)
=
I_el
Y
proof
end;
theorem
Th36
:
:: BVFUNC_6:36
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
'not'
(
a
'&'
b
)
)
'imp'
(
(
'not'
a
)
'or'
(
'not'
b
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:37
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
(
'not'
a
)
'or'
(
'not'
b
)
)
'imp'
(
'not'
(
a
'&'
b
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:38
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'&'
b
)
'imp'
a
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:39
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'&'
b
)
'imp'
(
a
'or'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:40
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'&'
b
)
'imp'
b
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:41
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
a
'&'
a
)
=
I_el
Y
proof
end;
theorem
Th42
:
:: BVFUNC_6:42
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'eqv'
b
)
'imp'
(
a
'imp'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:43
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'eqv'
b
)
'imp'
(
b
'imp'
a
)
=
I_el
Y
by
Th42
;
theorem
:: BVFUNC_6:44
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'or'
b
)
'or'
c
)
'imp'
(
a
'or'
(
b
'or'
c
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:45
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'&'
b
)
'&'
c
)
'imp'
(
a
'&'
(
b
'&'
c
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC_6:46
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'or'
(
b
'or'
c
)
)
'imp'
(
(
a
'or'
b
)
'or'
c
)
=
I_el
Y
proof
end;