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

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

Proof

Definitions occuring in Statement :  concat-lifting-loc-2: `f@Loc` 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` bag: `bag(T)`
Lemmas :  simple-loc-comb-2-concat-classrel sq_stable__bag-member es-loc_wf classrel_wf simple-loc-comb-2_wf concat-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 bag_wf

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

Date html generated: 2015_07_22-PM-00_11_06
Last ObjectModification: 2015_01_28-AM-11_40_36

Home Index