Nuprl Lemma : global-order-pairwise-compat-squash-invariant
∀[Info:Type]. ∀[P:Id ─→ Info List+ ─→ ℙ]. ∀[R:Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ].
∀LL:(Id × Info) List List
((∀L1,L2∈LL. L1 || L2)
⇒ (∀L∈LL.squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) global-eo(L))
⇒ (∃G:(Id × Info) List
((squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) global-eo(G))
∧ (∀L∈LL.∃f:E ─→ E. es-local-embedding(Info;global-eo(L);global-eo(G);f)))))
Proof
Definitions occuring in Statement :
global-order-compat: L1 || L2,
global-eo: global-eo(L),
squash-causal-invariant: squash-causal-invariant(i,L.P[i; L];a,b,L1,L2.R[a; b; L1; L2]),
es-local-embedding: es-local-embedding(Info;eo1;eo2;f),
es-E: E,
Id: Id,
pairwise: (∀x,y∈L. P[x; y]),
listp: A List+,
l_all: (∀x∈L.P[x]),
list: T List,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ─→ B[x],
product: x:A × B[x],
universe: Type
Lemmas :
list_induction,
list_wf,
pairwise_wf,
global-order-compat_wf,
l_all_wf2,
l_member_wf,
global-eo_wf,
exists_wf,
all_wf,
es-E_wf,
event-ordering+_subtype,
es-local-embedding_wf,
nil_wf,
cons_wf,
Id_wf,
global-eo-E-sq,
length_of_nil_lemma,
es-local-property_wf,
subtype_rel-equal,
listp_wf,
int_seg_wf,
l_all_nil,
filter_nil_lemma,
nil_iseg,
filter_wf5,
eq_id_wf,
iseg_wf,
pairwise-cons,
l_all-cons,
global-order-compat-squash-invariant,
compat_symmetry,
length_wf,
compose_wf,
select_wf,
sq_stable__le,
es-local-embedding-compose
Latex:
\mforall{}[Info:Type]. \mforall{}[P:Id {}\mrightarrow{} Info List\msupplus{} {}\mrightarrow{} \mBbbP{}]. \mforall{}[R:Id {}\mrightarrow{} Id {}\mrightarrow{} Info List\msupplus{} {}\mrightarrow{} Info List\msupplus{} {}\mrightarrow{} \mBbbP{}].
\mforall{}LL:(Id \mtimes{} Info) List List
((\mforall{}L1,L2\mmember{}LL. L1 || L2)
{}\mRightarrow{} (\mforall{}L\mmember{}LL.squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) global-eo(L))
{}\mRightarrow{} (\mexists{}G:(Id \mtimes{} Info) List
((squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) global-eo(G))
\mwedge{} (\mforall{}L\mmember{}LL.\mexists{}f:E {}\mrightarrow{} E. es-local-embedding(Info;global-eo(L);global-eo(G);f)))))
Date html generated:
2015_07_21-PM-04_41_25
Last ObjectModification:
2015_01_27-PM-05_04_47
Home
Index