Nuprl Definition : stump
stump(t) == wfd-tree-rec(λn,s. ff;r.λn,s. if (n =z 0) then tt else r (s 0) (n - 1) (λi.(s (i + 1))) fi ;t)
Definitions occuring in Statement :
wfd-tree-rec: wfd-tree-rec(b;r.F[r];t),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
bfalse: ff,
btrue: tt,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
wfd-tree-rec: wfd-tree-rec(b;r.F[r];t),
bfalse: ff,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
btrue: tt,
subtract: n - m,
lambda: λx.A[x],
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
stump
Latex:
stump(t) == wfd-tree-rec(\mlambda{}n,s. ff;r.\mlambda{}n,s. if (n =\msubz{} 0) then tt else r (s 0) (n - 1) (\mlambda{}i.(s (i + 1)))\000C fi ;t)
Date html generated:
2016_05_14-AM-06_18_04
Last ObjectModification:
2015_09_22-PM-05_47_29
Theory : co-recursion
Home
Index