---

{ [Info,A,B,C,D:Type].
    F:bag(A)  bag(B)  bag(C)  bag(D)
      [X:EClass(A)]. [Y:EClass(B)]. [Z:EClass(C)].
        (simple-comb3(x,y,z.F[x;y;z];X;Y;Z)  EClass(D)) }

{ Proof }

---

Definitions occuring in Statement :  simple-comb3: simple-comb3(x,y,z.F[x; y; z];X;Y;Z),  eclass: EClass(A[eo; e]),  uall: [x:A]. B[x],  so_apply: x[s1;s2;s3],  all: x:A. B[x],  member: t  T,  function: x:A  B[x],  universe: Type,  bag: bag(T)
Lemmas :  es-base-E_wf,  es-E_wf,  event-ordering+_wf,  eclass_wf,  event-ordering+_inc,  subtype_rel_self,  bag_wf,  member_wf,  simple-comb_wf,  le_wf,  not_wf,  false_wf,  nat_wf,  int_seg_wf,  select_wf,  length_wf_nat,  length_nil,  length_cons,  non_neg_length,  length_wf1,  top_wf,  subtype_rel_wf,  es-interface-top,  subtype_base_sq,  decidable__equal_int,  int_subtype_base

---

\mforall{}[Info,A,B,C,D:Type].
    \mforall{}F:bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C)  {}\mrightarrow{}  bag(D)
        \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[Z:EClass(C)].
            (simple-comb3(x,y,z.F[x;y;z];X;Y;Z)  \mmember{}  EClass(D))


Date html generated: 2011_08_16-PM-04_57_39
Last ObjectModification: 2011_07_25-AM-10_24_37

Home Index