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