---

{ [P:pi_prefix()  ]
    ((chan,val:Name.  P[chan<val>])
     (chan,var:Name.  P[chan?(var)])
     {x:pi_prefix(). P[x]}) }

{ Proof }

---

Definitions occuring in Statement :  pircv: chan?(var),  pisend: chan<val>,  pi_prefix: pi_prefix(),  name: Name,  uall: [x:A]. B[x],  prop: ,  guard: {T},  so_apply: x[s],  all: x:A. B[x],  implies: P  Q,  function: x:A  B[x]
Definitions :  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  all: x:A. B[x],  so_apply: x[s],  guard: {T},  member: t  T,  pi_prefix: pi_prefix(),  pisend: chan<val>,  pircv: chan?(var)
Lemmas :  pi_prefix_wf,  name_wf,  pircv_wf,  pisend_wf

---

\mforall{}[P:pi\_prefix()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}chan,val:Name.    P[chan<val>])  {}\mRightarrow{}  (\mforall{}chan,var:Name.    P[chan?(var)])  {}\mRightarrow{}  \{\mforall{}x:pi\_prefix().  P[x]\})


Date html generated: 2011_08_17-PM-06_40_25
Last ObjectModification: 2011_06_18-PM-12_07_05

Home Index