Nuprl Lemma : cond-msg-body-cbva
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[msg:Message(f)]. ∀[G:Top].
  let x ⟵ cond-msg-body(hdr;msg) in G[x] ~ G[cond-msg-body(hdr;msg)] supposing valueall-type(f hdr)
Proof
Definitions occuring in Statement : 
cond-msg-body: cond-msg-body(hdr;msg)
, 
Message: Message(f)
, 
name: Name
, 
valueall-type: valueall-type(T)
, 
callbyvalueall: callbyvalueall, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
so_apply: x[s]
, 
apply: f a
, 
function: x:A ⟶ B[x]
, 
universe: Type
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
uimplies: b supposing a
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
callbyvalueall: callbyvalueall, 
has-value: (a)↓
, 
has-valueall: has-valueall(a)
Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdr:Name].  \mforall{}[msg:Message(f)].  \mforall{}[G:Top].
    let  x  \mleftarrow{}{}  cond-msg-body(hdr;msg)  in  G[x]  \msim{}  G[cond-msg-body(hdr;msg)]  supposing  valueall-type(f  hdr)
Date html generated:
2016_05_17-AM-08_52_11
Last ObjectModification:
2015_12_29-PM-02_55_41
Theory : messages
Home
Index