---

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

∀[f:Name ─→ Type]
  ∀msg:Message(f). ∀hdr:Name. ∀locs:bag(Id).
    ↑has-header-and-in-locs(msg;hdr;locs) ⇐⇒ (msg-header(msg) = hdr ∈ Name) ∧ fst(msg-body(msg)) ↓∈ locs 
    supposing hdr encodes Id × Top
BY
{ (Intros THEN RepUR ``has-header-and-in-locs`` 0 THEN (BoolCase ⌈name_eq(msg-header(msg);hdr)⌉⋅ THENA 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
⊢ ↑bag-deq-member(IdDeq;fst(msg-body(msg));locs) ⇐⇒ (msg-header(msg) = hdr ∈ Name) ∧ fst(msg-body(msg)) ↓∈ locs

2
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

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type]
    \mforall{}msg:Message(f).  \mforall{}hdr:Name.  \mforall{}locs:bag(Id).
        \muparrow{}has-header-and-in-locs(msg;hdr;locs)  \mLeftarrow{}{}\mRightarrow{}  (msg-header(msg)  =  hdr)  \mwedge{}  fst(msg-body(msg))  \mdownarrow{}\mmember{}  locs 
        supposing  hdr  encodes  Id  \mtimes{}  Top


By

---

Latex:
(Intros
  THEN  RepUR  ``has-header-and-in-locs``  0
  THEN  (BoolCase  \mkleeneopen{}name\_eq(msg-header(msg);hdr)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index