Nuprl Lemma : local-simulation-class_wf
∀[f:Name ─→ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[locs:bag(Id)]. ∀[hdr:Name].
local-simulation-class(X;locs;hdr) ∈ EClass(T) supposing hdr encodes Id × Info
Proof
Definitions occuring in Statement :
local-simulation-class: local-simulation-class(X;locs;hdr),
encodes-msg-type: hdr encodes T,
Message: Message(f),
eclass: EClass(A[eo; e]),
Id: Id,
name: Name,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ─→ B[x],
product: x:A × B[x],
universe: Type,
bag: bag(T)
Lemmas :
parallel-bag-class_wf,
Message_wf,
base-process-class_wf,
encodes-msg-type_wf,
Id_wf,
name_wf,
bag_wf,
eclass_wf,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[Info,T:Type]. \mforall{}[X:EClass(T)]. \mforall{}[locs:bag(Id)]. \mforall{}[hdr:Name].
local-simulation-class(X;locs;hdr) \mmember{} EClass(T) supposing hdr encodes Id \mtimes{} Info
Date html generated:
2015_07_21-PM-04_49_43
Last ObjectModification:
2015_01_28-AM-08_44_45
Home
Index