begin
:: deftheorem BVFUNC_1:def 1 :
canceled;
:: deftheorem BVFUNC_1:def 2 :
canceled;
:: deftheorem Def3 defines <= BVFUNC_1:def 3 :
begin
:: deftheorem BVFUNC_1:def 4 :
canceled;
:: deftheorem Def5 defines 'or' BVFUNC_1:def 5 :
:: deftheorem Def6 defines 'xor' BVFUNC_1:def 6 :
:: deftheorem Def7 defines 'or' BVFUNC_1:def 7 :
:: deftheorem defines 'xor' BVFUNC_1:def 8 :
:: deftheorem Def9 defines 'imp' BVFUNC_1:def 9 :
:: deftheorem Def10 defines 'eqv' BVFUNC_1:def 10 :
:: deftheorem Def11 defines 'imp' BVFUNC_1:def 11 :
:: deftheorem Def12 defines 'eqv' BVFUNC_1:def 12 :
:: deftheorem Def13 defines O_el BVFUNC_1:def 13 :
:: deftheorem Def14 defines I_el BVFUNC_1:def 14 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th5:
theorem
theorem
theorem Th8:
theorem Th9:
theorem
theorem
theorem Th12:
theorem Th13:
theorem
theorem
theorem
theorem
:: deftheorem Def15 defines '<' BVFUNC_1:def 15 :
theorem
theorem Th19:
theorem
theorem
begin
definition
let Y be non
empty set ;
let a be
Element of
Funcs Y,
BOOLEAN ;
func B_INF a -> Element of
Funcs Y,
BOOLEAN means :
Def16:
it = I_el Y if for
x being
Element of
Y holds
a . x = TRUE otherwise it = O_el Y;
correctness
consistency
for b1 being Element of Funcs Y,BOOLEAN holds verum;
existence
( ( for b1 being Element of Funcs Y,BOOLEAN holds verum ) & ( ( for x being Element of Y holds a . x = TRUE ) implies ex b1 being Element of Funcs Y,BOOLEAN st b1 = I_el Y ) & ( not for x being Element of Y holds a . x = TRUE implies ex b1 being Element of Funcs Y,BOOLEAN st b1 = O_el Y ) );
uniqueness
for b1, b2 being Element of Funcs Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = TRUE ) & b1 = I_el Y & b2 = I_el Y implies b1 = b2 ) & ( not for x being Element of Y holds a . x = TRUE & b1 = O_el Y & b2 = O_el Y implies b1 = b2 ) );
;
func B_SUP a -> Element of
Funcs Y,
BOOLEAN means :
Def17:
it = O_el Y if for
x being
Element of
Y holds
a . x = FALSE otherwise it = I_el Y;
correctness
consistency
for b1 being Element of Funcs Y,BOOLEAN holds verum;
existence
( ( for b1 being Element of Funcs Y,BOOLEAN holds verum ) & ( ( for x being Element of Y holds a . x = FALSE ) implies ex b1 being Element of Funcs Y,BOOLEAN st b1 = O_el Y ) & ( not for x being Element of Y holds a . x = FALSE implies ex b1 being Element of Funcs Y,BOOLEAN st b1 = I_el Y ) );
uniqueness
for b1, b2 being Element of Funcs Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = FALSE ) & b1 = O_el Y & b2 = O_el Y implies b1 = b2 ) & ( not for x being Element of Y holds a . x = FALSE & b1 = I_el Y & b2 = I_el Y implies b1 = b2 ) );
;
end;
:: deftheorem Def16 defines B_INF BVFUNC_1:def 16 :
:: deftheorem Def17 defines B_SUP BVFUNC_1:def 17 :
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def18 defines is_dependent_of BVFUNC_1:def 18 :
theorem
theorem
definition
let Y be non
empty set ;
let a be
Element of
Funcs Y,
BOOLEAN ;
let PA be
a_partition of
Y;
func B_INF a,
PA -> Element of
Funcs Y,
BOOLEAN means :
Def19:
for
y being
Element of
Y holds
( ( ( for
x being
Element of
Y st
x in EqClass y,
PA holds
a . x = TRUE ) implies
it . y = TRUE ) & ( ex
x being
Element of
Y st
(
x in EqClass y,
PA & not
a . x = TRUE ) implies
it . y = FALSE ) );
existence
ex b1 being Element of Funcs Y,BOOLEAN st
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies b1 . y = FALSE ) )
uniqueness
for b1, b2 being Element of Funcs Y,BOOLEAN st ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies b2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
end;
:: deftheorem Def19 defines B_INF BVFUNC_1:def 19 :
definition
let Y be non
empty set ;
let a be
Element of
Funcs Y,
BOOLEAN ;
let PA be
a_partition of
Y;
func B_SUP a,
PA -> Element of
Funcs Y,
BOOLEAN means :
Def20:
for
y being
Element of
Y holds
( ( ex
x being
Element of
Y st
(
x in EqClass y,
PA &
a . x = TRUE ) implies
it . y = TRUE ) & ( ( for
x being
Element of
Y holds
( not
x in EqClass y,
PA or not
a . x = TRUE ) ) implies
it . y = FALSE ) );
existence
ex b1 being Element of Funcs Y,BOOLEAN st
for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies b1 . y = FALSE ) )
uniqueness
for b1, b2 being Element of Funcs Y,BOOLEAN st ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies b2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
end;
:: deftheorem Def20 defines B_SUP BVFUNC_1:def 20 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines GPart BVFUNC_1:def 21 :
theorem
theorem