---

Step * 1 1 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)> ∈ st:Id fp-> pi_prefix() List × (Id × (pi_prefix() List)) List × Id × 𝔹 × ℕ
BY
{ Auto }

---

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)>  \mmember{}  st:Id  fp->  pi\_prefix()  List  \mtimes{}  (Id  \mtimes{}  (pi\_prefix()  List))  List  \mtimes{}  Id  \mtimes{}  \mBbbB{}  \mtimes{}  \mBbbN{}


By

---

Latex:
Auto

---

Home Index