---

Step * 1 of Lemma pi-system_wf


1. f : (Id List) ─→ Id
2. l_server : Id
3. l_choose : Id
4. l_comm : Id
5. l_pi : Id
6. P : pi_term()@i
⊢ <"msg", pDVfire()> ∈ pCom(P.piM(P))
BY
{ (RepUR ``pCom Com`` 0  THEN Fold `mk-tagged` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  (Id  List)  {}\mrightarrow{}  Id
2.  l$_{server}$  :  Id
3.  l$_{choose}$  :  Id
4.  l$_{comm}$  :  Id
5.  l$_{pi}$  :  Id
6.  P  :  pi\_term()@i
\mvdash{}  <"msg",  pDVfire()>  \mmember{}  pCom(P.piM(P))


By

---

Latex:
(RepUR  ``pCom  Com``  0    THEN  Fold  `mk-tagged`  0  THEN  Auto)

---

Home Index