---

Step * 1 1 1 of Lemma member-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. e : E@i
8. v : Id × Info@i
9. y : Message(f)
10. y1 : {a:E| loc(a) = loc(e) ∈ Id} 
11. (y1 ∈ ≤loc(e))
12. y = info(y1) ∈ Message(f)
13. ↑has-header-and-in-locs(y;hdr;locs)
14. v = msg-body(y) ∈ (Id × Info)
⊢ ∃e':E. (e' ≤loc e  ∧ (msg-header(info(e')) = hdr ∈ Name) ∧ fst(v) ↓∈ locs ∧ (v = msg-body(info(e')) ∈ (Id × Info)))
BY
{ ((RWO "member-es-le-before2" (-4) THENA Auto)
   THEN (HypSubst' (-3) (-2) THENA Auto)
   THEN (RWO "assert-has-header-and-in-locs" (-2) THENA Auto)
   THEN With ⌈y1⌉ (D 0)⋅
   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.  e  :  E@i
8.  v  :  Id  \mtimes{}  Info@i
9.  y  :  Message(f)
10.  y1  :  \{a:E|  loc(a)  =  loc(e)\} 
11.  (y1  \mmember{}  \mleq{}loc(e))
12.  y  =  info(y1)
13.  \muparrow{}has-header-and-in-locs(y;hdr;locs)
14.  v  =  msg-body(y)
\mvdash{}  \mexists{}e':E.  (e'  \mleq{}loc  e    \mwedge{}  (msg-header(info(e'))  =  hdr)  \mwedge{}  fst(v)  \mdownarrow{}\mmember{}  locs  \mwedge{}  (v  =  msg-body(info(e'))))


By

---

Latex:
((RWO  "member-es-le-before2"  (-4)  THENA  Auto)
  THEN  (HypSubst'  (-3)  (-2)  THENA  Auto)
  THEN  (RWO  "assert-has-header-and-in-locs"  (-2)  THENA  Auto)
  THEN  With  \mkleeneopen{}y1\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index