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

begin

theorem Th1: :: BVFUNC13:1

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ('not' (All a,A,G)),B,G '<' 'not' (All (All a,B,G),A,G)

proof end;

theorem Th2: :: BVFUNC13:2

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (All ('not' a),A,G),B,G '<' 'not' (All (All a,B,G),A,G)

proof end;

theorem Th3: :: BVFUNC13:3

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ('not' (Ex a,A,G)),B,G '<' 'not' (All (All a,B,G),A,G)

proof end;

theorem Th4: :: BVFUNC13:4

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (Ex ('not' a),A,G),B,G '<' 'not' (All (All a,B,G),A,G)

proof end;

theorem :: BVFUNC13:5

canceled;

theorem :: BVFUNC13:6

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (All ('not' a),A,G),B,G '<' 'not' (All (All a,B,G),A,G)

proof end;

theorem Th7: :: BVFUNC13:7

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ('not' (Ex a,A,G)),B,G '<' 'not' (All (All a,B,G),A,G)

proof end;

theorem :: BVFUNC13:8

canceled;

theorem :: BVFUNC13:9

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All (Ex a,A,G),B,G) '<' 'not' (Ex (All a,B,G),A,G) by PARTIT_2:11, PARTIT_2:19;

theorem Th10: :: BVFUNC13:10

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex (Ex a,A,G),B,G) '<' 'not' (Ex (All a,B,G),A,G)

proof end;

theorem Th11: :: BVFUNC13:11

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (Ex a,B,G),A,G)

proof end;

theorem :: BVFUNC13:12

canceled;

theorem :: BVFUNC13:13

canceled;

theorem :: BVFUNC13:14

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex (All a,A,G),B,G) '<' 'not' (All (All a,B,G),A,G)

proof end;

theorem :: BVFUNC13:15

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All (Ex a,A,G),B,G) '<' 'not' (All (All a,B,G),A,G)

proof end;

theorem :: BVFUNC13:16

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (All a,B,G),A,G)

proof end;

theorem Th17: :: BVFUNC13:17

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex (All a,A,G),B,G) '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem Th18: :: BVFUNC13:18

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All (Ex a,A,G),B,G) '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem Th19: :: BVFUNC13:19

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex (Ex a,A,G),B,G) '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem Th20: :: BVFUNC13:20

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All (Ex a,A,G),B,G) '<' All ('not' (All a,B,G)),A,G

proof end;

theorem Th21: :: BVFUNC13:21

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex (Ex a,A,G),B,G) '<' All ('not' (All a,B,G)),A,G

proof end;

theorem Th22: :: BVFUNC13:22

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex (Ex a,A,G),B,G) '<' Ex ('not' (Ex a,B,G)),A,G

proof end;

theorem Th23: :: BVFUNC13:23

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex (Ex a,A,G),B,G) = All ('not' (Ex a,B,G)),A,G

proof end;

theorem Th24: :: BVFUNC13:24

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All (Ex a,A,G),B,G) '<' Ex (Ex ('not' a),B,G),A,G

proof end;

theorem Th25: :: BVFUNC13:25

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex (Ex a,A,G),B,G) '<' Ex (Ex ('not' a),B,G),A,G

proof end;

theorem Th26: :: BVFUNC13:26

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All (Ex a,A,G),B,G) '<' All (Ex ('not' a),B,G),A,G

proof end;

theorem Th27: :: BVFUNC13:27

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex (Ex a,A,G),B,G) '<' All (Ex ('not' a),B,G),A,G

proof end;

theorem Th28: :: BVFUNC13:28

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex (Ex a,A,G),B,G) '<' Ex (All ('not' a),B,G),A,G

proof end;

theorem Th29: :: BVFUNC13:29

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex (Ex a,A,G),B,G) = All (All ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC13:30

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ('not' (Ex a,A,G)),B,G '<' 'not' (Ex (All a,B,G),A,G)

proof end;

theorem :: BVFUNC13:31

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ('not' (Ex a,A,G)),B,G '<' 'not' (Ex (All a,B,G),A,G)

proof end;

theorem :: BVFUNC13:32

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ('not' (Ex a,A,G)),B,G '<' 'not' (All (Ex a,B,G),A,G)

proof end;

theorem :: BVFUNC13:33

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ('not' (Ex a,A,G)),B,G = 'not' (Ex (Ex a,B,G),A,G)

proof end;

theorem :: BVFUNC13:34

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ('not' (All a,A,G)),B,G = Ex ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:35

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ('not' (All a,A,G)),B,G '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:36

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ('not' (Ex a,A,G)),B,G '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:37

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ('not' (Ex a,A,G)),B,G '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:38

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ('not' (Ex a,A,G)),B,G '<' All ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:39

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ('not' (Ex a,A,G)),B,G '<' All ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:40

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ('not' (Ex a,A,G)),B,G '<' Ex ('not' (Ex a,B,G)),A,G

proof end;

theorem :: BVFUNC13:41

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ('not' (Ex a,A,G)),B,G = All ('not' (Ex a,B,G)),A,G

proof end;

theorem :: BVFUNC13:42

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ('not' (Ex a,A,G)),B,G '<' Ex (Ex ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC13:43

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ('not' (Ex a,A,G)),B,G '<' Ex (Ex ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC13:44

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ('not' (Ex a,A,G)),B,G '<' All (Ex ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC13:45

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ('not' (Ex a,A,G)),B,G '<' All (Ex ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC13:46

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ('not' (Ex a,A,G)),B,G '<' Ex (All ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC13:47

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ('not' (Ex a,A,G)),B,G = All (All ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC13:48

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (All ('not' a),A,G),B,G '<' 'not' (Ex (All a,B,G),A,G)

proof end;

theorem :: BVFUNC13:49

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (All ('not' a),A,G),B,G '<' 'not' (Ex (All a,B,G),A,G)

proof end;

theorem :: BVFUNC13:50

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (All ('not' a),A,G),B,G '<' 'not' (All (Ex a,B,G),A,G)

proof end;

theorem :: BVFUNC13:51

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (All ('not' a),A,G),B,G '<' 'not' (Ex (Ex a,B,G),A,G)

proof end;

theorem :: BVFUNC13:52

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (Ex ('not' a),A,G),B,G '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:53

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (Ex ('not' a),A,G),B,G '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:54

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (All ('not' a),A,G),B,G '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:55

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (All ('not' a),A,G),B,G '<' Ex ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:56

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (All ('not' a),A,G),B,G '<' All ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:57

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (All ('not' a),A,G),B,G '<' All ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC13:58

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (All ('not' a),A,G),B,G '<' Ex ('not' (Ex a,B,G)),A,G

proof end;

theorem :: BVFUNC13:59

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (All ('not' a),A,G),B,G = All ('not' (Ex a,B,G)),A,G

proof end;

theorem :: BVFUNC13:60

canceled;

theorem :: BVFUNC13:61

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (Ex ('not' a),A,G),B,G '<' Ex (Ex ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC13:62

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (All ('not' a),A,G),B,G '<' Ex (Ex ('not' a),B,G),A,G

proof end;