Nuprl Lemma : msg-has-type-encodes
∀[f,m,T:Top]. (msg-has-type(m;f;T) ~ msg-header(m) encodes T)
Proof
Definitions occuring in Statement :
encodes-msg-type: hdr encodes T,
msg-has-type: msg-has-type(m;f;T),
msg-header: msg-header(m),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
encodes-msg-type: hdr encodes T,
msg-has-type: msg-has-type(m;f;T),
msg-type: msg-type(msg;f)
Latex:
\mforall{}[f,m,T:Top]. (msg-has-type(m;f;T) \msim{} msg-header(m) encodes T)
Date html generated:
2016_05_17-AM-08_51_52
Last ObjectModification:
2015_12_29-PM-02_56_00
Theory : messages
Home
Index