---

Step * 1 1 of Lemma es-info-mk-msg


1. f : Name ─→ Type
2. es : EO+(Message(f))
3. e : E
4. auth : 𝔹
5. hdr : Name
6. v : f hdr
7. v2 : 𝔹@i
8. h : Name@i
9. v4 : f h@i
10. info(e) = <v2, h, v4> ∈ Message(f)@i
11. h = hdr ∈ Name@i
12. v4 = v ∈ (f hdr)@i
13. v2 = auth@i
⊢ mk-msg(auth;hdr;v) = <auth, h, v4> ∈ Message(f)
BY
{ RepUR ``mk-msg make-basicMsg Message basicMessage`` 0 }

1
1. f : Name ─→ Type
2. es : EO+(Message(f))
3. e : E
4. auth : 𝔹
5. hdr : Name
6. v : f hdr
7. v2 : 𝔹@i
8. h : Name@i
9. v4 : f h@i
10. info(e) = <v2, h, v4> ∈ Message(f)@i
11. h = hdr ∈ Name@i
12. v4 = v ∈ (f hdr)@i
13. v2 = auth@i
⊢ <auth, hdr, v> = <auth, h, v4> ∈ (𝔹 × h:Name × (f h))

---

Latex:

---

Latex:

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


By

---

Latex:
RepUR  ``mk-msg  make-basicMsg  Message  basicMessage``  0

---

Home Index