---

{ [Info,A,B,C:Type]. [f:Id  A  B  bag(C)]. [X:EClass(A)].
  [Y:EClass(B)].
    (LocBounded(B;Y)  LocBounded(C;f@Loc|Loc,X, Y|)) }

{ Proof }

---

Definitions occuring in Statement :  concat-lifting-loc-2: f@Loc,  simple-loc-comb-2: F|Loc,X, Y|,  loc-bounded-class: LocBounded(T;X),  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  implies: P  Q,  function: x:A  B[x],  universe: Type,  bag: bag(T)
Lemmas :  es-loc_wf,  bag-member_wf,  Id_wf,  concat-lifting-loc-2_wf,  simple-loc-comb-2_wf,  classrel_wf,  event-ordering+_inc,  es-E_wf,  event-ordering+_wf,  sq_stable__bag-member,  simple-loc-comb-2-concat-classrel,  bag_wf,  eclass_wf,  loc-bounded-class_wf

---

\mforall{}[Info,A,B,C:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    (LocBounded(B;Y)  {}\mRightarrow{}  LocBounded(C;f@Loc|Loc,X,  Y|))


Date html generated: 2011_08_17-PM-06_21_55
Last ObjectModification: 2011_07_14-PM-09_02_07

Home Index