:: BVFUNC_3 semantic presentation
theorem Th1: :: BVFUNC_3:1
theorem Th2: :: BVFUNC_3:2
theorem Th3: :: BVFUNC_3:3
theorem Th4: :: BVFUNC_3:4
for
b1 being non
empty set for
b2 being
Subset of
(PARTITIONS b1) for
b3,
b4 being
Element of
Funcs b1,
BOOLEAN for
b5 being
a_partition of
b1 holds
'not' ((All b3,b5,b2) '&' (All b4,b5,b2)) = (Ex ('not' b3),b5,b2) 'or' (Ex ('not' b4),b5,b2)
theorem Th5: :: BVFUNC_3:5
for
b1 being non
empty set for
b2 being
Subset of
(PARTITIONS b1) for
b3,
b4 being
Element of
Funcs b1,
BOOLEAN for
b5 being
a_partition of
b1 holds
'not' ((Ex b3,b5,b2) '&' (Ex b4,b5,b2)) = (All ('not' b3),b5,b2) 'or' (All ('not' b4),b5,b2)
theorem Th6: :: BVFUNC_3:6
theorem Th7: :: BVFUNC_3:7
theorem Th8: :: BVFUNC_3:8
for
b1 being non
empty set for
b2 being
Subset of
(PARTITIONS b1) for
b3,
b4 being
Element of
Funcs b1,
BOOLEAN for
b5 being
a_partition of
b1 holds
b3 'xor' b4 '<' ('not' ((Ex ('not' b3),b5,b2) 'xor' (Ex b4,b5,b2))) 'or' ('not' ((Ex b3,b5,b2) 'xor' (Ex ('not' b4),b5,b2)))
theorem Th9: :: BVFUNC_3:9
E1:
now
let c1 be non
empty set ;
let c2,
c3 be
Element of
Funcs c1,
BOOLEAN ;
let c4 be
Subset of
(PARTITIONS c1);
let c5 be
a_partition of
c1;
let c6 be
Element of
c1;
assume E2:
Pj (All (c2 'or' c3),c5,c4),
c6 = TRUE
;
assume
ex
b1 being
Element of
c1 st
(
b1 in EqClass c6,
(CompF c5,c4) & not
Pj (c2 'or' c3),
b1 = TRUE )
;
then
Pj (B_INF (c2 'or' c3),(CompF c5,c4)),
c6 = FALSE
by BVFUNC_1:def 19;
then
Pj (All (c2 'or' c3),c5,c4),
c6 = FALSE
by BVFUNC_2:def 9;
hence
contradiction
by E2, MARGREL1:43;
end;
theorem Th10: :: BVFUNC_3:10
theorem Th11: :: BVFUNC_3:11
theorem Th12: :: BVFUNC_3:12
theorem Th13: :: BVFUNC_3:13
E2:
now
let c1 be non
empty set ;
let c2,
c3 be
Element of
Funcs c1,
BOOLEAN ;
let c4 be
Subset of
(PARTITIONS c1);
let c5 be
a_partition of
c1;
let c6 be
Element of
c1;
assume E3:
Pj (All (c2 'imp' c3),c5,c4),
c6 = TRUE
;
assume
ex
b1 being
Element of
c1 st
(
b1 in EqClass c6,
(CompF c5,c4) & not
Pj (c2 'imp' c3),
b1 = TRUE )
;
then
Pj (B_INF (c2 'imp' c3),(CompF c5,c4)),
c6 = FALSE
by BVFUNC_1:def 19;
then
Pj (All (c2 'imp' c3),c5,c4),
c6 = FALSE
by BVFUNC_2:def 9;
hence
contradiction
by E3, MARGREL1:43;
end;
theorem Th14: :: BVFUNC_3:14
theorem Th15: :: BVFUNC_3:15
theorem Th16: :: BVFUNC_3:16
theorem Th17: :: BVFUNC_3:17
theorem Th18: :: BVFUNC_3:18
theorem Th19: :: BVFUNC_3:19
theorem Th20: :: BVFUNC_3:20
theorem Th21: :: BVFUNC_3:21
theorem Th22: :: BVFUNC_3:22
theorem Th23: :: BVFUNC_3:23
theorem Th24: :: BVFUNC_3:24
for
b1 being non
empty set for
b2 being
Subset of
(PARTITIONS b1) for
b3,
b4 being
Element of
Funcs b1,
BOOLEAN for
b5 being
a_partition of
b1 holds
(All b3,b5,b2) 'imp' (All b4,b5,b2) '<' (All b3,b5,b2) 'imp' (Ex b4,b5,b2)
theorem Th25: :: BVFUNC_3:25
for
b1 being non
empty set for
b2 being
Subset of
(PARTITIONS b1) for
b3,
b4 being
Element of
Funcs b1,
BOOLEAN for
b5 being
a_partition of
b1 holds
(Ex b3,b5,b2) 'imp' (Ex b4,b5,b2) '<' (All b3,b5,b2) 'imp' (Ex b4,b5,b2)
theorem Th26: :: BVFUNC_3:26
theorem Th27: :: BVFUNC_3:27
theorem Th28: :: BVFUNC_3:28
theorem Th29: :: BVFUNC_3:29
theorem Th30: :: BVFUNC_3:30
theorem Th31: :: BVFUNC_3:31
theorem Th32: :: BVFUNC_3:32
theorem Th33: :: BVFUNC_3:33
theorem Th34: :: BVFUNC_3:34
theorem Th35: :: BVFUNC_3:35
theorem Th36: :: BVFUNC_3:36
theorem Th37: :: BVFUNC_3:37
theorem Th38: :: BVFUNC_3:38
for
b1 being non
empty set for
b2 being
Subset of
(PARTITIONS b1) for
b3,
b4,
b5 being
Element of
Funcs b1,
BOOLEAN for
b6 being
a_partition of
b1 holds
((Ex b3,b6,b2) '&' (All (b3 'imp' b4),b6,b2)) '&' (All (b3 'imp' b5),b6,b2) '<' Ex (b5 '&' b4),
b6,
b2
theorem Th39: :: BVFUNC_3:39
theorem Th40: :: BVFUNC_3:40
for
b1 being non
empty set for
b2 being
Subset of
(PARTITIONS b1) for
b3,
b4,
b5 being
Element of
Funcs b1,
BOOLEAN for
b6 being
a_partition of
b1 holds
((Ex b3,b6,b2) '&' (All (b3 'imp' b4),b6,b2)) '&' (All (b4 'imp' b5),b6,b2) '<' Ex (b5 '&' b3),
b6,
b2
theorem Th41: :: BVFUNC_3:41
for
b1 being non
empty set for
b2 being
Subset of
(PARTITIONS b1) for
b3,
b4,
b5 being
Element of
Funcs b1,
BOOLEAN for
b6 being
a_partition of
b1 holds
((Ex b3,b6,b2) '&' (All (b4 'imp' ('not' b3)),b6,b2)) '&' (All (b3 'imp' b5),b6,b2) '<' Ex (b5 '&' ('not' b4)),
b6,
b2