---

Step * of Lemma local-simulation-input-validity_wf

∀[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) ∈ ℙ) 
  supposing hdr encodes Id × Message(g)
BY
{ (Auto
   THEN Unfold `local-simulation-input-validity` 0
   THEN RepeatFor 3 (MemCD)
   THEN Try ((Assert msgval(e) ∈ Id × Message(g) BY (RWO "assert-has-header-and-in-locs" (-1) THEN Complete (Auto))))
   THEN Auto) }

---

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)  \mmember{}  \mBbbP{}) 
    supposing  hdr  encodes  Id  \mtimes{}  Message(g)


By

---

Latex:
(Auto
  THEN  Unfold  `local-simulation-input-validity`  0
  THEN  RepeatFor  3  (MemCD)
  THEN  Try  ((Assert  msgval(e)  \mmember{}  Id  \mtimes{}  Message(g)  BY
                                    (RWO  "assert-has-header-and-in-locs"  (-1)  THEN  Complete  (Auto))))
  THEN  Auto)

---

Home Index