:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, MARGREL1, PARTIT1, BVFUNC_1, XBOOLEAN,
FUNCT_1, EQREL_1, BVFUNC_2;
notations TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1,
FUNCT_2, EQREL_1, BVFUNC_1, BVFUNC_2;
constructors BINARITH, BVFUNC_1, BVFUNC_2, NUMBERS;
registrations XBOOLEAN, MARGREL1;
requirements ARITHM, NUMERALS;
begin
::Chap. 1 Preliminaries
reserve Y for non empty set;
theorem :: BVFUNC_4:1
for a,b,c being Function of Y,BOOLEAN holds a '<' (b 'imp' c)
implies a '&' b '<' c;
theorem :: BVFUNC_4:2
for a,b,c being Function of Y,BOOLEAN holds a '&' b '<' c
implies a '<' (b 'imp' c);
theorem :: BVFUNC_4:3
for a,b being Function of Y,BOOLEAN holds a 'or' (a '&' b) = a;
theorem :: BVFUNC_4:4
for a,b being Function of Y,BOOLEAN holds a '&' (a 'or' b) = a;
theorem :: BVFUNC_4:5
for a being Function of Y,BOOLEAN holds a '&' 'not' a = O_el(Y);
theorem :: BVFUNC_4:6
for a being Function of Y,BOOLEAN holds a 'or' 'not' a = I_el(Y);
theorem :: BVFUNC_4:7
for a,b being Function of Y,BOOLEAN
holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a);
theorem :: BVFUNC_4:8
for a,b being Function of Y,BOOLEAN holds a 'imp' b = 'not' a 'or' b;
theorem :: BVFUNC_4:9
for a,b being Function of Y,BOOLEAN
holds a 'xor' b = ('not' a '&' b) 'or' (a '&' 'not' b);
theorem :: BVFUNC_4:10
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);
theorem :: BVFUNC_4:11
for a,b being Function of Y,BOOLEAN holds a 'eqv' b=I_el(Y)
implies 'not' a 'eqv' 'not' b=I_el(Y);
theorem :: BVFUNC_4:12
for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y
) & (c 'eqv' d)=I_el(Y) implies ((a '&' c) 'eqv' (b '&' d))=I_el(Y);
theorem :: BVFUNC_4:13
for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y
) & (c 'eqv' d)=I_el(Y) implies ((a 'imp' c) 'eqv' (b 'imp' d))=I_el(Y);
theorem :: BVFUNC_4:14
for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y
) & (c 'eqv' d)=I_el(Y) implies ((a 'or' c) 'eqv' (b 'or' d))=I_el(Y);
theorem :: BVFUNC_4:15
for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y
) & (c 'eqv' d)=I_el(Y) implies ((a 'eqv' c) 'eqv' (b 'eqv' d))=I_el(Y);
begin
::Chap. 2 Predicate Calculus
theorem :: BVFUNC_4:16
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), 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);
theorem :: BVFUNC_4:17
for a being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA,PB being a_partition of Y holds All(a,PA,G) '<' Ex(a,PB,G);
theorem :: BVFUNC_4:18
for a,u being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y st a 'imp' u = I_el(Y) holds All(a,PA,
G) 'imp' u = I_el(Y);
theorem :: BVFUNC_4:19
for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA being a_partition of Y st u is_independent_of PA,G holds Ex(u,PA,G) '<'
u;
theorem :: BVFUNC_4:20
for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA being a_partition of Y st u is_independent_of PA,G holds u '<' All(u,PA,
G);
theorem :: BVFUNC_4:21
for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA,PB being a_partition of Y st u is_independent_of PB,G holds All(u,PA,G)
'<' All(u,PB,G);
theorem :: BVFUNC_4:22
for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA,PB being a_partition of Y st u is_independent_of PA,G holds Ex(u,PA,G)
'<' Ex(u,PB,G);
theorem :: BVFUNC_4:23
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds All(a 'eqv' b,PA,G) '<' All(a,PA
,G) 'eqv' All(b,PA,G);
theorem :: BVFUNC_4:24
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds All(a '&' b,PA,G) '<' a '&' All(
b,PA,G);
theorem :: BVFUNC_4:25
for a,u being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds All(a,PA,G) 'imp' u '<' Ex(a
'imp' u,PA,G);
theorem :: BVFUNC_4:26
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds (a 'eqv' b)=I_el(Y) implies (All
(a,PA,G) 'eqv' All(b,PA,G))=I_el(Y);
theorem :: BVFUNC_4:27
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds (a 'eqv' b)=I_el(Y) implies (Ex(
a,PA,G) 'eqv' Ex(b,PA,G))=I_el(Y);