:: A Theory of Boolean Valued Functions and Quantifiers withRespect to Partitions
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received December 21, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem Th1: :: BVFUNC_2:1
:: deftheorem Def1 defines '/\' BVFUNC_2:def 1 :
:: deftheorem Def2 defines is_upper_min_depend_of BVFUNC_2:def 2 :
theorem Th2: :: BVFUNC_2:2
:: deftheorem Def3 defines '\/' BVFUNC_2:def 3 :
theorem :: BVFUNC_2:3
theorem :: BVFUNC_2:4
:: deftheorem defines generating BVFUNC_2:def 4 :
:: deftheorem defines independent BVFUNC_2:def 5 :
:: deftheorem defines is_a_coordinate BVFUNC_2:def 6 :
:: deftheorem defines CompF BVFUNC_2:def 7 :
:: deftheorem Def8 defines is_independent_of BVFUNC_2:def 8 :
:: deftheorem defines All BVFUNC_2:def 9 :
:: deftheorem defines Ex BVFUNC_2:def 10 :
theorem :: BVFUNC_2:5
theorem :: BVFUNC_2:6
theorem :: BVFUNC_2:7
theorem :: BVFUNC_2:8
theorem :: BVFUNC_2:9
theorem :: BVFUNC_2:10
theorem :: BVFUNC_2:11
theorem :: BVFUNC_2:12
theorem :: BVFUNC_2:13
canceled;
theorem :: BVFUNC_2:14
theorem :: BVFUNC_2:15
theorem :: BVFUNC_2:16
canceled;
theorem :: BVFUNC_2:17
theorem :: BVFUNC_2:18
theorem :: BVFUNC_2:19
theorem :: BVFUNC_2:20
theorem :: BVFUNC_2:21
theorem :: BVFUNC_2:22
theorem :: BVFUNC_2:23
theorem Th24: :: BVFUNC_2:24
theorem :: BVFUNC_2:25
theorem :: BVFUNC_2:26
theorem Th27: :: BVFUNC_2:27
theorem :: BVFUNC_2:28
theorem :: BVFUNC_2:29
theorem Th30: :: BVFUNC_2:30
theorem :: BVFUNC_2:31
theorem Th32: :: BVFUNC_2:32
theorem :: BVFUNC_2:33
theorem Th34: :: BVFUNC_2:34
theorem :: BVFUNC_2:35
theorem Th36: :: BVFUNC_2:36
theorem :: BVFUNC_2:37
theorem :: BVFUNC_2:38
theorem :: BVFUNC_2:39
theorem Th40: :: BVFUNC_2:40
theorem :: BVFUNC_2:41