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

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

Proof

Definitions occuring in Statement :  lifting-loc-2: `lifting-loc-2(f)` simple-loc-comb-2: `F o (Loc,X, Y)` loc-bounded-class: `LocBounded(T;X)` eclass: `EClass(A[eo; e])` Id: `Id` uall: `∀[x:A]. B[x]` implies: `P `` Q` or: `P ∨ 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 or_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)  \mvee{}  LocBounded(B;Y))  {}\mRightarrow{}  LocBounded(C;lifting-loc-2(f)  o  (Loc,X,  Y)))

Date html generated: 2015_07_22-PM-00_09_06
Last ObjectModification: 2015_01_28-AM-11_41_30

Home Index