Nuprl Definition : stump'
stump'(t) == λn,s. if (n =z 0) then empty-wfd-tree(t) else (¬b(stump(t) n s)) ∧b (stump(t) (n - 1) s) fi
Definitions occuring in Statement :
stump: stump(t),
empty-wfd-tree: empty-wfd-tree(t),
band: p ∧b q,
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
empty-wfd-tree: empty-wfd-tree(t),
band: p ∧b q,
bnot: ¬bb,
apply: f a,
stump: stump(t),
subtract: n - m,
natural_number: $n
FDL editor aliases :
stump'
Latex:
stump'(t) ==
\mlambda{}n,s. if (n =\msubz{} 0) then empty-wfd-tree(t) else (\mneg{}\msubb{}(stump(t) n s)) \mwedge{}\msubb{} (stump(t) (n - 1) s) fi
Date html generated:
2016_05_14-AM-06_18_22
Last ObjectModification:
2015_09_22-PM-05_47_30
Theory : co-recursion
Home
Index