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
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
listp: A List+,
subtype_rel: A ⊆r B,
prop: ℙ,
top: Top,
cand: A c∧ B,
and: P ∧ Q,
member: t ∈ T,
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x]
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:
2016_05_17-AM-08_25_05
Last ObjectModification:
2015_12_28-PM-10_59_08
Theory : event-ordering
Home
Index