:: Propositional Calculus for Boolean Valued Functions, {VII }
:: by Shunichi Kobayashi
::
:: Received February 6, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users
begin
theorem
:: BVFUNC25:1
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
'not'
(
a
'imp'
b
)
=
a
'&'
(
'not'
b
)
proof
end;
theorem
Th2
:
:: BVFUNC25:2
for
Y
being non
empty
set
for
b
,
a
being
Function
of
Y
,
BOOLEAN
holds
(
(
'not'
b
)
'imp'
(
'not'
a
)
)
'imp'
(
a
'imp'
b
)
=
I_el
Y
proof
end;
theorem
Th3
:
:: BVFUNC25:3
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
b
=
(
'not'
b
)
'imp'
(
'not'
a
)
proof
end;
theorem
:: BVFUNC25:4
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
b
=
(
'not'
a
)
'eqv'
(
'not'
b
)
proof
end;
theorem
Th5
:
:: BVFUNC25:5
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
b
=
a
'imp'
(
a
'&'
b
)
proof
end;
theorem
:: BVFUNC25:6
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
b
=
(
a
'or'
b
)
'imp'
(
a
'&'
b
)
proof
end;
theorem
:: BVFUNC25:7
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
(
'not'
a
)
=
O_el
Y
proof
end;
theorem
:: BVFUNC25:8
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
b
'imp'
c
)
=
b
'imp'
(
a
'imp'
c
)
proof
end;
theorem
:: BVFUNC25:9
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
b
'imp'
c
)
=
(
a
'imp'
b
)
'imp'
(
a
'imp'
c
)
proof
end;
theorem
:: BVFUNC25:10
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
b
=
a
'xor'
(
'not'
b
)
proof
end;
theorem
:: BVFUNC25:11
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'&'
(
b
'xor'
c
)
=
(
a
'&'
b
)
'xor'
(
a
'&'
c
)
proof
end;
theorem
:: BVFUNC25:12
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
b
=
'not'
(
a
'xor'
b
)
proof
end;
theorem
:: BVFUNC25:13
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
a
'xor'
a
=
O_el
Y
proof
end;
theorem
:: BVFUNC25:14
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
a
'xor'
(
'not'
a
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:15
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
b
)
'imp'
(
b
'imp'
a
)
=
b
'imp'
a
proof
end;
theorem
Th16
:
:: BVFUNC25:16
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'or'
b
)
'&'
(
(
'not'
a
)
'or'
(
'not'
b
)
)
=
(
(
'not'
a
)
'&'
b
)
'or'
(
a
'&'
(
'not'
b
)
)
proof
end;
theorem
Th17
:
:: BVFUNC25:17
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'&'
b
)
'or'
(
(
'not'
a
)
'&'
(
'not'
b
)
)
=
(
(
'not'
a
)
'or'
b
)
'&'
(
a
'or'
(
'not'
b
)
)
proof
end;
theorem
:: BVFUNC25:18
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'xor'
(
b
'xor'
c
)
=
(
a
'xor'
b
)
'xor'
c
proof
end;
theorem
:: BVFUNC25:19
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
a
'eqv'
(
b
'eqv'
c
)
=
(
a
'eqv'
b
)
'eqv'
c
proof
end;
theorem
:: BVFUNC25:20
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
'not'
(
'not'
a
)
)
'imp'
a
=
I_el
Y
by
BVFUNC_5:7
;
theorem
:: BVFUNC25:21
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'imp'
b
)
'&'
a
)
'imp'
b
=
I_el
Y
proof
end;
theorem
Th22
:
:: BVFUNC25:22
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
(
'not'
a
)
'imp'
a
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:23
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
(
(
'not'
a
)
'imp'
a
)
'eqv'
a
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:24
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'or'
(
a
'imp'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:25
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
b
)
'or'
(
c
'imp'
a
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:26
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
b
)
'or'
(
(
'not'
a
)
'imp'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:27
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
b
)
'or'
(
a
'imp'
(
'not'
b
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:28
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
'not'
a
)
'imp'
(
(
'not'
b
)
'eqv'
(
b
'imp'
a
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:29
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
b
)
'imp'
(
(
(
a
'imp'
c
)
'imp'
b
)
'imp'
b
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:30
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
b
=
a
'eqv'
(
a
'&'
b
)
proof
end;
theorem
:: BVFUNC25:31
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
( (
a
'imp'
b
=
I_el
Y
&
b
'imp'
a
=
I_el
Y
) iff
a
=
b
)
proof
end;
theorem
:: BVFUNC25:32
for
Y
being non
empty
set
for
a
being
Function
of
Y
,
BOOLEAN
holds
a
=
(
'not'
a
)
'imp'
a
proof
end;
theorem
Th33
:
:: BVFUNC25:33
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'imp'
(
(
a
'imp'
b
)
'imp'
a
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:34
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
=
(
a
'imp'
b
)
'imp'
a
proof
end;
theorem
:: BVFUNC25:35
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
=
(
b
'imp'
a
)
'&'
(
(
'not'
b
)
'imp'
a
)
proof
end;
theorem
:: BVFUNC25:36
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'&'
b
=
'not'
(
a
'imp'
(
'not'
b
)
)
proof
end;
theorem
:: BVFUNC25:37
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'or'
b
=
(
'not'
a
)
'imp'
b
proof
end;
theorem
:: BVFUNC25:38
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
a
'or'
b
=
(
a
'imp'
b
)
'imp'
b
proof
end;
theorem
:: BVFUNC25:39
for
Y
being non
empty
set
for
a
,
b
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
b
)
'imp'
(
a
'imp'
a
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:40
for
Y
being non
empty
set
for
a
,
b
,
c
,
d
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
(
b
'imp'
c
)
)
'imp'
(
(
d
'imp'
b
)
'imp'
(
a
'imp'
(
d
'imp'
c
)
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:41
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
(
a
'imp'
b
)
'&'
a
)
'&'
c
)
'imp'
b
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:42
for
Y
being non
empty
set
for
b
,
c
,
a
being
Function
of
Y
,
BOOLEAN
holds
(
b
'imp'
c
)
'imp'
(
(
a
'&'
b
)
'imp'
c
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:43
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'&'
b
)
'imp'
c
)
'imp'
(
(
a
'&'
b
)
'imp'
(
c
'&'
b
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:44
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'imp'
b
)
'imp'
(
(
a
'&'
c
)
'imp'
(
b
'&'
c
)
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:45
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'imp'
b
)
'&'
(
a
'&'
c
)
)
'imp'
(
b
'&'
c
)
=
I_el
Y
proof
end;
theorem
:: BVFUNC25:46
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
a
'&'
(
a
'imp'
b
)
)
'&'
(
b
'imp'
c
)
'<'
c
proof
end;
theorem
:: BVFUNC25:47
for
Y
being non
empty
set
for
a
,
b
,
c
being
Function
of
Y
,
BOOLEAN
holds
(
(
a
'or'
b
)
'&'
(
a
'imp'
c
)
)
'&'
(
b
'imp'
c
)
'<'
(
'not'
a
)
'imp'
(
b
'or'
c
)
proof
end;