Nuprl Definition : lg-search
lg-search(G;x.P[x]) == let s = search(lg-size(G);λn.P[lg-label(G;n)]) in if (s =z 0) then inr ⋅ else inl (s - 1) fi
Definitions occuring in Statement :
lg-label: lg-label(g;x),
lg-size: lg-size(g),
search: search(k;P),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
let: let,
it: ⋅,
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
subtract: n - m,
natural_number: $n
FDL editor aliases :
lg-search
Latex:
lg-search(G;x.P[x]) ==
let s = search(lg-size(G);\mlambda{}n.P[lg-label(G;n)]) in
if (s =\msubz{} 0) then inr \mcdot{} else inl (s - 1) fi
Date html generated:
2015_07_23-AM-11_04_51
Last ObjectModification:
2012_02_25-PM-03_36_47
Home
Index