Nuprl Lemma : isl-es-search-back
∀es:EO. ∀[T:Type]. ∀e:E. ∀f:{e':E| e' ≤loc e } ─→ (T + Top). (↑isl(es-search-back(es;x.f[x];e)) ⇐⇒ ∃e'≤e.↑isl(f[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,
isl: isl(x),
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
set: {x:A| B[x]} ,
function: x:A ─→ B[x],
union: left + right,
universe: Type
Lemmas :
es-causl-swellfnd,
less_than_transitivity1,
less_than_irreflexivity,
int_seg_wf,
decidable__equal_int,
subtype_rel-int_seg,
false_wf,
le_weakening,
subtract_wf,
int_seg_properties,
le_wf,
nat_wf,
zero-le-nat,
lelt_wf,
es-causl_wf,
es-search-back-cases,
es-le_wf,
subtype_rel_sum,
top_wf,
es-E_wf,
equal_wf,
all_wf,
int_seg_subtype-nat,
iff_wf,
assert_wf,
isl_wf,
es-search-back_wf,
exists_wf,
decidable__lt,
not-equal-2,
condition-implies-le,
minus-add,
minus-minus,
minus-one-mul,
add-swap,
add-commutes,
add-associates,
add_functionality_wrt_le,
zero-add,
le-add-cancel-alt,
less-iff-le,
le-add-cancel,
set_wf,
less_than_wf,
primrec-wf2,
decidable__le,
not-le-2,
sq_stable__le,
add-zero,
add-mul-special,
zero-mul,
event_ordering_wf,
es-le-self,
and_wf,
btrue_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
true_wf,
es-first_wf2,
eqtt_to_assert,
eqff_to_assert,
bool_cases_sqequal,
assert-bnot,
assert-es-first,
es-causl_weakening,
bfalse_wf,
assert_elim,
btrue_neq_bfalse,
es-pred_wf,
es-pred-locl,
subtype_rel_dep_function,
subtype_rel_sets,
es-locl_transitivity1,
es-le_weakening,
subtype_rel_self,
es-le-pred,
es-le_weakening_eq
\mforall{}es:EO
\mforall{}[T:Type]
\mforall{}e:E. \mforall{}f:\{e':E| e' \mleq{}loc e \} {}\mrightarrow{} (T + Top).
(\muparrow{}isl(es-search-back(es;x.f[x];e)) \mLeftarrow{}{}\mRightarrow{} \mexists{}e'\mleq{}e.\muparrow{}isl(f[e']))
Date html generated:
2015_07_17-AM-08_48_47
Last ObjectModification:
2015_01_27-PM-02_28_43
Home
Index