### Nuprl Lemma : prior-classrel

[T,Info:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].
uiff(v ∈ Prior(X)(e);↓∃e':E. (((last(λe'.0 <#(X es e')) e) (inl e') ∈ (E Top)) ∧ v ∈ X(e')))

Proof

Definitions occuring in Statement :  primed-class: Prior(X) es-local-pred: last(P) classrel: v ∈ X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E lt_int: i <j uiff: uiff(P;Q) uall: [x:A]. B[x] top: Top exists: x:A. B[x] squash: T and: P ∧ Q apply: a lambda: λx.A[x] inl: inl x union: left right natural_number: \$n universe: Type equal: t ∈ T bag-size: #(bs)
Lemmas :  classrel_wf primed-class_wf squash_wf exists_wf top_wf es-local-pred_wf lt_int_wf bag-size_wf subtype_rel_sum sq_exists_wf es-locl_wf assert_wf all_wf not_wf or_wf es-E_wf event-ordering+_subtype nat_wf event-ordering+_wf eclass_wf equal_wf bag-member_wf empty-bag_wf bag-member-empty-iff sq_stable__bag-member

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.  (((last(\mlambda{}e'.0  <z  \#(X  es  e'))  e)  =  (inl  e'))  \mwedge{}  v  \mmember{}  X(e')))

Date html generated: 2015_07_22-PM-00_14_44
Last ObjectModification: 2015_01_28-AM-10_46_22

Home Index