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

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

for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds

a '<' b 'imp' c

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)

for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a)

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

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

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

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

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

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

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

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

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)

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

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

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)

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)

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)

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

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

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)

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

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

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;