{ 
[f,i:Top]. [b,b':bag(Top)].
((concat-lifting-loc-3(f) i {} b b' ~ {})
(concat-lifting-loc-3(f) i b {} b' ~ {})
(concat-lifting-loc-3(f) i b b' {} ~ {})) }
{ Proof }
Definitions occuring in Statement :
concat-lifting-loc-3: concat-lifting-loc-3(f),
uall: [x:A]. B[x],
top: Top,
and: P Q,
apply: f a,
sqequal: s ~ t,
empty-bag: {},
bag: bag(T)
Lemmas :
concat-lifting-3-strict,
top_wf,
bag_wf
\mforall{}[f,i:Top]. \mforall{}[b,b':bag(Top)].
((concat-lifting-loc-3(f) i \{\} b b' \msim{} \{\})
\mwedge{} (concat-lifting-loc-3(f) i b \{\} b' \msim{} \{\})
\mwedge{} (concat-lifting-loc-3(f) i b b' \{\} \msim{} \{\}))
Date html generated:
2011_08_17-PM-06_16_14
Last ObjectModification:
2011_06_28-PM-03_57_13
Home
Index