Nuprl Definition : min-increasing-sequence

min-increasing-sequence(a;n;k) ==
  primrec(n;inr ⋅ ;λi,r. case r of inl(x) => inl x | inr(x) => if k ≤z a i then inl i else inr ⋅  fi )


Definitions occuring in Statement :  le_int: i ≤z j,  primrec: primrec(n;b;c),  ifthenelse: if b then t else f fi ,  it: ⋅,  apply: f a,  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x
Definitions occuring in definition :  it: ⋅,  inr: inr x ,  inl: inl x,  apply: f a,  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  lambda: λx.A[x],  primrec: primrec(n;b;c)
FDL editor aliases :  min-increasing-sequence
Latex:
min-increasing-sequence(a;n;k)  ==
    primrec(n;inr  \mcdot{}  ;\mlambda{}i,r.  case  r
                                                  of  inl(x)  =>
                                                  inl  x
                                                  |  inr(x)  =>
                                                  if  k  \mleq{}z  a  i  then  inl  i  else  inr  \mcdot{}    fi  )


Date html generated: 2017_04_20-AM-07_36_42
Last ObjectModification: 2017_04_18-AM-10_33_22

Theory : continuity


Home Index