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

theorem :: BVFUNC_4:1

for Y being non empty set
for a, b, c being Element of Funcs 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 Element of Funcs 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 Element of Funcs Y,BOOLEAN holds a 'or' (a '&' b) = a

proof end;

theorem :: BVFUNC_4:4

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

proof end;

theorem Th5: :: BVFUNC_4:5

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

proof end;

theorem :: BVFUNC_4:6

for Y being non empty set
for a being Element of Funcs 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 Element of Funcs 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 Element of Funcs 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 Element of Funcs 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 Element of Funcs 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

canceled;

theorem :: BVFUNC_4:12

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN st a 'eqv' b = I_el Y holds
('not' a) 'eqv' ('not' b) = I_el Y

proof end;

theorem :: BVFUNC_4:13

for Y being non empty set
for a, b, c, d being Element of Funcs 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:14

for Y being non empty set
for a, b, c, d being Element of Funcs 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:15

for Y being non empty set
for a, b, c, d being Element of Funcs 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:16

for Y being non empty set
for a, b, c, d being Element of Funcs 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;

theorem :: BVFUNC_4:17

for Y being non empty set
for a, b being Element of Funcs 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:18

for Y being non empty set
for a being Element of Funcs 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:19

for Y being non empty set
for a, u being Element of Funcs 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:20

for Y being non empty set
for u being Element of Funcs 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:21

for Y being non empty set
for u being Element of Funcs 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:22

for Y being non empty set
for u being Element of Funcs 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:23

for Y being non empty set
for u being Element of Funcs 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:24

for Y being non empty set
for a, b being Element of Funcs 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:25

for Y being non empty set
for a, b being Element of Funcs 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:26

for Y being non empty set
for a, u being Element of Funcs 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:27

for Y being non empty set
for a, b being Element of Funcs 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:28

for Y being non empty set
for a, b being Element of Funcs 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;