---

Step * of Lemma rsc4_when_new_proposal_wf

[Cmd:ValueAllType]. (rsc4_when_new_proposal(Cmd)  Id    Cmd    ( List)  bag(  Cmd))
BY
{ Try (Unfold `vatype` 0) THEN ProveWfLemma'' }

---

\mforall{}[Cmd:ValueAllType].  (rsc4\_when\_new\_proposal(Cmd)  \mmember{}  Id  {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  Cmd  {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  (\mBbbZ{}  List)  {}\mrightarrow{}  bag(\mBbbZ{}  \mtimes{}  Cmd))


By

---

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



Home Index