### Nuprl Lemma : primed-class-opt-classrel

`∀[T,Info:Type]. ∀[X:EClass(T)]. ∀[init:Id ─→ bag(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].`
`  uiff(v ∈ Prior(X)?init(e);↓(∃e':E. ((es-p-local-pred(es;λe'.(↓∃w:T. w ∈ X(e'))) e e') ∧ v ∈ X(e')))`
`                             ∨ ((∀e':E. ((e' <loc e) `` (∀w:T. (¬w ∈ X(e'))))) ∧ v ↓∈ init loc(e)))`

Proof

Definitions occuring in Statement :  primed-class-opt: `Prior(X)?b` classrel: `v ∈ X(e)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-p-local-pred: `es-p-local-pred(es;P)` es-locl: `(e <loc e')` es-loc: `loc(e)` es-E: `E` Id: `Id` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` squash: `↓T` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ─→ B[x]` universe: `Type` bag-member: `x ↓∈ bs` bag: `bag(T)`
Lemmas :  bag-member_wf squash_wf or_wf exists_wf es-E_wf event-ordering+_subtype es-p-local-pred_wf all_wf es-locl_wf not_wf es-loc_wf assert_of_lt_int bag-size_wf nat_wf assert_wf bag-member-iff-size sq_stable__bag-member true_wf bag_wf es-locl-trichotomy empty-bag-iff-no-member lt_int_wf length_of_nil_lemma

Latex:
\mforall{}[T,Info:Type].  \mforall{}[X:EClass(T)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].
uiff(v  \mmember{}  Prior(X)?init(
e);\mdownarrow{}(\mexists{}e':E.  ((es-p-local-pred(es;\mlambda{}e'.(\mdownarrow{}\mexists{}w:T.  w  \mmember{}  X(e')))  e  e')  \mwedge{}  v  \mmember{}  X(e')))
\mvee{}  ((\mforall{}e':E.  ((e'  <loc  e)  {}\mRightarrow{}  (\mforall{}w:T.  (\mneg{}w  \mmember{}  X(e')))))  \mwedge{}  v  \mdownarrow{}\mmember{}  init  loc(e)))

Date html generated: 2015_07_21-PM-02_31_23
Last ObjectModification: 2015_01_27-PM-09_57_52

Home Index