Nuprl Lemma : can-apply-es-search-back
∀es:EO
∀[T:Type]
∀e:E. ∀f:{e':E| e' ≤loc e } ─→ (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: P ⇐⇒ 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)
Lemmas :
isl-es-search-back,
event_ordering_wf
\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:
2015_07_17-AM-08_48_51
Last ObjectModification:
2015_01_27-PM-02_24_35
Home
Index