#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