Nuprl Lemma : local-simulation-validity
∀correct:Id ⟶ ℙ. ∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
(LocalClass(X)
⇒ (∀locs:bag(Id). ∀hdr:Name.
∀hdrs:Name List. ∀es:EO+(Message(f)).
((∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
⇒ (∀P:Interface ⟶ ℙ. ∀R:Interface ⟶ Message(g) ⟶ ℙ.
((∀eo:EO+(Message(g))
(eo-msg-interface-constraint(eo;X;hdrs;g)
⇒ (∀e:E. ∀v:Interface. (v ∈ X(e) ⇒ P[v] ⇒ (↓∃e':E. ((e' < e) ∧ R[v;info(e')]))))))
⇒ (∀e:E. ∀v:Interface.
((correct loc(e))
⇒ v ∈ local-simulation-class(X;locs;hdr)(e)
⇒ P[v]
⇒ (↓∃e':E
((e' <loc e)
∧ (↑has-header-and-in-locs(info(e');hdr;locs))
∧ R[v;snd(msg-body(info(e')))])))))))
supposing hdr encodes Id × Message(g)))
Proof
Definitions occuring in Statement :
local-simulation-input-validity: local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i),
eo-msg-interface-constraint: eo-msg-interface-constraint(es;X;hdrs;f),
msg-interface: Interface,
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,
msg-body: msg-body(msg),
Message: Message(f),
local-class: LocalClass(X),
classrel: v ∈ X(e),
eclass: EClass(A[eo; e]),
es-info: info(e),
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
name: Name,
list: T List,
assert: ↑b,
uimplies: b supposing a,
prop: ℙ,
so_apply: x[s1;s2],
so_apply: x[s],
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
bag: bag(T)
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
uiff: uiff(P;Q),
and: P ∧ Q,
subtype_rel: A ⊆r B,
squash: ↓T,
exists: ∃x:A. B[x],
prop: ℙ,
so_apply: x[s],
so_lambda: λ2x.t[x],
encodes-msg-type: hdr encodes T,
so_apply: x[s1;s2],
label: ...$L... t,
guard: {T},
local-simulation-eo: local-simulation-eo(es;e;hdr;locs),
top: Top,
iff: P ⇐⇒ Q,
local-simulation-event: local-simulation-event(es;e;hdr;locs),
compose: f o g,
sq_stable: SqStable(P),
int_seg: {i..j-},
lelt: i ≤ j < k,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
false: False,
not: ¬A,
le: A ≤ B,
cand: A c∧ B,
local-simulation-inputs: local-simulation-inputs(es;e;hdr;locs),
es-le-before: ≤loc(e),
mapfilter: mapfilter(f;P;L),
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
sq_type: SQType(T),
bnot: ¬bb,
assert: ↑b,
nat: ℕ,
msg-type: msg-type(msg;f),
rev_implies: P ⇐ Q
Latex:
\mforall{}correct:Id {}\mrightarrow{} \mBbbP{}. \mforall{}g,f:Name {}\mrightarrow{} Type. \mforall{}X:EClass(Interface).
(LocalClass(X)
{}\mRightarrow{} (\mforall{}locs:bag(Id). \mforall{}hdr:Name.
\mforall{}hdrs:Name List. \mforall{}es:EO+(Message(f)).
((\mforall{}i:Id. ((correct i) {}\mRightarrow{} local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
{}\mRightarrow{} (\mforall{}P:Interface {}\mrightarrow{} \mBbbP{}. \mforall{}R:Interface {}\mrightarrow{} Message(g) {}\mrightarrow{} \mBbbP{}.
((\mforall{}eo:EO+(Message(g))
(eo-msg-interface-constraint(eo;X;hdrs;g)
{}\mRightarrow{} (\mforall{}e:E. \mforall{}v:Interface.
(v \mmember{} X(e) {}\mRightarrow{} P[v] {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} R[v;info(e')]))))))
{}\mRightarrow{} (\mforall{}e:E. \mforall{}v:Interface.
((correct loc(e))
{}\mRightarrow{} v \mmember{} local-simulation-class(X;locs;hdr)(e)
{}\mRightarrow{} P[v]
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
((e' <loc e)
\mwedge{} (\muparrow{}has-header-and-in-locs(info(e');hdr;locs))
\mwedge{} R[v;snd(msg-body(info(e')))])))))))
supposing hdr encodes Id \mtimes{} Message(g)))
Date html generated:
2016_05_17-AM-09_14_34
Last ObjectModification:
2016_01_17-PM-11_15_44
Theory : classrel!lemmas
Home
Index