---

{ [Info,A,B:Type]. [F:Id  bag(A)  bag(B)  bag(B)]. [X:EClass(A)].
  [init:Id  bag(B)].
    (F|Loc, X, Prior(self)?init|  EClass(B)) }

{ Proof }

---

Definitions occuring in Statement :  rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init|,  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  universe: Type,  bag: bag(T)
Lemmas :  eclass_wf,  length_cons,  length_nil,  length_wf_nat,  select_wf,  int_seg_wf,  le_wf,  member_wf,  nat_wf,  false_wf,  not_wf,  Error :rec-comb_wf,  bag_wf,  Id_wf,  event-ordering+_wf,  event-ordering+_inc,  es-E_wf,  non_neg_length,  length_wf1,  top_wf

---

\mforall{}[Info,A,B:Type].  \mforall{}[F:Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    (F|Loc,  X,  Prior(self)?init|  \mmember{}  EClass(B))


Date html generated: 2011_08_16-PM-04_55_00
Last ObjectModification: 2011_07_22-PM-10_23_48

Home Index