---

Step * 1 of Lemma local-simulation-eo-loc


1. f : Name ─→ Type
2. Info : Type
3. es : EO+(Message(f))
4. hdr : Name
5. locs : bag(Id)
6. hdr encodes Id × Info
7. e : E
8. global-eo(local-simulation-inputs(es;e;hdr;locs)) ∈ EO+(Info)
9. e1 : ℕ||local-simulation-inputs(es;e;hdr;locs)||
10. local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Info) List
11. ∀v:Id × Info
      ((v ∈ local-simulation-inputs(es;e;hdr;locs))
      ⇐⇒ ∃e':E
           (e' ≤loc e  ∧ (msg-header(info(e')) = hdr ∈ Name) ∧ fst(v) ↓∈ locs ∧ (v = msg-body(info(e')) ∈ (Id × Info))))
⊢ fst(local-simulation-inputs(es;e;hdr;locs)[e1]) ↓∈ locs
BY
{ (With ⌈local-simulation-inputs(es;e;hdr;locs)[e1]⌉ (D (-1))⋅ THENA Auto) }

1
1. f : Name ─→ Type
2. Info : Type
3. es : EO+(Message(f))
4. hdr : Name
5. locs : bag(Id)
6. hdr encodes Id × Info
7. e : E
8. global-eo(local-simulation-inputs(es;e;hdr;locs)) ∈ EO+(Info)
9. e1 : ℕ||local-simulation-inputs(es;e;hdr;locs)||
10. local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Info) List
11. (local-simulation-inputs(es;e;hdr;locs)[e1] ∈ local-simulation-inputs(es;e;hdr;locs))
⇐⇒ ∃e':E
     (e' ≤loc e 
     ∧ (msg-header(info(e')) = hdr ∈ Name)
     ∧ fst(local-simulation-inputs(es;e;hdr;locs)[e1]) ↓∈ locs
     ∧ (local-simulation-inputs(es;e;hdr;locs)[e1] = msg-body(info(e')) ∈ (Id × Info)))
⊢ fst(local-simulation-inputs(es;e;hdr;locs)[e1]) ↓∈ locs

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  Info  :  Type
3.  es  :  EO+(Message(f))
4.  hdr  :  Name
5.  locs  :  bag(Id)
6.  hdr  encodes  Id  \mtimes{}  Info
7.  e  :  E
8.  global-eo(local-simulation-inputs(es;e;hdr;locs))  \mmember{}  EO+(Info)
9.  e1  :  \mBbbN{}||local-simulation-inputs(es;e;hdr;locs)||
10.  local-simulation-inputs(es;e;hdr;locs)  \mmember{}  (\{i:Id|  i  \mdownarrow{}\mmember{}  locs\}    \mtimes{}  Info)  List
11.  \mforall{}v:Id  \mtimes{}  Info
            ((v  \mmember{}  local-simulation-inputs(es;e;hdr;locs))
            \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')))))
\mvdash{}  fst(local-simulation-inputs(es;e;hdr;locs)[e1])  \mdownarrow{}\mmember{}  locs


By

---

Latex:
(With  \mkleeneopen{}local-simulation-inputs(es;e;hdr;locs)[e1]\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)

---

Home Index