---

Step * of Lemma local-simulation-msg-constraint

∀[f,g:Name ⟶ Type]. ∀[X:EClass(Interface)].
  ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
    ∀[hdrs:Name List]. ∀[i:Id].
      (local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)
      ⇒ (∀e:E. ((loc(e) = i ∈ Id) ⇒ eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g)))) 
    supposing hdr encodes Id × Message(g) 
  supposing LocalClass(X)
BY
{ (Intros
   THEN (InstLemma `local-simulation-eo_wf`  [⌜f⌝;⌜Message(g)⌝;⌜es⌝;⌜hdr⌝;⌜locs⌝;⌜e⌝]⋅ THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN Unhide
   THEN RenameVar `j' (-2)
   THEN (Assert j ∈ E BY
               Declaration)
   THEN RepUR ``local-simulation-eo`` -3
   THEN (RWO "global-eo-E-sq" (-3) THENA Auto)
   THEN D -3
   THEN Thin (-3)
   THEN RepUR ``local-simulation-inputs`` -3
   THEN (RWW "length-mapfilter filter-map length-map" (-3) THENA Auto)
   THEN RepUR ``compose`` -3) }

1
1. f : Name ⟶ Type
2. g : Name ⟶ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℕ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
16. (header(j) ∈ hdrs)@i
17. j ∈ E
⊢ ↓∃e':E. ∃delay:ℤ. ((e' < j) ∧ make-msg-interface(delay;loc(j);info(j)) ∈ X(e'))

---

Latex:

---

Latex:
\mforall{}[f,g:Name  {}\mrightarrow{}  Type].  \mforall{}[X:EClass(Interface)].
    \mforall{}[es:EO+(Message(f))].  \mforall{}[hdr:Name].  \mforall{}[locs:bag(Id)].
        \mforall{}[hdrs:Name  List].  \mforall{}[i:Id].
            (local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)
            {}\mRightarrow{}  (\mforall{}e:E
                        ((loc(e)  =  i)
                        {}\mRightarrow{}  eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g)))) 
        supposing  hdr  encodes  Id  \mtimes{}  Message(g) 
    supposing  LocalClass(X)


By

---

Latex:
(Intros
  THEN  (InstLemma  `local-simulation-eo\_wf`    [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Message(g)\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Unhide
  THEN  RenameVar  `j'  (-2)
  THEN  (Assert  j  \mmember{}  E  BY
                          Declaration)
  THEN  RepUR  ``local-simulation-eo``  -3
  THEN  (RWO  "global-eo-E-sq"  (-3)  THENA  Auto)
  THEN  D  -3
  THEN  Thin  (-3)
  THEN  RepUR  ``local-simulation-inputs``  -3
  THEN  (RWW  "length-mapfilter  filter-map  length-map"  (-3)  THENA  Auto)
  THEN  RepUR  ``compose``  -3)

---

Home Index