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