(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
1
1
1.
f
:
0
2.
m
:
1
0 = sum(
f
(
x
) |
x
<
m
)+sum(
f
(
x
+
m
) |
x
< 0-
m
)
By:
Subst' (
m
= 0) 0 THEN Reduce 0
Generated subgoals:
None
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
0
1
0 = sum(f(x) | x < m)+sum(f(x+m) | x < 0-m)0
1
0 = sum(f(x) | x < m)+sum(f(x+m) | x < 0-m)
