---

Step * of Lemma Comm-next-continue_wf

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

1
1. l_comm : Id
2. l_choose : Id
3. piD : PiDataVal()
4. cSt : Comm-state()
5. ↑pDVcontinue?(piD)
⊢ if Comm-waiting(cSt) then <cSt, make-lg([])>
  if null(fst(Comm-process-q(Comm-q(cSt);l_comm;Comm-st(cSt))))
    then <<fst(snd(Comm-process-q(Comm-q(cSt);l_comm;Comm-st(cSt)))), [], l_comm, ff, Comm-count(cSt)>, make-lg([])>
  else <<fst(snd(Comm-process-q(Comm-q(cSt);l_comm;Comm-st(cSt))))
        , fst(Comm-process-q(Comm-q(cSt);l_comm;Comm-st(cSt)))
        , fst(snd(snd(Comm-process-q(Comm-q(cSt);l_comm;Comm-st(cSt)))))
        , tt
        , Comm-count(cSt) + 1>
       , make-lg([<l_comm, mk-tagged("msg";pDVcontinue())> / 
                  map(λx.<l_choose, mk-tagged("msg";pDVrequest(x;Comm-count(cSt)))>;
                      snd(snd(snd(Comm-process-q(Comm-q(cSt);l_comm;Comm-st(cSt))))))])
       >
  fi  ∈ Comm-state() × LabeledDAG(Id × "msg"×PiDataVal())

---

Latex:

---

Latex:
\mforall{}[l$_{comm}$,l$_{choose}$:Id].  \mforall{}[piD:PiDataVal()].  \mforall{}[cSt:Com\000Cm-state()].
    Comm-next-continue(l$_{comm}$;l$_{choose}$;piD;cSt)  \mmember{}  Comm\000C-output()  supposing  \muparrow{}pDVcontinue?(piD)


By

---

Latex:
Auto
THEN  RepUR  ``Comm-output  Comm-next-continue  let``  0

---

Home Index