(27steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
int
ooc
nat
1
1
f
:(
). (
i
:
. 0
i
f
(
i
) =
i
2) & (
i
:
.
0
i
f
(
i
) = (-
i
)
2-1)
By:
SideProof
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(27steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
f:(
). (
i:. 0
i 
f(i) = i
2) & (i:. 
0i f(i) = (-i)2-1) f:(). (i:. 0i f(i) = i2) & (i:. 0i f(i) = (-i)2-1)
