Nuprl Lemma : iseg-es-embedding
∀[Info:Type]. ∀L1,L2:(Id × Info) List. (L1 ≤ L2 ⇒ (λx.x embeds global-eo(L1) into global-eo(L2)))
Proof
Definitions occuring in Statement :
global-eo: global-eo(L),
es-embedding: (f embeds eo1 into eo2),
Id: Id,
iseg: l1 ≤ l2,
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
lambda: λx.A[x],
product: x:A × B[x],
universe: Type
Lemmas :
iseg_length,
es-causl_wf,
global-eo_wf,
event-ordering+_subtype,
es-E_wf,
iseg_wf,
Id_wf,
list_wf,
map_wf,
es-loc_wf,
es-info_wf,
es-le-before_wf,
iseg-global-order-history,
listp_wf,
iff_weakening_equal,
iseg-global-order-loc,
global-eo-causl,
global-eo-E-sq,
subtype_rel_list,
top_wf,
less_than_transitivity1,
length_wf,
lelt_wf,
true_wf
Latex:
\mforall{}[Info:Type]. \mforall{}L1,L2:(Id \mtimes{} Info) List. (L1 \mleq{} L2 {}\mRightarrow{} (\mlambda{}x.x embeds global-eo(L1) into global-eo(L2)))
Date html generated:
2015_07_21-PM-04_38_12
Last ObjectModification:
2015_02_04-PM-05_57_04
Home
Index