Nuprl Definition : seq-add

s.x@n ==  λm.if m=n  then x  else (s m)



Definitions occuring in Statement :  int_eq: if a=b  then c  else d apply: a lambda: λx.A[x]
Definitions occuring in definition :  lambda: λx.A[x] int_eq: if a=b  then c  else d apply: a
FDL editor aliases :  seq-add

Latex:
s.x@n  ==    \mlambda{}m.if  m=n    then  x    else  (s  m)



Date html generated: 2016_05_13-PM-03_48_28
Last ObjectModification: 2015_09_22-PM-05_45_18

Theory : bar-induction


Home Index