Nuprl Definition : append-finite-nat-seq
f**g == let n,s = f in let m,r = g in λx.if (x) < (n) then s x else (r (x - n))^(n + m)
Definitions occuring in Statement :
mk-finite-nat-seq: f^(n),
less: if (a) < (b) then c else d,
apply: f a,
lambda: λx.A[x],
spread: spread def,
subtract: n - m,
add: n + m
Definitions occuring in definition :
spread: spread def,
mk-finite-nat-seq: f^(n),
add: n + m,
lambda: λx.A[x],
less: if (a) < (b) then c else d,
apply: f a,
subtract: n - m
FDL editor aliases :
append-finite-nat-seq
Latex:
f**g == let n,s = f in let m,r = g in \mlambda{}x.if (x) < (n) then s x else (r (x - n))\^{}(n + m)
Date html generated:
2016_05_14-PM-09_54_34
Last ObjectModification:
2016_01_15-AM-09_03_33
Theory : continuity
Home
Index