:: Predicate Calculus for Boolean Valued Functions, II
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

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 '&' b '<' c

proof end;

theorem :: BVFUNC_4:2

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '<' b 'imp' c

proof end;

theorem :: BVFUNC_4:3

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a '&' b) = a

proof end;

theorem :: BVFUNC_4:4

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'or' b) = a

proof end;

theorem Th5: :: BVFUNC_4:5

for Y being non empty set
for a being Function of Y,BOOLEAN holds a '&' ('not' a) = O_el Y

proof end;

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

proof end;

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) '&' (b 'imp' a)

proof end;

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

proof end;

theorem :: BVFUNC_4:9

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b))

proof end;

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 & b 'imp' a = I_el Y ) )

proof end;

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

proof end;

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 & c 'eqv' d = I_el Y holds
(a '&' c) 'eqv' (b '&' d) = I_el Y

proof end;

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 & c 'eqv' d = I_el Y holds
(a 'imp' c) 'eqv' (b 'imp' d) = I_el Y

proof end;

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 & c 'eqv' d = I_el Y holds
(a 'or' c) 'eqv' (b 'or' d) = I_el Y

proof end;

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 & c 'eqv' d = I_el Y holds
(a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y

proof end;

::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)) '&' (All ((b 'imp' a),PA,G))

proof end;

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)

proof end;

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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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))

proof end;

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 '&' b),PA,G) '<' a '&' (All (b,PA,G))

proof end;

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)

proof end;

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

proof end;

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

proof end;