---

{ [f:Top]. [b:bag(Top)]. [i:Top].
    ((f@Loc i {} b ~ {})  (f@Loc i b {} ~ {})) }

{ Proof }

---

Definitions occuring in Statement :  concat-lifting-loc-2: f@Loc,  uall: [x:A]. B[x],  top: Top,  and: P  Q,  apply: f a,  sqequal: s ~ t,  empty-bag: {},  bag: bag(T)
Lemmas :  concat-lifting-2-strict,  top_wf,  bag_wf

---

\mforall{}[f:Top].  \mforall{}[b:bag(Top)].  \mforall{}[i:Top].    ((f@Loc  i  \{\}  b  \msim{}  \{\})  \mwedge{}  (f@Loc  i  b  \{\}  \msim{}  \{\}))


Date html generated: 2011_08_17-PM-06_15_38
Last ObjectModification: 2011_06_28-PM-03_55_08

Home Index