Nuprl Lemma : rec-combined-loc-class-3_wf

[Info,A,B,C,D:Type]. ∀[F:Id ─→ bag(A) ─→ bag(B) ─→ bag(C) ─→ bag(D) ─→ bag(D)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
[Z:EClass(C)].
  (rec-combined-loc-class-3(F;X;Y;Z) ∈ EClass(D))


Proof




Definitions occuring in Statement :  rec-combined-loc-class-3: rec-combined-loc-class-3(F;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 :  rec-combined-loc-class_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,D:Type].  \mforall{}[F:Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C)  {}\mrightarrow{}  bag(D)  {}\mrightarrow{}  bag(D)].  \mforall{}[X:EClass(A)].
\mforall{}[Y:EClass(B)].  \mforall{}[Z:EClass(C)].
    (rec-combined-loc-class-3(F;X;Y;Z)  \mmember{}  EClass(D))



Date html generated: 2015_07_21-PM-02_55_39
Last ObjectModification: 2015_01_27-PM-07_38_36

Home Index