---

Step * of Lemma rsc4_roundout_wf

[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:].
  (rsc4_roundout(Cmd;cmdeq;coeff;flrs)  Id      Cmd  Id  Cmd List  (Id List)  bag(Id  Message))
BY
{ Try (Unfold `vatype` 0) THEN ProveWfLemma'' }

---

\mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[coeff,flrs:\mBbbZ{}].
    (rsc4\_roundout(Cmd;cmdeq;coeff;flrs)  \mmember{}  Id
                                                                                  {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id
                                                                                  {}\mrightarrow{}  Cmd  List  \mtimes{}  (Id  List)
                                                                                  {}\mrightarrow{}  bag(Id  \mtimes{}  Message))


By

---

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



Home Index