Nuprl Definition : bar

Nuprl Definition : bar_recursion

bar_recursion(d;
              b;
              i;
              n;s) ==
  fix((λbar_recursion,n,s. case d n s
                           of inl(r) =>
                           b n s r
                           | inr(r) =>

                           i n s (λt.(bar_recursion (n + 1) (λm.if m=n  then t  else (s m))))))

n
s

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

Latex:
bar\_recursion(d; b; i; n;s) == fix((\mlambda{}bar$_{recursion}$,n,s. case d n s of inl(r) => b n s r | inr(r) => i n s (\mlambda{}t.(bar$_{recursion}$ (n + 1) (\mlambda{}m.if m=n then \000Ct else (s m)))))) n s Date html generated: 2016_05_13-PM-03_49_33 Last ObjectModification: 2015_09_22-PM-05_45_18 Theory : bar-induction Home Index