:: Predicate Calculus for Boolean Valued Functions, { I }
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received December 21, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: BVFUNC_3:1
theorem :: BVFUNC_3:2
theorem :: BVFUNC_3:3
theorem :: BVFUNC_3:4
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
'not' ((All a,PA,G) '&' (All b,PA,G)) = (Ex ('not' a),PA,G) 'or' (Ex ('not' b),PA,G)
theorem :: BVFUNC_3:5
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
'not' ((Ex a,PA,G) '&' (Ex b,PA,G)) = (All ('not' a),PA,G) 'or' (All ('not' b),PA,G)
theorem :: BVFUNC_3:6
theorem :: BVFUNC_3:7
theorem :: BVFUNC_3:8
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
a 'xor' b '<' ('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))
theorem :: BVFUNC_3:9
Lm1:
now
let Y be non
empty set ;
:: thesis: for a, b being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All (a 'or' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE let a,
b be
Element of
Funcs Y,
BOOLEAN ;
:: thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All (a 'or' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE let G be
Subset of
(PARTITIONS Y);
:: thesis: for PA being a_partition of Y
for z being Element of Y st (All (a 'or' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE let PA be
a_partition of
Y;
:: thesis: for z being Element of Y st (All (a 'or' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE let z be
Element of
Y;
:: thesis: ( (All (a 'or' b),PA,G) . z = TRUE implies for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE )assume A1:
(All (a 'or' b),PA,G) . z = TRUE
;
:: thesis: for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE assume
ex
x being
Element of
Y st
(
x in EqClass z,
(CompF PA,G) & not
(a 'or' b) . x = TRUE )
;
:: thesis: contradictionthen
(B_INF (a 'or' b),(CompF PA,G)) . z = FALSE
by BVFUNC_1:def 19;
hence
contradiction
by A1, BVFUNC_2:def 9;
:: thesis: verum
end;
theorem :: BVFUNC_3:10
theorem :: BVFUNC_3:11
theorem :: BVFUNC_3:12
theorem :: BVFUNC_3:13
Lm2:
now
let Y be non
empty set ;
:: thesis: for a, b being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All (a 'imp' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE let a,
b be
Element of
Funcs Y,
BOOLEAN ;
:: thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All (a 'imp' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE let G be
Subset of
(PARTITIONS Y);
:: thesis: for PA being a_partition of Y
for z being Element of Y st (All (a 'imp' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE let PA be
a_partition of
Y;
:: thesis: for z being Element of Y st (All (a 'imp' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE let z be
Element of
Y;
:: thesis: ( (All (a 'imp' b),PA,G) . z = TRUE implies for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE )assume A1:
(All (a 'imp' b),PA,G) . z = TRUE
;
:: thesis: for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE assume
ex
x being
Element of
Y st
(
x in EqClass z,
(CompF PA,G) & not
(a 'imp' b) . x = TRUE )
;
:: thesis: contradictionthen
(B_INF (a 'imp' b),(CompF PA,G)) . z = FALSE
by BVFUNC_1:def 19;
hence
contradiction
by A1, BVFUNC_2:def 9;
:: thesis: verum
end;
theorem :: BVFUNC_3:14
theorem :: BVFUNC_3:15
theorem :: BVFUNC_3:16
theorem :: BVFUNC_3:17
theorem :: BVFUNC_3:18
theorem :: BVFUNC_3:19
theorem :: BVFUNC_3:20
theorem :: BVFUNC_3:21
theorem :: BVFUNC_3:22
theorem :: BVFUNC_3:23
theorem :: BVFUNC_3:24
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
(All a,PA,G) 'imp' (All b,PA,G) '<' (All a,PA,G) 'imp' (Ex b,PA,G)
theorem :: BVFUNC_3:25
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
(Ex a,PA,G) 'imp' (Ex b,PA,G) '<' (All a,PA,G) 'imp' (Ex b,PA,G)
theorem Th26: :: BVFUNC_3:26
theorem :: BVFUNC_3:27
theorem :: BVFUNC_3:28
theorem :: BVFUNC_3:29
theorem :: BVFUNC_3:30
theorem :: BVFUNC_3:31
theorem :: BVFUNC_3:32
theorem :: BVFUNC_3:33
theorem :: BVFUNC_3:34
theorem :: BVFUNC_3:35
theorem :: BVFUNC_3:36
theorem :: BVFUNC_3:37
theorem :: BVFUNC_3:38
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
c,
b,
a being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
((Ex c,PA,G) '&' (All (c 'imp' b),PA,G)) '&' (All (c 'imp' a),PA,G) '<' Ex (a '&' b),
PA,
G
theorem :: BVFUNC_3:39
theorem :: BVFUNC_3:40
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
b,
c,
a being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
((Ex b,PA,G) '&' (All (b 'imp' c),PA,G)) '&' (All (c 'imp' a),PA,G) '<' Ex (a '&' b),
PA,
G
theorem :: BVFUNC_3:41
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
c,
b,
a being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
((Ex c,PA,G) '&' (All (b 'imp' ('not' c)),PA,G)) '&' (All (c 'imp' a),PA,G) '<' Ex (a '&' ('not' b)),
PA,
G