Nuprl Definition : int_seg_decide_all

int_seg_decide_all(d;i;j) ==
  fix((λG,x. if j ≤then inl ⋅ else case of inl(z) => (x 1) inr(z) => inr ⋅  fi )) i

Definitions occuring in Statement :  le_int: i ≤j ifthenelse: if then else fi  it: apply: a fix: fix(F) lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x add: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) lambda: λx.A[x] ifthenelse: if then else fi  le_int: i ≤j inl: inl x decide: case of inl(x) => s[x] inr(y) => t[y] apply: a add: m natural_number: $n inr: inr  it:
FDL editor aliases :  int_seg_decide

int\_seg\_decide\_all(d;i;j)  ==
    fix((\mlambda{}G,x.  if  j  \mleq{}z  x  then  inl  \mcdot{}  else  case  d  x  of  inl(z)  =>  G  (x  +  1)  |  inr(z)  =>  inr  \mcdot{}    fi  ))  i

Date html generated: 2016_05_14-AM-07_26_31
Last ObjectModification: 2015_09_22-PM-05_46_20

Theory : int_2

Home Index