---

Step * of Lemma local-simulation-E-subtype

∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e1,e2:E].  (e1 ≤loc e2  ⇒ (E ⊆r E)) supposing hdr encodes Id × Info
BY
{ (InstLemma `local-simulation-eo_wf` []
   THEN RepeatFor 7 (ParallelLast')
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN All (RepUR ``local-simulation-eo``)
   THEN (All (RWO "global-eo-E-sq") THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Try (Complete (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. e1 : E
8. global-eo(local-simulation-inputs(es;e1;hdr;locs)) ∈ EO+(Info)
9. e2 : E
10. e1 ≤loc e2 @i
11. x : ℕ||local-simulation-inputs(es;e1;hdr;locs)||@i
12. True@i
⊢ x ∈ ℕ||local-simulation-inputs(es;e2;hdr;locs)||

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[Info:Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[hdr:Name].  \mforall{}[locs:bag(Id)].
    \mforall{}[e1,e2:E].    (e1  \mleq{}loc  e2    {}\mRightarrow{}  (E  \msubseteq{}r  E))  supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(InstLemma  `local-simulation-eo\_wf`  []
  THEN  RepeatFor  7  (ParallelLast')
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  All  (RepUR  ``local-simulation-eo``)
  THEN  (All  (RWO  "global-eo-E-sq")  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Try  (Complete  (Auto)))

---

Home Index