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)
Definitions unfolded in proof :
label: ...$L... t,
top: Top,
guard: {T},
cand: A c∧ B,
exists: ∃x:A. B[x],
local-simulation-eo: local-simulation-eo(es;e;hdr;locs),
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
encodes-msg-type: hdr encodes T,
subtype_rel: A ⊆r B,
member: t ∈ T,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
implies: P ⇒ Q,
all: ∀x:A. B[x],
l_all: (∀x∈L.P[x]),
squash: ↓T,
less_than: a < b,
not: ¬A,
false: False,
satisfiable_int_formula: satisfiable_int_formula(fmla),
or: P ∨ Q,
decidable: Dec(P),
lelt: i ≤ j < k,
int_seg: {i..j-},
bag-member: x ↓∈ bs,
classrel: v ∈ X(e)
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:
2016_05_17-AM-09_14_13
Last ObjectModification:
2016_04_03-PM-09_43_43
Theory : classrel!lemmas
Home
Index