mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
3
Thm*
f
:(
T
T
),
n
:
,
x
:
T
.
f
(
f
^
n
(
x
)) =
f
^
n
+1(
x
)
[fun_exp_add1]
cites the following:
2
Thm*
n
,
m
:
,
f
:(
T
T
).
f
^
n
+
m
=
f
^
n
o
f
^
m
[fun_exp_add]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
nat
Sections
MarkB
generic
Doc
f:(T
T), n:
, x:T. f(f^n(x)) = f^n+1(x)n,m:, f:(TT). f^n+m = f^n o f^mf:(TT), n:, x:T. f(f^n(x)) = f^n+1(x)n,m:, f:(TT). f^n+m = f^n o f^m