---

{ [X:{j}]. [x:pi_prefix()]. [send,rcv:chan:Name  var:Name  X].
    (G(x) where   
     G(chan<val>) = send[chan;val]  
     G(chan?(var)) = rcv[chan;var]  X) }

{ Proof }

---

Definitions occuring in Statement :  pi_prefix_ind: pi_prefix_ind,  pi_prefix: pi_prefix(),  name: Name,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  member: t  T,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  pi_prefix_ind: pi_prefix_ind,  so_apply: x[s1;s2],  pi1: fst(t),  pi2: snd(t),  pi_prefix: pi_prefix()
Lemmas :  name_wf,  pi_prefix_wf

---

\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[x:pi\_prefix()].  \mforall{}[send,rcv:chan:Name  {}\mrightarrow{}  var:Name  {}\mrightarrow{}  X].
    (G(x)  where     
      G(chan<val>)  =  send[chan;val]   
      G(chan?(var))  =  rcv[chan;var]  \mmember{}  X)


Date html generated: 2011_08_17-PM-06_40_17
Last ObjectModification: 2011_06_18-PM-12_06_50

Home Index