---

Step * of Lemma local-simulation-eo-loc

∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e:E]. ∀[e1:E].  loc(e1) ↓∈ locs supposing hdr encodes Id × Info
BY
{ (InstLemma `local-simulation-eo_wf` []
   THEN RepeatFor 7 (ParallelLast')
   THEN Auto
   THEN All (\h. RepUR ``local-simulation-eo`` h)⋅
   THEN (RWO  "global-eo-loc" 0 THENA Auto)
   THEN (RWO  "global-eo-E-sq" (-1) THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN (InstLemma `local-simulation-inputs_wf` [⌜f⌝;⌜Info⌝;⌜es⌝;⌜hdr⌝;⌜locs⌝;⌜e⌝]⋅ THENA Auto)
   THEN (InstLemma `member-local-simulation-inputs` [⌜f⌝;⌜Info⌝;⌜es⌝;⌜hdr⌝;⌜locs⌝;⌜e⌝]⋅ 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. ∀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

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[Info:Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[hdr:Name].  \mforall{}[locs:bag(Id)].
    \mforall{}[e:E].  \mforall{}[e1:E].    loc(e1)  \mdownarrow{}\mmember{}  locs  supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(InstLemma  `local-simulation-eo\_wf`  []
  THEN  RepeatFor  7  (ParallelLast')
  THEN  Auto
  THEN  All  (\mbackslash{}h.  RepUR  ``local-simulation-eo``  h)\mcdot{}
  THEN  (RWO    "global-eo-loc"  0  THENA  Auto)
  THEN  (RWO    "global-eo-E-sq"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  (InstLemma  `local-simulation-inputs\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `member-local-simulation-inputs`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index