Nuprl Lemma : simple-loc-comb-2-loc-bounded2

[Info,A,B,C:Type]. ∀[f:Id ─→ A ─→ B ─→ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (LocBounded(A;X)  LocBounded(C;lifting-loc-2(f) (Loc,X, Y)))


Proof




Definitions occuring in Statement :  lifting-loc-2: lifting-loc-2(f) simple-loc-comb-2: (Loc,X, Y) loc-bounded-class: LocBounded(T;X) eclass: EClass(A[eo; e]) Id: Id uall: [x:A]. B[x] implies:  Q function: x:A ─→ B[x] universe: Type
Lemmas :  simple-loc-comb-2-classrel sq_stable__bag-member es-loc_wf classrel_wf simple-loc-comb-2_wf lifting-loc-2_wf es-E_wf event-ordering+_subtype all_wf bag-member_wf loc-bounded-class_wf eclass_wf event-ordering+_wf Id_wf

Latex:
\mforall{}[Info,A,B,C:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    (LocBounded(A;X)  {}\mRightarrow{}  LocBounded(C;lifting-loc-2(f)  o  (Loc,X,  Y)))



Date html generated: 2015_07_22-PM-00_09_07
Last ObjectModification: 2015_01_28-AM-11_41_19

Home Index