Nuprl Definition : decidable-bar-rec

decidable-bar-rec(dec;base;ind;n;s)

==r case dec n s of inl(r) => base n s r | inr(x) => ind n s (λt.decidable-bar-rec(dec;base;ind;n + 1;s.t@n))

decidable-bar-rec(dec;base;ind;n;s) ==
  fix((λdecidable-bar-rec,n,s. case dec n s
                               of inl(r) =>
                               base n s r
                               | inr(x) =>
                               ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))))
  n
  s

Definitions occuring in Statement : seq-add: s.x@n, apply: f a, fix: fix(F), lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y], add: n + m, natural_number: $n
Definitions occuring in definition : seq-add: s.x@n, natural_number: $n, add: n + m, apply: f a, lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y], fix: fix(F)
FDL editor aliases : decidable-bar-rec decidable-bar-rec decidable-bar-rec

Latex:
decidable-bar-rec(dec;base;ind;n;s) ==r case dec n s of inl(r) => base n s r | inr(x) => ind n s (\mlambda{}t.decidable-bar-rec(dec;base;ind;n + 1;s.t@n))

Latex:
decidable-bar-rec(dec;base;ind;n;s) == fix((\mlambda{}decidable-bar-rec,n,s. case dec n s of inl(r) => base n s r | inr(x) => ind n s (\mlambda{}t.(decidable-bar-rec (n + 1) s.t@n)))) n s Date html generated: 2016_05_19-PM-00_03_46 Last ObjectModification: 2016_05_15-PM-04_57_15 Theory : continuity Home Index