---

G(x) where   
G(chan<val>) = send[chan; val]  
G(chan?(var)) = rcv[chan; var] ==
  case x of inl(x) => send[fst(x); snd(x)] | inr(x) => rcv[fst(x); snd(x)]

---

Definitions :  decide: case b of inl(x) => s[x] | inr(y) => t[y],  pi1: fst(t),  pi2: snd(t)
FDL editor aliases :  pi_prefix_ind pi_prefix_ind

---

G(x)  where     
G(chan<val>)  =  send[chan;  val]   
G(chan?(var))  =  rcv[chan;  var]  ==
    case  x  of  inl(x)  =>  send[fst(x);  snd(x)]  |  inr(x)  =>  rcv[fst(x);  snd(x)]


Date html generated: 2010_08_27-PM-08_36_28
Last ObjectModification: 2010_02_11-PM-06_31_03

Home Index