(4steps total)
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
T
:Type,
f
:(
T
T
),
n
:
,
x
:
T
.
f
(
f
^
n
(
x
)) =
f
^
n
+1(
x
)
By:
Auto THEN Subst (
f
^
n
+1 =
f
o
f
^
n
) 0 THEN Reduce 0
Generated subgoal:
1
1.
T
: Type
2.
f
:
T
T
3.
n
:
4.
T
f
^
n
+1 =
f
o
f
^
n
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
mb
nat
Sections
MarkB
generic
Doc
T:Type, f:(T
T), n:
, x:T. f(f^n(x)) = f^n+1(x) T:Type, f:(TT), n:, x:T. f(f^n(x)) = f^n+1(x)T
f^n+1 = f o f^n
