(13steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sum
split
n
:
,
f
:(
n
),
m
:
(
n
+1).
sum(
f
(
x
) |
x
<
n
) = sum(
f
(
x
) |
x
<
m
)+sum(
f
(
x
+
m
) |
x
<
n
-
m
)
By:
Analyze 0 THEN NatInd 1 THEN Reduce 0
Generated subgoals:
1
f
:(
0
),
m
:
1. 0 = sum(
f
(
x
) |
x
<
m
)+sum(
f
(
x
+
m
) |
x
< 0-
m
)
2
steps
2
1.
n
:
2. 0<
n
3.
f
:(
(
n
-1)
),
m
:
(
n
-1+1).
3.
sum(
f
(
x
) |
x
<
n
-1) = sum(
f
(
x
) |
x
<
m
)+sum(
f
(
x
+
m
) |
x
<
n
-1-
m
)
f
:(
n
),
m
:
(
n
+1).
sum(
f
(
x
) |
x
<
n
) = sum(
f
(
x
) |
x
<
m
)+sum(
f
(
x
+
m
) |
x
<
n
-
m
)
10
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(13steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc