---

Step * 1 of Lemma message-constraint-swap-hdr_wf


1. f : Name ⟶ Type
2. es : EO+(Message(f))
3. X : EClass(Id × Message(f))
4. hdr_in : Name
5. hdrs_out : Name List
6. e : E@i'
7. header(e) = hdr_in ∈ Name
8. e' : E@i'
9. hdr : Name@i
10. (hdr ∈ hdrs_out)
11. (f hdr) = (f hdr_in) ∈ Type
12. (e' < e)
⊢ msgval(e) ∈ f hdr
BY
{ (SubsumeC ⌜f hdr_in⌝⋅
   THEN Auto
   THEN DoSubsume
   THEN Auto
   THEN RepUR ``es-info-type msg-type`` 0
   THEN Fold `es-header` 0
   THEN HypSubst' 7 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  es  :  EO+(Message(f))
3.  X  :  EClass(Id  \mtimes{}  Message(f))
4.  hdr$_{in}$  :  Name
5.  hdrs$_{out}$  :  Name  List
6.  e  :  E@i'
7.  header(e)  =  hdr$_{in}$
8.  e'  :  E@i'
9.  hdr  :  Name@i
10.  (hdr  \mmember{}  hdrs$_{out}$)
11.  (f  hdr)  =  (f  hdr$_{in}$)
12.  (e'  <  e)
\mvdash{}  msgval(e)  \mmember{}  f  hdr


By

---

Latex:
(SubsumeC  \mkleeneopen{}f  hdr$_{in}$\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  DoSubsume
  THEN  Auto
  THEN  RepUR  ``es-info-type  msg-type``  0
  THEN  Fold  `es-header`  0
  THEN  HypSubst'  7  0
  THEN  Auto)

---

Home Index