---

Step * of 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)
BY
{ (Auto
   THEN GenConclAtAddrType ⌜bag(f hdr)⌝ [1;1]⋅
   THEN Auto
   THEN Try ((D 0 THEN Auto))
   THEN CallByValueReduce 0
   THEN Auto) }

---

Latex:

---

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)


By

---

Latex:
(Auto
  THEN  GenConclAtAddrType  \mkleeneopen{}bag(f  hdr)\mkleeneclose{}  [1;1]\mcdot{}
  THEN  Auto
  THEN  Try  ((D  0  THEN  Auto))
  THEN  CallByValueReduce  0
  THEN  Auto)

---

Home Index