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
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
squash: ↓T,
true: True,
subtype_rel: A ⊆r B,
prop: ℙ
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:
2016_05_17-AM-08_51_25
Last ObjectModification:
2016_01_17-PM-08_35_31
Theory : messages
Home
Index