mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
f
:(
T
T
),
n
:
,
x
:
T
.
f
(
f
^
n
-1(
x
)) =
f
^
n
(
x
)
[fun_exp_add1_sub]
cites the following:
3
Thm*
f
:(
T
T
),
n
:
,
x
:
T
.
f
(
f
^
n
(
x
)) =
f
^
n
+1(
x
)
[fun_exp_add1]
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-1(x)) = f^n(x)f:(TT), n:, x:T. f(f^n(x)) = f^n+1(x)f:(TT), n:, x:T. f(f^n-1(x)) = f^n(x)f:(TT), n:, x:T. f(f^n(x)) = f^n+1(x)