### Nuprl Lemma : prior-classrel-p-local-pred

`∀[T,Info:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].`
`  uiff(v ∈ Prior(X)(e);↓∃e':E. ((es-p-local-pred(es;λe'.(↓∃w:T. w ∈ X(e'))) e e') ∧ v ∈ X(e')))`

Proof

Definitions occuring in Statement :  primed-class: `Prior(X)` classrel: `v ∈ X(e)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-p-local-pred: `es-p-local-pred(es;P)` es-E: `E` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` squash: `↓T` and: `P ∧ Q` apply: `f a` lambda: `λx.A[x]` universe: `Type`
Lemmas :  prior-classrel es-p-local-pred_wf event-ordering+_subtype squash_wf exists_wf classrel_wf es-E_wf primed-class_wf top_wf es-local-pred_wf lt_int_wf bag-size_wf subtype_rel_sum sq_exists_wf es-locl_wf assert_wf nat_wf all_wf not_wf or_wf es-local-pred-iff-es-p-local-pred

Latex:
\mforall{}[T,Info:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].
uiff(v  \mmember{}  Prior(X)(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')))

Date html generated: 2015_07_22-PM-00_14_54
Last ObjectModification: 2015_01_28-AM-10_46_32

Home Index