:: Predicate 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_4:1
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '<' b 'imp' c holds
a '&amp;' b '<' c
proofend;

theorem :: BVFUNC_4:2
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '&amp;' b '<' c holds
a '<' b 'imp' c
proofend;

theorem :: BVFUNC_4:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a '&amp;' b) = a
proofend;

theorem :: BVFUNC_4:4
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&amp;' (a 'or' b) = a
proofend;

theorem Th5: :: BVFUNC_4:5
for Y being non empty set
for a being Function of Y,BOOLEAN holds a '&amp;' ('not' a) = O_el Y
proofend;

theorem :: BVFUNC_4:6
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' ('not' a) = I_el Y
proofend;

theorem Th7: :: BVFUNC_4:7
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'imp' b) '&amp;' (b 'imp' a)
proofend;

theorem Th8: :: BVFUNC_4:8
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' a) 'or' b
proofend;

theorem :: BVFUNC_4:9
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = (('not' a) '&amp;' b) 'or' (a '&amp;' ('not' b))
proofend;

theorem Th10: :: BVFUNC_4:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y &amp; b 'imp' a = I_el Y ) )
proofend;

theorem :: BVFUNC_4:11
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'eqv' b = I_el Y holds
('not' a) 'eqv' ('not' b) = I_el Y
proofend;

theorem :: BVFUNC_4:12
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y &amp; c 'eqv' d = I_el Y holds
(a '&amp;' c) 'eqv' (b '&amp;' d) = I_el Y
proofend;

theorem :: BVFUNC_4:13
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y &amp; c 'eqv' d = I_el Y holds
(a 'imp' c) 'eqv' (b 'imp' d) = I_el Y
proofend;

theorem :: BVFUNC_4:14
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y &amp; c 'eqv' d = I_el Y holds
(a 'or' c) 'eqv' (b 'or' d) = I_el Y
proofend;

theorem :: BVFUNC_4:15
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y &amp; c 'eqv' d = I_el Y holds
(a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y
proofend;

begin

::Chap. 2 Predicate Calculus
theorem :: BVFUNC_4:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&amp;' (All ((b 'imp' a),PA,G))
proofend;

theorem :: BVFUNC_4:17
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)
proofend;

theorem :: BVFUNC_4:18
for Y being non empty set
for a, u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'imp' u = I_el Y holds
(All (a,PA,G)) 'imp' u = I_el Y
proofend;

theorem :: BVFUNC_4:19
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' u
proofend;

theorem :: BVFUNC_4:20
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st u is_independent_of PA,G holds
u '<' All (u,PA,G)
proofend;

theorem :: BVFUNC_4:21
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PB,G holds
All (u,PA,G) '<' All (u,PB,G)
proofend;

theorem :: BVFUNC_4:22
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' Ex (u,PB,G)
proofend;

theorem :: BVFUNC_4:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G))
proofend;

theorem :: BVFUNC_4:24
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds All ((a '&amp;' b),PA,G) '<' a '&amp;' (All (b,PA,G))
proofend;

theorem :: BVFUNC_4:25
for Y being non empty set
for a, u being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
proofend;

theorem :: BVFUNC_4:26
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
proofend;

theorem :: BVFUNC_4:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y
proofend;