---

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

∀[f:Name ⟶ Type]
  ∀msg:Message(f). ∀hdr:Name. ∀loc:Id.
    uiff(↑test-msg-header-and-loc(msg;hdr;loc);(msg-header(msg) = hdr ∈ Name) ∧ (loc = (fst(msg-body(msg))) ∈ Id)) 
    supposing hdr encodes Id × Top
BY
{ (Intros THEN RepUR ``test-msg-header-and-loc`` 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. 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))

2
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))

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type]
    \mforall{}msg:Message(f).  \mforall{}hdr:Name.  \mforall{}loc:Id.
        uiff(\muparrow{}test-msg-header-and-loc(msg;hdr;loc);(msg-header(msg)  =  hdr)
        \mwedge{}  (loc  =  (fst(msg-body(msg))))) 
        supposing  hdr  encodes  Id  \mtimes{}  Top


By

---

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

---

Home Index