---

{ [chan,val:Name].  (chan<val>  pi_prefix()) }

{ Proof }

---

Definitions occuring in Statement :  pisend: chan<val>,  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(),  pisend: chan<val>
Lemmas :  name_wf

---

\mforall{}[chan,val:Name].    (chan<val>  \mmember{}  pi\_prefix())


Date html generated: 2011_08_17-PM-06_39_59
Last ObjectModification: 2011_06_18-PM-12_06_20

Home Index