Nuprl Lemma : can-apply-es-search-back

es:EO
  ∀[T:Type]
    ∀e:E. ∀f:{e':E| e' ≤loc }  ⟶ (T Top).
      (↑can-apply(λe.es-search-back(es;x.f[x];e);e) ⇐⇒ ∃e'≤e.↑can-apply(λx.f[x];e'))


Proof




Definitions occuring in Statement :  existse-le: e≤e'.P[e] es-search-back: es-search-back(es;x.f[x];e) es-le: e ≤loc e'  es-E: E event_ordering: EO assert: b uall: [x:A]. B[x] top: Top so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q set: {x:A| B[x]}  lambda: λx.A[x] function: x:A ⟶ B[x] union: left right universe: Type can-apply: can-apply(f;x)
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] can-apply: can-apply(f;x) member: t ∈ T

Latex:
\mforall{}es:EO
    \mforall{}[T:Type]
        \mforall{}e:E.  \mforall{}f:\{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  (T  +  Top).
            (\muparrow{}can-apply(\mlambda{}e.es-search-back(es;x.f[x];e);e)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e'\mleq{}e.\muparrow{}can-apply(\mlambda{}x.f[x];e'))



Date html generated: 2016_05_16-AM-09_46_53
Last ObjectModification: 2015_12_28-PM-09_37_30

Theory : new!event-ordering


Home Index