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 :  natural_number: $n,  code-seq1: code-seq1(k;s),  subtract: n - m,  code-pair: code-pair(a;b),  add: n + m,  eq_int: (i =z j),  ifthenelse: if b then t else f fi 
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: 2019_06_20-PM-02_40_12
Last ObjectModification: 2019_06_12-PM-00_28_14

Theory : num_thy_1


Home Index