---

Step * of Lemma local-simulation-embedding

∀f:Name ─→ Type
  ∀[Info:Type]
    ∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
      ∀e1,e2:E.
        (e1 ≤loc e2  ⇒ (λx.x embeds local-simulation-eo(es;e1;hdr;locs) into local-simulation-eo(es;e2;hdr;locs))) 
      supposing hdr encodes Id × Info
BY
{ (Intros
   THEN Unfold `local-simulation-eo` 0
   THEN BLemma `iseg-es-embedding`
   THEN Auto
   THEN Try ((UsingVars [`Info'] MemCD THEN Auto))
   THEN BLemma `iseg-local-simulation-inputs`
   THEN Auto) }

---

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{}  (\mlambda{}x.x  embeds  local-simulation-eo(es;e1;hdr;locs)  into
                                                local-simulation-eo(es;e2;hdr;locs))) 
            supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(Intros
  THEN  Unfold  `local-simulation-eo`  0
  THEN  BLemma  `iseg-es-embedding`
  THEN  Auto
  THEN  Try  ((UsingVars  [`Info']  MemCD  THEN  Auto))
  THEN  BLemma  `iseg-local-simulation-inputs`
  THEN  Auto)

---

Home Index