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

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


Proof




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



Date html generated: 2015_07_21-PM-02_57_03
Last ObjectModification: 2015_01_27-PM-07_29_03

Home Index