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