Nuprl Lemma : es-info-body-equal
∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e,e':E]. ∀[T:Type].
(msgval(e) = msgval(e') ∈ T) supposing ((e = e' ∈ E) and ((f header(e)) ⊆r T))
Proof
Definitions occuring in Statement :
es-info-body: msgval(e),
es-header: header(e),
Message: Message(f),
event-ordering+: EO+(Info),
es-E: E,
name: Name,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
apply: f a,
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
es-info-body_wf,
equal_wf,
subtype_rel_wf,
es-header_wf
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[es:EO+(Message(f))]. \mforall{}[e,e':E]. \mforall{}[T:Type].
(msgval(e) = msgval(e')) supposing ((e = e') and ((f header(e)) \msubseteq{}r T))
Date html generated:
2015_07_21-PM-04_48_46
Last ObjectModification:
2015_01_28-AM-08_46_53
Home
Index