---

Step * of Lemma rsc4_message-constraint_wf

[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:]. [locs:bag(Id)].
  (rsc4_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;locs)  EO'  ')
BY
{ Try (Unfold `vatype` 0) THEN ProveWfLemma'' }

---

\mforall{}[Cmd:ValueAllType].  \mforall{}[clients:bag(Id)].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[coeff,flrs:\mBbbZ{}].  \mforall{}[locs:bag(Id)].
    (rsc4\_message-constraint\{i:l\}(Cmd;clients;cmdeq;coeff;flrs;locs)  \mmember{}  EO'  {}\mrightarrow{}  \mBbbP{}')


By

---

Try  (Unfold  `vatype`  0)  THEN  ProveWfLemma''



Home Index