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