---

Step * 1 1 of Lemma Comm-next-selex_wf

.....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()
BY
{ Unfold `Comm-state` 0 }

1
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 × 𝔹 × ℕ

---

Latex:

---

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


By

---

Latex:
Unfold  `Comm-state`  0

---

Home Index