---

Step * of Lemma es-info-mk-msg

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[auth:𝔹]. ∀[hdr:Name]. ∀[v:f hdr].
  (mk-msg(auth;hdr;v) = info(e) ∈ Message(f)) supposing 
     (msg-authentic(info(e)) = auth and 
     (msg-body(info(e)) = v ∈ (f hdr)) and 
     (header(e) = hdr ∈ Name))
BY
{ Intros }

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

2
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
⊢ (msg-body(info(e)) = v ∈ (f hdr)) = (msg-body(info(e)) = v ∈ (f hdr)) ∈ Type

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[auth:\mBbbB{}].  \mforall{}[hdr:Name].  \mforall{}[v:f  hdr].
    (mk-msg(auth;hdr;v)  =  info(e))  supposing 
          (msg-authentic(info(e))  =  auth  and 
          (msg-body(info(e))  =  v)  and 
          (header(e)  =  hdr))


By

---

Latex:
Intros

---

Home Index