Nuprl Lemma : global-order-compat-joint-embedding
∀[Info:Type]
∀L1,L2:(Id × Info) List.
(L1 || L2
⇒ (∃L:(Id × Info) List
((∃f:E ─→ E. ∃g:E ─→ E. es-weak-joint-embedding(Info;global-eo(L1);global-eo(L2);global-eo(L);f;g))
∧ (∀L':(Id × Info) List. (L1 || L' ⇒ L2 || L' ⇒ L || L')))))
Proof
Definitions occuring in Statement :
global-order-compat: L1 || L2,
global-eo: global-eo(L),
es-weak-joint-embedding: es-weak-joint-embedding(Info;eo1;eo2;eo;f;g),
es-E: E,
Id: Id,
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ─→ B[x],
product: x:A × B[x],
universe: Type
Lemmas :
iseg_length,
Id_wf,
global-eo-E-sq,
true_wf,
int_seg_wf,
length_wf,
less_than_transitivity1,
lelt_wf,
subtype_rel_dep_function,
set_wf,
es-weak-joint-embedding_wf,
global-eo_wf,
exists_wf,
es-E_wf,
event-ordering+_subtype,
global-eo-loc,
pi1_wf_top,
squash_wf,
top_wf,
subtype_rel_product,
iff_weakening_equal,
global-eo-info-le-before,
subtype_rel_list,
subtype_base_sq,
atom2_subtype_base,
filter_wf5,
firstn_wf,
l_member_wf,
eq_id_wf,
list_wf,
map_wf,
equal_wf,
subtype_rel_sets,
subtype_rel_set,
subtype_rel-int_seg,
false_wf,
global-eo-causl,
es-causl_wf,
less_than_wf,
or_wf,
zero-le-nat,
nat_wf,
int_seg_subtype-nat,
length_wf_nat,
compat_wf
Latex:
\mforall{}[Info:Type]
\mforall{}L1,L2:(Id \mtimes{} Info) List.
(L1 || L2
{}\mRightarrow{} (\mexists{}L:(Id \mtimes{} Info) List
((\mexists{}f:E {}\mrightarrow{} E
\mexists{}g:E {}\mrightarrow{} E. es-weak-joint-embedding(Info;global-eo(L1);global-eo(L2);global-eo(L);f;g))
\mwedge{} (\mforall{}L':(Id \mtimes{} Info) List. (L1 || L' {}\mRightarrow{} L2 || L' {}\mRightarrow{} L || L')))))
Date html generated:
2015_07_21-PM-04_40_13
Last ObjectModification:
2015_02_04-PM-05_58_42
Home
Index