(16steps 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:
sum
switch
n
:
,
f
:(
n
),
i
:
(
n
-1). sum(
f
((
i
,
i
+1)(
x
)) |
x
<
n
) = sum(
f
(
x
) |
x
<
n
)
By:
Auto
Generated subgoal:
1
1.
n
:
2.
f
:
n
3.
i
:
(
n
-1)
sum(
f
((
i
,
i
+1)(
x
)) |
x
<
n
) = sum(
f
(
x
) |
x
<
n
)
15
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(16steps total)
PrintForm
Definitions
Lemmas
mb
nat
Sections
MarkB
generic
Doc
n:
, f:(
), i:
