---

Step * of Lemma map-cond-msg-body

∀[g,hdr,m:Top].  (map(g;cond-msg-body(hdr;m)) ~ if name_eq(msg-header(m);hdr) then {g msg-body(m)} else {} fi )
BY
{ (Auto
   THEN RepUR ``cond-msg-body`` 0
   THEN RWO "map-ifthenelse" 0
   THEN Try (Fold `bag-map` 0)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g,hdr,m:Top].
    (map(g;cond-msg-body(hdr;m))  \msim{}  if  name\_eq(msg-header(m);hdr)  then  \{g  msg-body(m)\}  else  \{\}  fi  )


By

---

Latex:
(Auto
  THEN  RepUR  ``cond-msg-body``  0
  THEN  RWO  "map-ifthenelse"  0
  THEN  Try  (Fold  `bag-map`  0)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index