mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
n
,
m
:
,
f
,
g
:(
n
m
).
Thm*
(
x
:
n
,
y
:
m
.
f
(
x
,
y
) =
g
(
x
,
y
))
Thm*
Thm*
sum(
f
(
x
,
y
) |
x
<
n
;
y
<
m
) = sum(
g
(
x
,
y
) |
x
<
n
;
y
<
m
)
[double_sum_functionality]
cites the following:
Thm*
n
:
,
f
,
g
:(
n
).
Thm*
(
i
:
n
.
f
(
i
) =
g
(
i
))
sum(
f
(
x
) |
x
<
n
) = sum(
g
(
x
) |
x
<
n
)
[sum_functionality]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
nat
Sections
MarkB
generic
Doc