Nuprl Definition : coded-seq
coded-seq(x) == if (x =z 0) then <0, λx.x> else let a,b = coded-pair(x - 1) in <a + 1, λn.coded-seq1(a;b;n)> fi
Definitions occuring in Statement :
coded-seq1: coded-seq1(k;x;n),
coded-pair: coded-pair(m),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
coded-seq1: coded-seq1(k;x;n),
lambda: λx.A[x],
natural_number: $n,
add: n + m,
pair: <a, b>,
subtract: n - m,
coded-pair: coded-pair(m),
spread: spread def,
eq_int: (i =z j),
ifthenelse: if b then t else f fi
FDL editor aliases :
coded-seq
Latex:
coded-seq(x) ==
if (x =\msubz{} 0) then ɘ, \mlambda{}x.x> else let a,b = coded-pair(x - 1) in <a + 1, \mlambda{}n.coded-seq1(a;b;n)> fi
Date html generated:
2019_06_20-PM-02_40_23
Last ObjectModification:
2019_06_12-PM-00_28_24
Theory : num_thy_1
Home
Index