Nuprl Definition : first-choosable
first-choosable(r;t) ==
let G = snd(run-system(r;t)) in
let s = search(lg-size(G);λn.lg-is-source(G;n)) in
if 0 <z s then s - 1 else s fi
Definitions occuring in Statement :
run-system: run-system(r;t),
lg-is-source: lg-is-source(g;i),
lg-size: lg-size(g),
search: search(k;P),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
let: let,
pi2: snd(t),
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
FDL editor aliases :
first-choosable
Latex:
first-choosable(r;t) ==
let G = snd(run-system(r;t)) in
let s = search(lg-size(G);\mlambda{}n.lg-is-source(G;n)) in
if 0 <z s then s - 1 else s fi
Date html generated:
2015_07_23-AM-11_16_52
Last ObjectModification:
2012_02_25-PM-03_45_00
Home
Index