Nuprl Definition : coded-seq1

coded-seq1(k;x;n)
==r if (k =z 0) then x else let y,m = coded-pair(x) in if (n =z k) then m else coded-seq1(k - 1;y;n) fi  fi 
coded-seq1(k;x;n) ==
  fix((λcoded-seq1,k,x. if (k =z 0)
                       then x
                       else let y,m = coded-pair(x) 
                            in if (n =z k) then m else coded-seq1 (k - 1) y fi 
                       fi )) 
  k 
  x


Definitions occuring in Statement :  coded-pair: coded-pair(m),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  natural_number: $n,  subtract: n - m,  apply: f a,  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  coded-pair: coded-pair(m),  spread: spread def,  lambda: λx.A[x],  fix: fix(F)
FDL editor aliases :  coded-seq1
Latex:
coded-seq1(k;x;n)
==r  if  (k  =\msubz{}  0)
        then  x
        else  let  y,m  =  coded-pair(x) 
                  in  if  (n  =\msubz{}  k)  then  m  else  coded-seq1(k  -  1;y;n)  fi 
        fi 

Latex:
coded-seq1(k;x;n)  ==
    fix((\mlambda{}coded-seq1,k,x.  if  (k  =\msubz{}  0)
                                              then  x
                                              else  let  y,m  =  coded-pair(x) 
                                                        in  if  (n  =\msubz{}  k)  then  m  else  coded-seq1  (k  -  1)  y  fi 
                                              fi  )) 
    k 
    x


Date html generated: 2019_06_20-PM-02_39_45
Last ObjectModification: 2019_06_12-PM-00_27_50

Theory : num_thy_1


Home Index