Nuprl Definition : pv11_p1_pmax

pv11_p1_pmax(Cmd;ldrs_uid) ==
  λpvals.let g = λbn,slt,z. let bn',z = z in let s',z = z in (slt =z s') ∧b (bn  < bn') in
          let P = λz.let bn,z = z 
                     in let s,c = z 
                        in ¬b(∃zw∈pvals.g bn s zw)_b in
          mapfilter(λx.(snd(x));P;pvals)


Definitions occuring in Statement :  pv11_p1_lt_bnum: pv11_p1_lt_bnum(ldrs_uid),  bl-exists: (∃x∈L.P[x])_b,  mapfilter: mapfilter(f;P;L),  band: p ∧b q,  bnot: ¬bb,  eq_int: (i =z j),  let: let,  pi2: snd(t),  apply: f a,  lambda: λx.A[x],  spread: spread def
FDL editor aliases :  pv11_p1_pmax
Latex:
pv11\_p1\_pmax(Cmd;ldrs$_{uid}$)  ==
    \mlambda{}pvals.let  g  =  \mlambda{}bn,slt,z.  let  bn',z  =  z  in  let  s',z  =  z  in  (slt  =\msubz{}  s')  \mwedge{}\msubb{}  (bn    <  bn')  in
                    let  P  =  \mlambda{}z.let  bn,z  =  z 
                                          in  let  s,c  =  z 
                                                in  \mneg{}\msubb{}(\mexists{}zw\mmember{}pvals.g  bn  s  zw)\_b  in
                    mapfilter(\mlambda{}x.(snd(x));P;pvals)


Date html generated: 2015_07_23-PM-04_11_16
Last ObjectModification: 2014_11_26-AM-11_22_41

Home Index