---

Step * 1 3 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. e' : E@i
10. e' ≤loc e @i
11. msg-header(info(e')) = hdr ∈ Name@i
12. fst(v) ↓∈ locs@i
13. v = msg-body(info(e')) ∈ (Id × Info)@i
⊢ ∃y:Message(f)
   ((y ∈ map(λe.info(e);≤loc(e))) ∧ ((↑has-header-and-in-locs(y;hdr;locs)) c∧ (v = msg-body(y) ∈ (Id × Info))))
BY
{ (With ⌈info(e')⌉ (D 0)⋅ THEN Auto) }

1
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. e' : E@i
10. e' ≤loc e @i
11. msg-header(info(e')) = hdr ∈ Name@i
12. fst(v) ↓∈ locs@i
13. v = msg-body(info(e')) ∈ (Id × Info)@i
⊢ (info(e') ∈ map(λe.info(e);≤loc(e)))

2
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. e' : E@i
10. e' ≤loc e @i
11. msg-header(info(e')) = hdr ∈ Name@i
12. fst(v) ↓∈ locs@i
13. v = msg-body(info(e')) ∈ (Id × Info)@i
14. (info(e') ∈ map(λe.info(e);≤loc(e)))
⊢ ↑has-header-and-in-locs(info(e');hdr;locs)

3
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. e' : E@i
10. e' ≤loc e @i
11. msg-header(info(e')) = hdr ∈ Name@i
12. fst(v) ↓∈ locs@i
13. v = msg-body(info(e')) ∈ (Id × Info)@i
14. y : Message(f)
15. (y ∈ map(λe.info(e);≤loc(e)))
16. ↑has-header-and-in-locs(y;hdr;locs)
⊢ msg-type(y;f) ⊆r (Id × Info)

---

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.  e'  :  E@i
10.  e'  \mleq{}loc  e  @i
11.  msg-header(info(e'))  =  hdr@i
12.  fst(v)  \mdownarrow{}\mmember{}  locs@i
13.  v  =  msg-body(info(e'))@i
\mvdash{}  \mexists{}y:Message(f)
      ((y  \mmember{}  map(\mlambda{}e.info(e);\mleq{}loc(e)))  \mwedge{}  ((\muparrow{}has-header-and-in-locs(y;hdr;locs))  c\mwedge{}  (v  =  msg-body(y))))


By

---

Latex:
(With  \mkleeneopen{}info(e')\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index