{ [Info,A,B,C,D,E:Type]. [F:Id
                               bag(A)
                               bag(B)
                               bag(C)
                               bag(D)
                               bag(E)]. [W:EClass(A)]. [X:EClass(B)].
  [Y:EClass(C)]. [Z:EClass(D)].
    (simple-loc-comb-4(F;W;X;Y;Z)  EClass(E)) }

{ Proof }



Definitions occuring in Statement :  simple-loc-comb-4: simple-loc-comb-4(F;W;X;Y;Z) 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 :  int_seg_properties decidable__equal_int int_subtype_base es-E_wf event-ordering+_wf eclass_wf event-ordering+_inc Id_wf bag_wf member_wf simple-loc-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

\mforall{}[Info,A,B,C,D,E:Type].  \mforall{}[F:Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C)  {}\mrightarrow{}  bag(D)  {}\mrightarrow{}  bag(E)].  \mforall{}[W:EClass(A)].
\mforall{}[X:EClass(B)].  \mforall{}[Y:EClass(C)].  \mforall{}[Z:EClass(D)].
    (simple-loc-comb-4(F;W;X;Y;Z)  \mmember{}  EClass(E))


Date html generated: 2011_08_16-PM-05_00_57
Last ObjectModification: 2011_07_24-PM-11_46_17

Home Index