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 :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  spread: spread def,  coded-pair: coded-pair(m),  subtract: n - m,  pair: <a, b>,  add: n + m,  natural_number: $n,  lambda: λx.A[x],  coded-seq1: coded-seq1(k;x;n)
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: 2016_05_15-PM-05_23_38
Last ObjectModification: 2015_09_23-AM-07_53_59

Theory : general


Home Index