---

Step * of Lemma Comm-next-selex_wf

∀[l_comm:Id]. ∀[piD:PiDataVal()]. ∀[cSt:Comm-state()].
  Comm-next-selex(l_comm;piD;cSt) ∈ Comm-output() supposing ↑pDVselex?(piD)
BY
{ (Auto THEN RepUR ``Comm-next-selex let Comm-output`` 0) }

1
1. l_comm : Id
2. piD : PiDataVal()
3. cSt : Comm-state()
4. ↑pDVselex?(piD)
⊢ <<fpf-restrict(Comm-st(cSt);λx.(¬bx = fst(snd(pDVselex-rndv1(piD)))))
   , Comm-q(cSt)
   , Comm-req_from(cSt)
   , ff
   , Comm-count(cSt)>
  , make-lg([<l_comm, mk-tagged("msg";pDVcontinue())>;
             <Comm-req_from(cSt), mk-tagged("msg";pDVmsg(snd(snd(snd(pDVselex-rndv1(piD))));fst(pDVselex-rndv1(piD))))>;
             <fst(snd(pDVselex-rndv1(piD)))
             , mk-tagged("msg";pDVmsg(snd(snd(snd(pDVselex-rndv1(piD))));fst(snd(snd(pDVselex-rndv1(piD))))))
             >])
  > ∈ Comm-state() × LabeledDAG(Id × "msg"×PiDataVal())

---

Latex:

---

Latex:
\mforall{}[l$_{comm}$:Id].  \mforall{}[piD:PiDataVal()].  \mforall{}[cSt:Comm-state()].
    Comm-next-selex(l$_{comm}$;piD;cSt)  \mmember{}  Comm-output()  supposing  \muparrow{}pDVselex?(piD)


By

---

Latex:
(Auto  THEN  RepUR  ``Comm-next-selex  let  Comm-output``  0)

---

Home Index