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 : 
pi2: snd(t), 
run-system: run-system(r;t), 
let: let, 
search: search(k;P), 
lg-size: lg-size(g), 
lambda:
x.A[x], 
lg-is-source: lg-is-source(g;i), 
ifthenelse: if b then t else f fi , 
lt_int: i <z j, 
subtract: n - m, 
natural_number: $n
FDL editor aliases : 
first-choosable
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:
2010_08_27-PM-06_44_28
Last ObjectModification:
2010_05_05-PM-01_11_02
Home
Index