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)
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