Nuprl Definition : ind def

I(v) where I(α) = 
  when x = α < 0,  y = I(α+1).  d[x; y]
  when α = 0.  b
  when  w = α > 0,  z = I(α-1).  u[w; z]
end where  ==
  PRIMITIVE

Latex:
I(v)  where  I(\malpha{})  = 
    when  x  =  \malpha{}  <  0,    y  =  I(\malpha{}+1).    d[x;  y]
    when  \malpha{}  =  0.    b
    when    w  =  \malpha{}  >  0,    z  =  I(\malpha{}-1).    u[w;  z]
end  where    ==
    PRIMITIVE


Date html generated: 2016_05_13-PM-03_03_48
Last ObjectModification: 2006_01_26-PM-03_53_14

Theory : core_1


Home Index