---

Step * 2 of Lemma assert-test-msg-header-and-loc


1. [f] : Name ─→ Type
2. msg : Message(f)@i
3. hdr : Name@i
4. ¬(msg-header(msg) = hdr ∈ Name)
5. loc : Id@i
6. [%] : hdr encodes Id × Top
⊢ uiff(False;(msg-header(msg) = hdr ∈ Name) ∧ (loc = (fst(msg-body(msg))) ∈ Id))
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.  loc  :  Id@i
6.  [\%]  :  hdr  encodes  Id  \mtimes{}  Top
\mvdash{}  uiff(False;(msg-header(msg)  =  hdr)  \mwedge{}  (loc  =  (fst(msg-body(msg)))))


By

---

Latex:
Auto

---

Home Index