Nuprl Definition : pv8_p1_pmax

pv8_p1_pmax(Cid;Op;ldrs_uid) ==
  pvals.let g = bn,s,z.let bn',z = z in let s',z = z in (eqof(IntDeq) s s')  (pv8_p1_lt_bnum(ldrs_uid) bn bn') in
          let P = z.let bn,z = z 
                     in let s,c = z 
                        in (zvpvals.g bn s zv)_b in
          mapfilter(x.(snd(x));P;pvals)


Definitions occuring in Statement :  pv8_p1_lt_bnum: pv8_p1_lt_bnum(ldrs_uid),  band: p  q,  bnot: b,  let: let,  pi2: snd(t),  apply: f a,  lambda: x.A[x],  spread: spread def,  mapfilter: mapfilter(f;P;L),  int-deq: IntDeq,  eqof: eqof(d),  bl-exists: (xL.P[x])_b
FDL editor aliases :  pv8_p1_pmax pv8_p1_pmax
pv8\_p1\_pmax(Cid;Op;ldrs$_{uid}$)  ==
    \mlambda{}pvals.let  g  =  \mlambda{}bn,s,z.
                                    let  bn',z  =  z 
                                    in  let  s',z  =  z 
                                          in  (eqof(IntDeq)  s  s')  \mwedge{}\msubb{}  (pv8\_p1\_lt\_bnum(ldrs$_{uid}$)  bn  \000Cbn')  in
                    let  P  =  \mlambda{}z.let  bn,z  =  z 
                                          in  let  s,c  =  z 
                                                in  \mneg{}\msubb{}(\mexists{}zv\mmember{}pvals.g  bn  s  zv)\_b  in
                    mapfilter(\mlambda{}x.(snd(x));P;pvals)


Date html generated: 2012_02_20-PM-07_14_41
Last ObjectModification: 2012_02_06-PM-01_37_07

Home Index