Nuprl Definition : pv8_p1_on

Nuprl Definition : pv8_p1_on_p1b

pv8_p1_on_p1b(Cid;Op;eq_Cid) ==

bnum,zo.
   let a,zp = zo
   in let b',r = zp
      in

z.let waitfor,pvalues = z
in if eqof(union-deq(

Id;Unit;product-deq(

;Id;IntDeq;IdDeq);unit-deq())) bnum b'
               then let waitfor' = waitfor - a in
                     let pvalues' = pv8_p1_append_news(Cid;Op) pv8_p1_same_pvalue(Cid;Op;eq_Cid) pvalues r in
                     <waitfor', pvalues'>
               else <waitfor, pvalues>
               fi

Definitions occuring in Statement : pv8_p1_append_news: pv8_p1_append_news(Cid;Op), pv8_p1_same_pvalue: pv8_p1_same_pvalue(Cid;Op;eq_Cid), id-deq: IdDeq, Id: Id, ifthenelse: if b then t else f fi , let: let, unit: Unit, apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>, 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_p1b

pv8\_p1\_on\_p1b(Cid;Op;eq$_{Cid}$) == \mlambda{}bnum,zo. let a,zp = zo in let b',r = zp in \mlambda{}z.let waitfor,pvalues = z in if eqof(union-deq(\mBbbZ{} \mtimes{} Id;Unit;product-deq(\mBbbZ{};Id;IntDeq;IdDeq);unit-deq())) bnum b' then let waitfor' = waitfor - a in let pvalues' = pv8\_p1\_append\_news(Cid;Op) pv8\_p1\_same\_pvalue(Cid;Op;eq$\mbackslash{}ff5\000Cf{Cid}$) pvalues r in <waitfor', pvalues'> else <waitfor, pvalues> fi Date html generated: 2012_02_20-PM-07_28_38 Last ObjectModification: 2012_02_06-PM-01_46_22 Home Index