---

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


1. [f] : Name ─→ Type
2. msg : Message(f)@i
3. hdr : Name@i
4. loc : Id@i
5. [%] : hdr encodes Id × Top
6. msg-header(msg) = hdr ∈ Name
⊢ uiff(↑loc = fst(msg-body(msg));(msg-header(msg) = hdr ∈ Name) ∧ (loc = (fst(msg-body(msg))) ∈ Id))
BY
{ (Assert ⌈msg-body(msg) ∈ Id × Top⌉⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [f]  :  Name  {}\mrightarrow{}  Type
2.  msg  :  Message(f)@i
3.  hdr  :  Name@i
4.  loc  :  Id@i
5.  [\%]  :  hdr  encodes  Id  \mtimes{}  Top
6.  msg-header(msg)  =  hdr
\mvdash{}  uiff(\muparrow{}loc  =  fst(msg-body(msg));(msg-header(msg)  =  hdr)  \mwedge{}  (loc  =  (fst(msg-body(msg)))))


By

---

Latex:
(Assert  \mkleeneopen{}msg-body(msg)  \mmember{}  Id  \mtimes{}  Top\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index