---

Step * of Lemma member-local-simulation-inputs

∀f:Name ⟶ Type
  ∀[Info:Type]
    ∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
      ∀e:E. ∀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)))) 
      supposing hdr encodes Id × Info
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `local-simulation-inputs` 0
   THEN (InstLemma `member-mapfilter` [⌜Message(f)⌝;⌜map(λe.info(e);≤loc(e))⌝;⌜λm.has-header-and-in-locs(m;hdr;locs)⌝;
         ⌜Id × Info⌝;⌜λm.msg-body(m)⌝
         ;⌜v⌝]⋅
         THENA (Auto
                THEN Try ((Reduce (-1)
                           THEN D -1
                           THEN (RWO "assert-has-header-and-in-locs" (-1) THENA Auto)
                           THEN D -1
                           THEN Unfold `msg-type` 0
                           THEN HypSubst' (-2) 0
                           THEN Auto))
                )
         )
   THEN Reduce (-1)) }

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. e : E@i
8. v : Id × Info@i
9. (v ∈ mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e))))
⇐⇒ ∃y:Message(f)
     ((y ∈ map(λe.info(e);≤loc(e))) ∧ ((↑has-header-and-in-locs(y;hdr;locs)) c∧ (v = msg-body(y) ∈ (Id × Info))))
⊢ (v ∈ mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e))))
⇐⇒ ∃e':E. (e' ≤loc e  ∧ (msg-header(info(e')) = hdr ∈ Name) ∧ fst(v) ↓∈ locs ∧ (v = msg-body(info(e')) ∈ (Id × Info)))

---

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{}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'))))) 
            supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `local-simulation-inputs`  0
  THEN  (InstLemma  `member-mapfilter`  [\mkleeneopen{}Message(f)\mkleeneclose{};\mkleeneopen{}map(\mlambda{}e.info(e);\mleq{}loc(e))\mkleeneclose{};
              \mkleeneopen{}\mlambda{}m.has-header-and-in-locs(m;hdr;locs)\mkleeneclose{};\mkleeneopen{}Id  \mtimes{}  Info\mkleeneclose{};\mkleeneopen{}\mlambda{}m.msg-body(m)\mkleeneclose{}
              ;\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  Try  ((Reduce  (-1)
                                                  THEN  D  -1
                                                  THEN  (RWO  "assert-has-header-and-in-locs"  (-1)  THENA  Auto)
                                                  THEN  D  -1
                                                  THEN  Unfold  `msg-type`  0
                                                  THEN  HypSubst'  (-2)  0
                                                  THEN  Auto))
                            )
              )
  THEN  Reduce  (-1))

---

Home Index