Nuprl Definition : pi_prefix_ind

pi_prefix_ind(v;
              pisend(chan,var)⇒ send[chan; var];
              pircv(chan,var)⇒ rcv[chan; var])  ==
  let lbl,v1 = v 
  in if lbl="send" then let chan,v2 = v1 in send[chan; v2]
     if lbl="rcv" then let chan,v2 = v1 in rcv[chan; v2]
     else Ax
     fi 


Definitions occuring in Statement :  atom_eq: if a=b then c else d fi ,  spread: spread def,  token: "$token",  axiom: Ax
FDL editor aliases :  pi_prefix_ind pi_prefix_ind
Latex:
pi\_prefix\_ind(v;
                            pisend(chan,var){}\mRightarrow{}  send[chan;  var];
                            pircv(chan,var){}\mRightarrow{}  rcv[chan;  var])    ==
    let  lbl,v1  =  v 
    in  if  lbl="send"  then  let  chan,v2  =  v1  in  send[chan;  v2]
          if  lbl="rcv"  then  let  chan,v2  =  v1  in  rcv[chan;  v2]
          else  Ax
          fi 


Date html generated: 2016_05_17-AM-11_20_20
Last ObjectModification: 2015_12_14-PM-04_50_11

Theory : event-logic-applications


Home Index