---

Step * 1 of Lemma Comm-next-selex_wf


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

1
.....subterm..... T:t
1:n
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)> ∈ Comm-state()

2
.....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())

---

Latex:

---

Latex:

1.  l$_{comm}$  :  Id
2.  piD  :  PiDataVal()
3.  cSt  :  Comm-state()
4.  \muparrow{}pDVselex?(piD)
\mvdash{}  <<fpf-restrict(Comm-st(cSt);\mlambda{}x.(\mneg{}\msubb{}x  =  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(...)))))
                          >])
    >  \mmember{}  Comm-state()  \mtimes{}  LabeledDAG(Id  \mtimes{}  "msg"\mtimes{}PiDataVal())


By

---

Latex:
MemCD

---

Home Index