---

Step * 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. (v ∈ mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e))))
⇐⇒ ∃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))))
⊢ (v ∈ mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e))))
⇐⇒ ∃e':E. (e' ≤loc e  ∧ (msg-header(info(e')) = hdr ∈ Name) ∧ fst(v) ↓∈ locs ∧ (v = msg-body(info(e')) ∈ (Id × Info)))
BY
{ (RepeatFor 2 (D 0) THENM ((FHyp (-2) [-1] THEN RepeatFor 2 (Thin (-2))) ORELSE (BHyp -2  THEN Thin (-2)))) }

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. ∃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))))
⊢ ∃e':E. (e' ≤loc e  ∧ (msg-header(info(e')) = hdr ∈ Name) ∧ fst(v) ↓∈ locs ∧ (v = msg-body(info(e')) ∈ (Id × Info)))

2
.....wf..... 
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. (v ∈ mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e))))
⇐⇒ ∃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))))
⊢ (v ∈ mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e)))) ∈ ℙ

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. (e' ≤loc e  ∧ (msg-header(info(e')) = hdr ∈ Name) ∧ fst(v) ↓∈ locs ∧ (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))))

4
.....wf..... 
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. (v ∈ mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e))))
⇐⇒ ∃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))))
⊢ ∃e':E. (e' ≤loc e  ∧ (msg-header(info(e')) = hdr ∈ Name) ∧ fst(v) ↓∈ locs ∧ (v = msg-body(info(e')) ∈ (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.  (v  \mmember{}  mapfilter(\mlambda{}m.msg-body(m);\mlambda{}m.has-header-and-in-locs(m;hdr;locs);map(\mlambda{}e.info(e);\mleq{}loc(e))))
\mLeftarrow{}{}\mRightarrow{}  \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))))
\mvdash{}  (v  \mmember{}  mapfilter(\mlambda{}m.msg-body(m);\mlambda{}m.has-header-and-in-locs(m;hdr;locs);map(\mlambda{}e.info(e);\mleq{}loc(e))))
\mLeftarrow{}{}\mRightarrow{}  \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:
(RepeatFor  2  (D  0)
THENM  ((FHyp  (-2)  [-1]  THEN  RepeatFor  2  (Thin  (-2)))  ORELSE  (BHyp  -2    THEN  Thin  (-2)))
)

---

Home Index