Nuprl Definition : int_seg_decide

Nuprl Definition : int_seg_decide_all

int_seg_decide_all(d;i;j) ==

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

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

Latex:
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