Nuprl Lemma : simple-loc-comb2_wf

[Info,A,B,C:Type]. ∀[F:Id ─→ bag(A) ─→ bag(B) ─→ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (simple-loc-comb2(l,a,b.F[l;a;b];X;Y) ∈ EClass(C))


Proof




Definitions occuring in Statement :  simple-loc-comb2: simple-loc-comb2(l,a,b.F[l; a; b];X;Y) eclass: EClass(A[eo; e]) Id: Id uall: [x:A]. B[x] so_apply: x[s1;s2;s3] member: t ∈ T function: x:A ─→ B[x] universe: Type bag: bag(T)
Lemmas :  simple-loc-comb_wf select_wf cons_wf nil_wf length_wf length_nil non_neg_length length_wf_nil length_cons length_wf_nat int_seg_wf decidable__equal_int subtype_base_sq int_subtype_base es-interface-subtype_rel2 es-E_wf event-ordering+_subtype bag_wf false_wf eclass_wf event-ordering+_wf Id_wf

Latex:
\mforall{}[Info,A,B,C:Type].  \mforall{}[F:Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C)].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    (simple-loc-comb2(l,a,b.F[l;a;b];X;Y)  \mmember{}  EClass(C))



Date html generated: 2015_07_21-PM-02_57_15
Last ObjectModification: 2015_01_27-PM-07_32_54

Home Index