Nuprl Definition : bar-recursion

bar-recursion(d;
              b;
              i;
              s) ==

  fix((λbar-recursion,s. case d s of inl(r) => b s r | inr(r) => i s (λt.(bar-recursion (s @ [t]))))) s

Definitions occuring in Statement : append: as @ bs, cons: [a / b], nil: [], apply: f a, fix: fix(F), lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : fix: fix(F), decide: case b of inl(x) => s[x] | inr(y) => t[y], lambda: λx.A[x], apply: f a, append: as @ bs, cons: [a / b], nil: []
FDL editor aliases : bar-recursion

Latex:
bar-recursion(d; b; i; s) == fix((\mlambda{}bar-recursion,s. case d s of inl(r) => b s r | inr(r) => i s (\mlambda{}t.(bar-recursion (s @ [t]))))\000C) s Date html generated: 2016_05_15-PM-10_04_58 Last ObjectModification: 2015_09_23-AM-08_22_09 Theory : bar!induction Home Index