Nuprl Lemma : last-es-hist
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2:E]. last(es-hist(es;e1;e2)) ~ info(e2) supposing e1 ≤loc e2
Proof
Definitions occuring in Statement :
es-hist: es-hist(es;e1;e2),
es-info: info(e),
event-ordering+: EO+(Info),
es-le: e ≤loc e' ,
es-E: E,
last: last(L),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
universe: Type,
sqequal: s ~ t
Lemmas :
last-map,
es-interval_wf,
subtype_rel_list,
top_wf,
es-le_wf,
event-ordering+_subtype,
es-E_wf,
event-ordering+_wf,
es-locl_transitivity2,
es-locl_irreflexivity,
es-locl_wf,
es-interval-nil,
es-le-loc,
equal-wf-T-base,
list_wf,
not_wf,
assert_of_null,
assert_wf,
null_wf3,
es-interval-last
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[e1,e2:E]. last(es-hist(es;e1;e2)) \msim{} info(e2) supposing e1 \mleq{}loc e2
Date html generated:
2015_07_17-PM-00_10_11
Last ObjectModification:
2015_01_28-AM-00_09_00
Home
Index