---

Step * 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. header(e) = hdr ∈ Name
8. msg-body(info(e)) = v ∈ (f hdr)
9. msg-authentic(info(e)) = auth
⊢ mk-msg(auth;hdr;v) = info(e) ∈ Message(f)
BY
{ (RepUR ``es-header`` (-3)⋅
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN GenConclAtAddr [1;2;1]⋅
   THEN RepeatFor 2 (D (-2))
   THEN RepUR ``msg-header msg-body msg-msg msg-authentic`` 0
   THEN Auto
   THEN HypSubst' (-1) 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
⊢ mk-msg(auth;hdr;v) = <auth, h, v4> ∈ Message(f)

---

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.  header(e)  =  hdr
8.  msg-body(info(e))  =  v
9.  msg-authentic(info(e))  =  auth
\mvdash{}  mk-msg(auth;hdr;v)  =  info(e)


By

---

Latex:
(RepUR  ``es-header``  (-3)\mcdot{}
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  GenConclAtAddr  [1;2;1]\mcdot{}
  THEN  RepeatFor  2  (D  (-2))
  THEN  RepUR  ``msg-header  msg-body  msg-msg  msg-authentic``  0
  THEN  Auto
  THEN  HypSubst'  (-1)  0)

---

Home Index