Nuprl Definition : pv8_p2_diff_proposal

pv8_p2_diff_proposal(Cid;Op;eq_Cid) ==
  zc.let slt1,cmd1 = zc 
      in z.let slt2,cmd2 = z 
            in (eqof(IntDeq) slt1 slt2)  ((pv8_p2_same_command(Cid;Op;eq_Cid) cmd1 cmd2))


Definitions occuring in Statement :  pv8_p2_same_command: pv8_p2_same_command(Cid;Op;eq_Cid),  band: p  q,  bnot: b,  apply: f a,  lambda: x.A[x],  spread: spread def,  int-deq: IntDeq,  eqof: eqof(d)
FDL editor aliases :  pv8_p2_diff_proposal
pv8\_p2\_diff\_proposal(Cid;Op;eq$_{Cid}$)  ==
    \mlambda{}zc.let  slt1,cmd1  =  zc 
            in  \mlambda{}z.let  slt2,cmd2  =  z 
                        in  (eqof(IntDeq)  slt1  slt2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(pv8\_p2\_same\_command(Cid;Op;eq$_{Cid}\mbackslash{}\000Cff24)  cmd1  cmd2))


Date html generated: 2012_02_20-PM-07_35_29
Last ObjectModification: 2012_02_06-PM-03_03_52

Home Index