---

Step * 1 2 of Lemma Comm-next-selex_wf

.....subterm..... T:t
2:n
1. l_comm : Id
2. piD : PiDataVal()
3. cSt : Comm-state()
4. ↑pDVselex?(piD)
⊢ 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))))))
           >]) ∈ LabeledDAG(Id × "msg"×PiDataVal())
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  l$_{comm}$  :  Id
2.  piD  :  PiDataVal()
3.  cSt  :  Comm-state()
4.  \muparrow{}pDVselex?(piD)
\mvdash{}  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(...)))))
                      >])  \mmember{}  LabeledDAG(Id  \mtimes{}  "msg"\mtimes{}PiDataVal())


By

---

Latex:
Auto

---

Home Index