---

Step * 1 of Lemma Comm-next-continue_wf


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())
BY
{ Auto }

---

Latex:

---

Latex:

1.  l$_{comm}$  :  Id
2.  l$_{choose}$  :  Id
3.  piD  :  PiDataVal()
4.  cSt  :  Comm-state()
5.  \muparrow{}pDVcontinue?(piD)
\mvdash{}  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\mbackslash{}\000Cff24_{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(\mlambda{}x.<l$_{choose}$,  mk-tagged("msg";pDVrequest(x;Comm-count(\000CcSt)))>
                                            snd(snd(snd(Comm-process-q(Comm-q(cSt);l$_{comm}$;Comm-st(\000CcSt))))))])
              >
    fi    \mmember{}  Comm-state()  \mtimes{}  LabeledDAG(Id  \mtimes{}  "msg"\mtimes{}PiDataVal())


By

---

Latex:
Auto

---

Home Index