Nuprl Definition : gammaFIM
gammaFIM(a;g;h) ==  list_ind_reverse(a;[];
r,f,l. if (g (r @ [l]) =
 0) then r @ [l] else r @ [h r] fi )
Definitions occuring in Statement : 
append: as @ bs, 
eq_int: (i =
 j), 
ifthenelse: if b then t else f fi , 
apply: f a, 
lambda:
x.A[x], 
natural_number: $n
FDL editor aliases : 
gammaFIM
gammaFIM(a;g;h)  ==
    list\_ind\_reverse(a;[];\mlambda{}r,f,l.  if  (g  (r  @  [l])  =\msubz{}  0)  then  r  @  [l]  else  r  @  [h  r]  fi  )
Date html generated:
2013_03_20-AM-10_32_46
Last ObjectModification:
2013_03_08-PM-10_03_19
Home
Index