---

Step * 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
⊢ ↑bag-deq-member(IdDeq;fst(msg-body(msg));locs) ⇐⇒ (msg-header(msg) = hdr ∈ Name) ∧ fst(msg-body(msg)) ↓∈ locs
BY
{ (Assert ⌈msg-body(msg) ∈ Id × Top⌉⋅ THEN Auto) }

1
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

---

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
\mvdash{}  \muparrow{}bag-deq-member(IdDeq;fst(msg-body(msg));locs)
\mLeftarrow{}{}\mRightarrow{}  (msg-header(msg)  =  hdr)  \mwedge{}  fst(msg-body(msg))  \mdownarrow{}\mmember{}  locs


By

---

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

---

Home Index