---

{ [chan,var:Name].  (chan?(var)  pi_prefix()) }

{ Proof }

---

Definitions occuring in Statement :  pircv: chan?(var),  pi_prefix: pi_prefix(),  name: Name,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  member: t  T,  pi_prefix: pi_prefix(),  pircv: chan?(var)
Lemmas :  name_wf

---

\mforall{}[chan,var:Name].    (chan?(var)  \mmember{}  pi\_prefix())


Date html generated: 2011_08_17-PM-06_40_08
Last ObjectModification: 2011_06_18-PM-12_06_35

Home Index