{ 
[n:
]. [f:Top]. [a:k:n 
bag(Top)].
lifting-gen(n;f) a ~ {} supposing 
k:n. (
bag-null(a k)) }
{ Proof }
Definitions occuring in Statement :
lifting-gen: lifting-gen(n;f),
assert: b,
int_seg: {i..j
},
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
exists: x:A. B[x],
apply: f a,
function: x:A B[x],
natural_number: $n,
sqequal: s ~ t,
bag-null: bag-null(bs),
empty-bag: {},
bag: bag(T)
Lemmas :
equal-empty-bag,
assert-bag-null,
bag-combine-empty-left,
subtype_base_sq,
bag-combine-empty-right,
decidable__equal_int,
member_wf,
eq_int_wf,
bnot_wf,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
assert_of_eq_int,
eqtt_to_assert,
uiff_transitivity,
bool_wf,
bag-null_wf,
not_wf,
false_wf,
uall_wf,
nat_ind_tp,
nat_wf,
le_wf,
assert_wf,
int_seg_wf,
top_wf,
bag_wf,
nat_properties,
ge_wf
\mforall{}[n:\mBbbN{}]. \mforall{}[f:Top]. \mforall{}[a:k:\mBbbN{}n {}\mrightarrow{} bag(Top)]. lifting-gen(n;f) a \msim{} \{\} supposing \mexists{}k:\mBbbN{}n. (\muparrow{}bag-null(a k))
Date html generated:
2011_08_17-PM-05_59_04
Last ObjectModification:
2011_06_28-PM-12_53_53
Home
Index