---

Step * 1 1 of Lemma assert-has-header-and-in-locs


1. f : Name ─→ Type
2. msg : Message(f)@i
3. hdr : Name@i
4. locs : bag(Id)@i
5. hdr encodes Id × Top
6. msg-header(msg) = hdr ∈ Name
7. msg-body(msg) ∈ Id × Top
8. ↑bag-deq-member(IdDeq;fst(msg-body(msg));locs)@i
⊢ fst(msg-body(msg)) ↓∈ locs
BY
{ (RWO "assert-bag-deq-member" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  msg  :  Message(f)@i
3.  hdr  :  Name@i
4.  locs  :  bag(Id)@i
5.  hdr  encodes  Id  \mtimes{}  Top
6.  msg-header(msg)  =  hdr
7.  msg-body(msg)  \mmember{}  Id  \mtimes{}  Top
8.  \muparrow{}bag-deq-member(IdDeq;fst(msg-body(msg));locs)@i
\mvdash{}  fst(msg-body(msg))  \mdownarrow{}\mmember{}  locs


By

---

Latex:
(RWO  "assert-bag-deq-member"  (-1)  THEN  Auto)

---

Home Index