Nuprl Definition : min-increasing-sequence

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

Definitions occuring in Statement :  le_int: i ≤j primrec: primrec(n;b;c) ifthenelse: if then else fi  it: apply: a lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x
Definitions occuring in definition :  it: inr: inr  inl: inl x apply: a le_int: i ≤j ifthenelse: if then else fi  decide: case of inl(x) => s[x] inr(y) => t[y] lambda: λx.A[x] primrec: primrec(n;b;c)
FDL editor aliases :  min-increasing-sequence

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