---

Step * 1 1 of Lemma iseg-local-simulation-inputs


1. f : Name ─→ Type@i'
2. Info : Type
3. es : EO+(Message(f))@i'
4. hdr : Name@i
5. locs : bag(Id)@i
6. hdr encodes Id × Info
7. e1 : E@i
8. e2 : E@i
9. e1 ≤loc e2 @i
10. ∀x:Message(f). (↑((λm.has-header-and-in-locs(m;hdr;locs)) x) ∈ Type)
11. m : Message(f)@i
12. ↑((λm.has-header-and-in-locs(m;hdr;locs)) m)@i
⊢ msg-type(m;f) ⊆r (Id × Info)
BY
{ (Reduce (-1) THEN RWO  "assert-has-header-and-in-locs" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type@i'
2.  Info  :  Type
3.  es  :  EO+(Message(f))@i'
4.  hdr  :  Name@i
5.  locs  :  bag(Id)@i
6.  hdr  encodes  Id  \mtimes{}  Info
7.  e1  :  E@i
8.  e2  :  E@i
9.  e1  \mleq{}loc  e2  @i
10.  \mforall{}x:Message(f).  (\muparrow{}((\mlambda{}m.has-header-and-in-locs(m;hdr;locs))  x)  \mmember{}  Type)
11.  m  :  Message(f)@i
12.  \muparrow{}((\mlambda{}m.has-header-and-in-locs(m;hdr;locs))  m)@i
\mvdash{}  msg-type(m;f)  \msubseteq{}r  (Id  \mtimes{}  Info)


By

---

Latex:
(Reduce  (-1)  THEN  RWO    "assert-has-header-and-in-locs"  (-1)  THEN  Auto)

---

Home Index