WhoCites Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Iterated self-composition of a function.

Who Cites compose iter?
compose_iterDef  f{i}(x) == if i=0 x else f(f{i-1}(x)) fi  (recursive)
Thm*  f:(AA), i:f{i AA
eq_intDef  i=j == if i=j true ; false fi
Thm*  i,j:. (i=j 

Syntax:f{i} has structure: compose_iter(fi)

About:
boolbfalsebtrueifthenelseintnatural_numbersubtractint_eq
applyfunctionrecursive_def_noticeuniversememberall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions DiscreteMath Sections DiscrMathExt Doc