Nuprl Definition : Wmul
(w1 * w2) == fix((λWmul,w2. let a,f = w2 in if succ a then (Wmul (f ⋅) + w1) else Wsup(a;λx.(Wmul (f x))) fi )) w2
Definitions occuring in Statement :
Wadd: (w1 + w2),
Wsup: Wsup(a;b),
ifthenelse: if b then t else f fi ,
it: ⋅,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
fix: fix(F),
spread: spread def,
ifthenelse: if b then t else f fi ,
Wadd: (w1 + w2),
it: ⋅,
Wsup: Wsup(a;b),
lambda: λx.A[x],
apply: f a
FDL editor aliases :
Wmul
Latex:
(w1 * w2) ==
fix((\mlambda{}Wmul,w2. let a,f = w2 in if succ a then (Wmul (f \mcdot{}) + w1) else Wsup(a;\mlambda{}x.(Wmul (f x))) fi ))\000C w2
Date html generated:
2016_05_14-AM-06_17_12
Last ObjectModification:
2015_09_22-PM-05_47_24
Theory : co-recursion
Home
Index