Nuprl Lemma : consistent-local-simulation
∀g,f:Name ─→ Type. ∀X:EClass(Interface).
(LocalClass(X)
⇒ (∀locs:bag(Id). ∀hdr:Name.
∀es:EO+(Message(f)). ∀ee:E List.
((∀e1,e2∈ee. local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))
⇒ (∀hdrs:Name List
((∀e∈ee.eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))
⇒ (∃eo:EO+(Message(g))
(eo-msg-interface-constraint(eo;X;hdrs;g)
∧ (∀e∈ee.∀[v:Interface]
(↑has-header-and-in-locs(info(e);hdr;locs)) ∧ (∃e':E. v ∈ X(e'))
supposing v ∈ local-simulation-class(X;locs;hdr)(e)))))))
supposing hdr encodes Id × Message(g)))
Proof
Definitions occuring in Statement :
eo-msg-interface-constraint: eo-msg-interface-constraint(es;X;hdrs;f),
msg-interface: Interface,
local-simulation-eo: local-simulation-eo(es;e;hdr;locs),
local-simulation-inputs: local-simulation-inputs(es;e;hdr;locs),
has-header-and-in-locs: has-header-and-in-locs(msg;hdr;locs),
local-simulation-class: local-simulation-class(X;locs;hdr),
encodes-msg-type: hdr encodes T,
Message: Message(f),
global-order-compat: L1 || L2,
local-class: LocalClass(X),
classrel: v ∈ X(e),
eclass: EClass(A[eo; e]),
es-info: info(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
name: Name,
pairwise: (∀x,y∈L. P[x; y]),
l_all: (∀x∈L.P[x]),
list: T List,
assert: ↑b,
uimplies: b supposing a,
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,
bag: bag(T)
Lemmas :
local-simulation-inputs_wf,
local-simulation-classrel,
global-order-pairwise-compat-msg-and-classrel,
map_wf,
list_wf,
subtype_rel_list,
bag-member_wf,
subtype_rel_product,
subtype_rel_self,
set_wf,
pairwise-map1,
global-order-compat_wf,
l_all_map,
eo-msg-interface-constraint_wf,
global-eo_wf,
l_all_wf2,
l_member_wf,
uall_wf,
isect_wf,
classrel_wf,
local-simulation-class_wf,
assert_wf,
has-header-and-in-locs_wf,
es-info_wf,
top_wf,
subtype_top,
subtype_rel_transitivity,
exists_wf,
es-E_wf,
event-ordering+_subtype,
Message_wf,
local-simulation-eo_wf,
pairwise_wf,
event-ordering+_wf,
encodes-msg-type_wf,
name_wf,
bag_wf,
Id_wf,
local-class_wf,
eclass_wf3,
msg-interface_wf,
length-map,
select-map,
int_seg_wf,
length_wf,
select_wf,
sq_stable__le,
local-simulation-event_wf,
assert_witness,
iff_weakening_uiff
Latex:
\mforall{}g,f:Name {}\mrightarrow{} Type. \mforall{}X:EClass(Interface).
(LocalClass(X)
{}\mRightarrow{} (\mforall{}locs:bag(Id). \mforall{}hdr:Name.
\mforall{}es:EO+(Message(f)). \mforall{}ee:E List.
((\mforall{}e1,e2\mmember{}ee.
local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))
{}\mRightarrow{} (\mforall{}hdrs:Name List
((\mforall{}e\mmember{}ee.eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))
{}\mRightarrow{} (\mexists{}eo:EO+(Message(g))
(eo-msg-interface-constraint(eo;X;hdrs;g)
\mwedge{} (\mforall{}e\mmember{}ee.\mforall{}[v:Interface]
(\muparrow{}has-header-and-in-locs(info(e);hdr;locs)) \mwedge{} (\mexists{}e':E. v \mmember{} X(e'))
supposing v \mmember{} local-simulation-class(X;locs;hdr)(e)))))))
supposing hdr encodes Id \mtimes{} Message(g)))
Date html generated:
2015_07_22-PM-00_07_06
Last ObjectModification:
2015_01_28-AM-11_43_04
Home
Index