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: f a
, 
lambda: λx.A[x]
Definitions occuring in definition : 
lambda: λx.A[x]
, 
int_eq: if a=b  then c  else d
, 
apply: f 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