---

Step * of Lemma iseg-local-simulation-inputs

∀f:Name ─→ Type
  ∀[Info:Type]
    ∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
      ∀e1,e2:E.  (e1 ≤loc e2  ⇒ local-simulation-inputs(es;e1;hdr;locs) ≤ local-simulation-inputs(es;e2;hdr;locs)) 
      supposing hdr encodes Id × Info
BY
{ (Auto THEN RepUR ``local-simulation-inputs`` 0) }

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. e1 : E@i
8. e2 : E@i
9. e1 ≤loc e2 @i
⊢ mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e1))) ≤
   mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e2)))

---

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{}  local-simulation-inputs(es;e1;hdr;locs)  \mleq{}  local-simulation-inputs(es;e2;hdr;locs)) 
            supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(Auto  THEN  RepUR  ``local-simulation-inputs``  0)

---

Home Index