(7steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
not
nat
occ
natfuns
1
1
1
1
1. (
) ~
2.
f
:
3. Inj(
;
;
f
)
4. Surj(
;
;
f
)
5.
a
:
.
f
(
a
) = (
i
.
f
(
i
,
i
)+1)
False
By:
Analyze-1
Generated subgoal:
1
5.
a
:
6.
f
(
a
) = (
i
.
f
(
i
,
i
)+1)
False
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
a:
i.f(i,i)+1)
False
