Nuprl Definition : code-seq

code-seq(k;s) ==  if (k =z 0) then 0 else code-pair(k - 1;code-seq1(k;s)) + 1 fi 


Definitions occuring in Statement :  code-seq1: code-seq1(k;s),  code-pair: code-pair(a;b),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  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),  add: n + m,  code-pair: code-pair(a;b),  subtract: n - m,  code-seq1: code-seq1(k;s),  natural_number: $n
FDL editor aliases :  code-seq
Latex:
code-seq(k;s)  ==    if  (k  =\msubz{}  0)  then  0  else  code-pair(k  -  1;code-seq1(k;s))  +  1  fi 


Date html generated: 2016_05_15-PM-05_23_19
Last ObjectModification: 2015_09_23-AM-07_53_52

Theory : general


Home Index