Nuprl Definition : int_seg_decide

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

Definitions occuring in Statement :  it: less: if (a) < (b)  then c  else d apply: a fix: fix(F) lambda: λx.A[x] pair: <a, b> 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) less: if (a) < (b)  then c  else d decide: case of inl(x) => s[x] inr(y) => t[y] inl: inl x pair: <a, b> apply: a add: m natural_number: $n inr: inr  lambda: λx.A[x] it:
FDL editor aliases :  int_seg_decide

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

Date html generated: 2016_05_13-PM-03_47_40
Last ObjectModification: 2015_09_22-PM-05_45_15

Theory : call!by!value_2

Home Index