Nuprl Definition : W_iterate_functor
W_iterate_functor(A;a.B[a];T.F[T];w)==r F[⋂x:{b:W(A;a.B[a])| b < w} . W_iterate_functor(A;a.B[a];T.F[T];x)]
W_iterate_functor(A;a.B[a];T.F[T];w) == fix((λW_iterate_functor,w. F[⋂x:{b:W(A;a.B[a])| b < w} . (W_iterate_functor x)\000C])) w
Definitions occuring in Statement :
Wcmp: Wcmp(A;a.B[a];leq),
W: W(A;a.B[a]),
bfalse: ff,
infix_ap: x f y,
set: {x:A| B[x]} ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
isect: ⋂x:A. B[x]
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
isect: ⋂x:A. B[x],
set: {x:A| B[x]} ,
W: W(A;a.B[a]),
infix_ap: x f y,
Wcmp: Wcmp(A;a.B[a];leq),
bfalse: ff,
apply: f a
FDL editor aliases :
W_iterate_functor
Latex:
W\_iterate\_functor(A;a.B[a];T.F[T];w)
==r F[\mcap{}x:\{b:W(A;a.B[a])| b < w\} . W\_iterate\_functor(A;a.B[a];T.F[T];x)]
Latex:
W\_iterate\_functor(A;a.B[a];T.F[T];w) ==
fix((\mlambda{}W\_iterate$_{functor}$,w. F[\mcap{}x:\{b:W(A;a.B[a])| b < w\} . (W\_iterate$\mbackslash{}\000Cff5f{functor}$ x)])) w
Date html generated:
2016_05_14-AM-06_16_24
Last ObjectModification:
2015_09_22-PM-05_47_20
Theory : co-recursion
Home
Index