### Nuprl Lemma : return-loc-bag-class-classrel

`∀[Info,A:Type]. ∀[x:Id ─→ bag(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A].`
`  (v ∈ return-loc-bag-class(x)(e) `⇐⇒` v ↓∈ x loc(e) ∧ (↑first(e)))`

Proof

Definitions occuring in Statement :  return-loc-bag-class: `return-loc-bag-class(x)` classrel: `v ∈ X(e)` event-ordering+: `EO+(Info)` es-first: `first(e)` es-loc: `loc(e)` es-E: `E` Id: `Id` assert: `↑b` uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` bag-member: `x ↓∈ bs` bag: `bag(T)`
Lemmas :  es-first_wf2 bool_wf eqtt_to_assert bag-member_wf es-loc_wf true_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot bag-member-empty-iff event-ordering+_subtype classrel_wf return-loc-bag-class_wf assert_wf es-E_wf event-ordering+_wf Id_wf bag_wf

Latex:
\mforall{}[Info,A:Type].  \mforall{}[x:Id  {}\mrightarrow{}  bag(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:A].
(v  \mmember{}  return-loc-bag-class(x)(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mdownarrow{}\mmember{}  x  loc(e)  \mwedge{}  (\muparrow{}first(e)))

Date html generated: 2015_07_22-PM-00_06_25
Last ObjectModification: 2015_01_28-AM-11_42_47

Home Index