(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
2
1.
f
:
2.
i
:
. 0
i
f
(
i
) =
i
2
3.
i
:
.
0
i
f
(
i
) = (-
i
)
2-1
Bij(
;
;
f
)
By:
x
,
y
:
.
x
2
y
2-1 By
SideProof
Generated subgoal:
1
4.
x
,
y
:
.
x
2
y
2-1
Bij(
;
;
f
)
16
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(27steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
i:. 0
i 
f(i) = i
2
i:. 
0i f(i) = (-i)2-1
Bij(; ; f)
i:. 0i f(i) = i2
i:. 0i f(i) = (-i)2-1
Bij(; ; f)x,y:. x2 
y2-1 By SideProofx,y:. x2 y2-1
Bij(; ; f)
