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_iter
Def
f
{
i
}(
x
) == if
i
=
0
x
else
f
(
f
{
i
-1}(
x
)) fi (recursive)
Thm*
f
:(
A
A
),
i
:
.
f
{
i
}
A
A
eq_int
Def
i
=
j
== if
i
=
j
true
; false
fi
Thm*
i
,
j
:
. (
i
=
j
)
Syntax:
f
{
i
}
has structure:
compose_iter(
f
;
i
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc