Nuprl Lemma : list2extended-eo
∀[Info:Type]
∀L:Info List+. ∀i:Id. ∃es:EO+(Info). ∃e:E. ((loc(e) = i ∈ Id) ∧ (L = map(λe.info(e);≤loc(e)) ∈ (Info List)))
Proof
Definitions occuring in Statement :
es-info: info(e),
event-ordering+: EO+(Info),
es-le-before: ≤loc(e),
es-loc: loc(e),
es-E: E,
Id: Id,
listp: A List+,
map: map(f;as),
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
lambda: λx.A[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
list-eo_wf,
list-eo-property,
list-eo-loc,
es-loc_wf,
event-ordering+_subtype,
list_wf,
map_wf,
es-E_wf,
es-info_wf,
es-le-before_wf,
exists_wf,
Id_wf,
listp_wf
Latex:
\mforall{}[Info:Type]
\mforall{}L:Info List\msupplus{}. \mforall{}i:Id. \mexists{}es:EO+(Info). \mexists{}e:E. ((loc(e) = i) \mwedge{} (L = map(\mlambda{}e.info(e);\mleq{}loc(e))))
Date html generated:
2015_07_21-PM-04_32_19
Last ObjectModification:
2015_01_27-PM-05_07_55
Home
Index