(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
f
:(
0
),
m
:
1. 0 = sum(
f
(
x
) |
x
<
m
)+sum(
f
(
x
+
m
) |
x
< 0-
m
)
By:
Auto
Generated subgoal:
1
1.
f
:
0
2.
m
:
1
0 = sum(
f
(
x
) |
x
<
m
)+sum(
f
(
x
+
m
) |
x
< 0-
m
)
1
step
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
f:(
0
), m:1. 0 = sum(f(x) | x < m)+sum(f(x+m) | x < 0-m) f:(0), m: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)
