#f(e) ==
  Y (num-antecedents,e.if f e = e then 0 else 1 + (num-antecedents (f e)) fi ) 
  e



Definitions :  ycomb: Y,  lambda: x.A[x],  ifthenelse: if b then t else f fi ,  es-eq-E: e = e',  add: n + m,  natural_number: $n,  apply: f a
FDL editor aliases :  num-antecedents

\#f(e)  ==    Y  (\mlambda{}num-antecedents,e.if  f  e  =  e  then  0  else  1  +  (num-antecedents  (f  e))  fi  )  e


Date html generated: 2010_08_27-PM-02_07_03
Last ObjectModification: 2009_12_16-AM-01_30_43

Home Index