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


1. Name ─→ Type
2. es EO+(Message(f))
3. E
4. hdr Name
5. hdr
6. header(e) hdr ∈ Name
⊢ (msg-body(info(e)) v ∈ (f hdr)) (msg-body(info(e)) v ∈ (f hdr)) ∈ Type
BY
(EqCD THEN Auto) }

1
1. Name ─→ Type
2. es EO+(Message(f))
3. E
4. hdr Name
5. hdr
6. header(e) hdr ∈ Name
⊢ msg-type(info(e);f) ⊆(f hdr)


Latex:



Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  es  :  EO+(Message(f))
3.  e  :  E
4.  hdr  :  Name
5.  v  :  f  hdr
6.  header(e)  =  hdr
\mvdash{}  (msg-body(info(e))  =  v)  =  (msg-body(info(e))  =  v)


By


Latex:
(EqCD  THEN  Auto)




Home Index