Nuprl Lemma : local-simulation-classrel
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)].
∀locs:bag(Id). ∀hdr:Name.
∀es:EO+(Message(f)). ∀e:E.
∀[v:T]
uiff(v ∈ local-simulation-class(X;locs;hdr)(e);(↑has-header-and-in-locs(info(e);hdr;locs))
∧ v ∈ X(local-simulation-event(es;e;hdr;locs)))
supposing LocalClass(X)
supposing hdr encodes Id × Info
Proof
Definitions occuring in Statement :
local-simulation-event: local-simulation-event(es;e;hdr;locs),
local-simulation-eo: local-simulation-eo(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),
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,
assert: ↑b,
uiff: uiff(P;Q),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
and: P ∧ Q,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
bag: bag(T)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
uimplies: b supposing a,
encodes-msg-type: hdr encodes T,
guard: {T},
so_lambda: λ2x.t[x],
so_apply: x[s],
subtype_rel: A ⊆r B,
top: Top,
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
and: P ∧ Q,
assert: ↑b,
ifthenelse: if b then t else f fi ,
bfalse: ff,
exists: ∃x:A. B[x],
prop: ℙ,
or: P ∨ Q,
sq_type: SQType(T),
bnot: ¬bb,
false: False,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
local-simulation-class: local-simulation-class(X;locs;hdr),
iff: P ⇐⇒ Q,
true: True,
classrel: v ∈ X(e),
bag-member: x ↓∈ bs,
squash: ↓T,
rev_implies: P ⇐ Q,
base-process-class: base-process-class(X;loc;hdr),
Id: Id,
cand: A c∧ B,
msg-type: msg-type(msg;f),
eclass: EClass(A[eo; e]),
rev_uimplies: rev_uimplies(P;Q),
let: let,
class-ap: X(e),
listp: A List+,
int_seg: {i..j-},
lelt: i ≤ j < k,
decidable: Dec(P),
less_than: a < b,
satisfiable_int_formula: satisfiable_int_formula(fmla),
not: ¬A,
eo-local-agree: eo-local-agree(Info;eo1;eo2;e1;e2),
local-simulation-eo: local-simulation-eo(es;e;hdr;locs),
base-process-inputs: base-process-inputs(loc;hdr;es;e),
local-simulation-inputs: local-simulation-inputs(es;e;hdr;locs),
mapfilter: mapfilter(f;P;L),
es-le-before: ≤loc(e),
local-simulation-event: local-simulation-event(es;e;hdr;locs),
compose: f o g,
band: p ∧b q
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[Info,T:Type]. \mforall{}[X:EClass(T)].
\mforall{}locs:bag(Id). \mforall{}hdr:Name.
\mforall{}es:EO+(Message(f)). \mforall{}e:E.
\mforall{}[v:T]
uiff(v \mmember{} local-simulation-class(X;locs;hdr)(e);(\muparrow{}has-header-and-in-locs(info(e);hdr;locs))
\mwedge{} v \mmember{} X(local-simulation-event(es;e;hdr;locs)))
supposing LocalClass(X)
supposing hdr encodes Id \mtimes{} Info
Date html generated:
2016_05_17-AM-09_13_47
Last ObjectModification:
2016_01_17-PM-11_16_51
Theory : classrel!lemmas
Home
Index