PrintForm
Definitions
Lemmas
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fun
exp
add1
sub
T
:Type,
f
:(
T
T
),
n
:
,
x
:
T
.
f
(
f
^
n
-1(
x
)) =
f
^
n
(
x
)
By:
Auto THEN RWO
Thm*
f
:(
T
T
),
n
:
,
x
:
T
.
f
(
f
^
n
(
x
)) =
f
^
n
+1(
x
) 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
nat
Sections
MarkB
generic
Doc
T:Type, f:(T
T), n:
, x:T. f(f^n-1(x)) = f^n(x) T:Type, 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) 0
