---

Step * of Lemma local-simulation-input-consistency_wf

∀[f,g:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[i,j:Id].  (local-simulation-input-consistency(g;X;hdr;locs;es;i;j) ∈ ℙ) supposing hdr encodes Id × Message(g)
BY
{ (ProveWfLemma THEN Using [`Info',⌜Message(g)⌝] MemCD⋅ 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{}[i,j:Id].    (local-simulation-input-consistency(g;X;hdr;locs;es;i;j)  \mmember{}  \mBbbP{}) 
    supposing  hdr  encodes  Id  \mtimes{}  Message(g)


By

---

Latex:
(ProveWfLemma  THEN  Using  [`Info',\mkleeneopen{}Message(g)\mkleeneclose{}]  MemCD\mcdot{}  THEN  Auto)

---

Home Index