---

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


1. [f] : Name ─→ Type
2. msg : Message(f)@i
3. hdr : Name@i
4. ¬(msg-header(msg) = hdr ∈ Name)
5. locs : bag(Id)@i
6. [%] : hdr encodes Id × Top
⊢ False ⇐⇒ (msg-header(msg) = hdr ∈ Name) ∧ fst(msg-body(msg)) ↓∈ locs
BY
{ Auto }

---

Latex:

---

Latex:

1.  [f]  :  Name  {}\mrightarrow{}  Type
2.  msg  :  Message(f)@i
3.  hdr  :  Name@i
4.  \mneg{}(msg-header(msg)  =  hdr)
5.  locs  :  bag(Id)@i
6.  [\%]  :  hdr  encodes  Id  \mtimes{}  Top
\mvdash{}  False  \mLeftarrow{}{}\mRightarrow{}  (msg-header(msg)  =  hdr)  \mwedge{}  fst(msg-body(msg))  \mdownarrow{}\mmember{}  locs


By

---

Latex:
Auto

---

Home Index