Nuprl Definition : pv8_p1_on_p2b

pv8_p1_on_p2b() ==
  bnum,z.
   let a,b' = z 
   in waitfor.if eqof(union-deq(  Id;Unit;product-deq(;Id;IntDeq;IdDeq);unit-deq())) bnum b'
               then waitfor - a
               else waitfor
               fi 


Definitions occuring in Statement :  id-deq: IdDeq,  Id: Id,  ifthenelse: if b then t else f fi ,  unit: Unit,  apply: f a,  lambda: x.A[x],  spread: spread def,  product: x:A  B[x],  int: ,  bag-remove: bs - x,  union-deq: union-deq(A;B;a;b),  product-deq: product-deq(A;B;a;b),  unit-deq: unit-deq(),  int-deq: IntDeq,  eqof: eqof(d)
FDL editor aliases :  pv8_p1_on_p2b
pv8\_p1\_on\_p2b()  ==
    \mlambda{}bnum,z.
      let  a,b'  =  z 
      in  \mlambda{}waitfor.if  eqof(union-deq(\mBbbZ{}  \mtimes{}  Id;Unit;product-deq(\mBbbZ{};Id;IntDeq;IdDeq);unit-deq()))  bnum  b'
                              then  waitfor  -  a
                              else  waitfor
                              fi 


Date html generated: 2012_02_20-PM-07_26_54
Last ObjectModification: 2012_02_06-PM-01_45_15

Home Index