---

Step * of Lemma rsc4_add_to_quorum_wf

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

---

\mforall{}[Cmd:ValueAllType]
    (rsc4\_add\_to\_quorum(Cmd)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}
                                                          {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id
                                                          {}\mrightarrow{}  Cmd  List  \mtimes{}  (Id  List)
                                                          {}\mrightarrow{}  (Cmd  List  \mtimes{}  (Id  List)))


By

---

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



Home Index