---

Step * 1 1 of Lemma es-info-make-Msg


1. f : Name ─→ Type
2. es : EO+(Message(f))
3. e : E
4. hdr : Name
5. v : f hdr
6. v2 : 𝔹@i
7. h : Name@i
8. v4 : f h@i
9. info(e) = <v2, h, v4> ∈ Message(f)@i
10. h = hdr ∈ Name@i
11. v4 = v ∈ (f hdr)@i
12. v2 = ff@i
⊢ make-Msg(hdr;v) = <ff, h, v4> ∈ Message(f)
BY
{ (RW (AddrC [3;2] (FoldC `make-basicMsg`)) 0 THEN Fold `make-Msg` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  es  :  EO+(Message(f))
3.  e  :  E
4.  hdr  :  Name
5.  v  :  f  hdr
6.  v2  :  \mBbbB{}@i
7.  h  :  Name@i
8.  v4  :  f  h@i
9.  info(e)  =  <v2,  h,  v4>@i
10.  h  =  hdr@i
11.  v4  =  v@i
12.  v2  =  ff@i
\mvdash{}  make-Msg(hdr;v)  =  <ff,  h,  v4>


By

---

Latex:
(RW  (AddrC  [3;2]  (FoldC  `make-basicMsg`))  0  THEN  Fold  `make-Msg`  0  THEN  Auto)

---

Home Index