{ 
[f:Top]. [b:bag(Top)]. ((f@ {} b ~ {}) 
(f@ b {} ~ {})) }
{ Proof }
Definitions occuring in Statement :
concat-lifting-2: f@,
uall: [x:A]. B[x],
top: Top,
and: P Q,
apply: f a,
sqequal: s ~ t,
empty-bag: {},
bag: bag(T)
Lemmas :
true_wf,
null_wf,
ifthenelse_wf,
bag-subtype-list,
subtype_rel_wf,
permutation_wf,
null_wf3,
lifting-gen-strict,
select_wf,
empty-bag_wf,
top_wf,
bag_wf,
int_seg_wf,
assert_wf,
nat_wf,
member_wf,
le_wf,
not_wf,
false_wf
\mforall{}[f:Top]. \mforall{}[b:bag(Top)]. ((f@ \{\} b \msim{} \{\}) \mwedge{} (f@ b \{\} \msim{} \{\}))
Date html generated:
2011_08_17-PM-06_11_06
Last ObjectModification:
2011_06_28-PM-03_45_46
Home
Index